Side preservation for locally finite face fillings

The metric estimates of LocallyFinitePLApproximation put nonincident vertices outside each replacement polygon. This file propagates that information along every replacement edge. The argument is the same connected-side argument used in Moise Chapter 6: an edge can cross a polygonal boundary only where the corresponding abstract edge meets the face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryLift_mem_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (q : StandardFaceBoundary) : ↑(faceBoundaryLift f q) ∈ PlaneGraphRealization.faceInSupport f

The canonical boundary lift belongs to the face whose boundary it parametrizes.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundariesClose_of_lt_vertexSeparationControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (harc : ∀ (p : ↑PlaneGraphRealization.oneSkeletonInSupport), dist (G.graphReplacementMap p) (G.map ↑p) < vertexSeparationControl G ↑p) : FaceBoundariesClose G (faceVertexSeparationRadius G)

A replacement graph pointwise finer than the canonical vertex-separation control is facewise close at the canonical per-face separation radii. This is the bridge from a tolerance-parametrized one-skeleton replacement to the side-preservation entry FaceBoundariesClose G (faceVertexSeparationRadius G).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePolygonalCircle_carrier_subset_graphReplacement {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : (facePolygonalCircle f).carrier ⊆ Set.range G.graphReplacementMap

Every selected face boundary is part of the single global replacement graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_faceInSupport_of_graphReplacement_mem_facePolygonalCircle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (p : ↑PlaneGraphRealization.oneSkeletonInSupport) (hp : G.graphReplacementMap p ∈ (facePolygonalCircle f).carrier) : ↑p ∈ PlaneGraphRealization.faceInSupport f

If a replacement-graph point lies on one face polygon, its source lies in that face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathInOneSkeleton {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑PlaneGraphRealization.oneSkeletonInSupport

Include the interval parametrization of an edge in the source one-skeleton.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_edgePathInOneSkeleton {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Continuous (edgePathInOneSkeleton e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathInOneSkeleton_val {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑(edgePathInOneSkeleton e r) = PlaneGraphRealization.edgePathInSupport e r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeInSupport_subset_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) : PlaneGraphRealization.edgeInSupport e ⊆ PlaneGraphRealization.faceInSupport f

An edge contained in a face has all its support points in that face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathInSupport_parameter_eq_zero_of_mem_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (e : K.Edge) (r : ↑(Set.Icc 0 1)) (hsecond : K.edgeSecond e ∉ K.faceVertices f) (hr : PlaneGraphRealization.edgePathInSupport e r ∈ PlaneGraphRealization.faceInSupport f) : ↑r = 0

If the second endpoint of an edge is absent from a face, an edge-path point in that face must have parameter zero.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathInSupport_parameter_eq_one_of_mem_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (e : K.Edge) (r : ↑(Set.Icc 0 1)) (hfirst : K.edgeFirst e ∉ K.faceVertices f) (hr : PlaneGraphRealization.edgePathInSupport e r ∈ PlaneGraphRealization.faceInSupport f) : ↑r = 1

If the first endpoint of an edge is absent from a face, an edge-path point in that face must have parameter one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacement_mem_facePolygonalCircle_of_edge_subset {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (e : K.Edge) (p : ↑PlaneGraphRealization.oneSkeletonInSupport) (hp : ↑p ∈ PlaneGraphRealization.edgeInSupport e) (hef : ↑e ⊆ K.faceVertices f) : G.graphReplacementMap p ∈ (facePolygonalCircle f).carrier

The replacement of an abstract edge contained in a face lies on that face's polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacementMap_vertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (v : K.Vertex) : ∃ (p : ↑PlaneGraphRealization.oneSkeletonInSupport), ↑↑p = K.vertexPoint v ∧ G.graphReplacementMap p = G.vertexImage v

The simultaneous graph replacement fixes every abstract vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacement_vertex_mem_facePolygonalCircle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (v : K.Vertex) (hvf : v ∈ K.faceVertices f) : G.vertexImage v ∈ (facePolygonalCircle f).carrier

A vertex of a face maps to that face's replacement polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacementMap_edgePathInOneSkeleton_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (e : K.Edge) : G.graphReplacementMap (edgePathInOneSkeleton e ⟨0, ⋯⟩) = G.vertexImage (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacementMap_edgePathInOneSkeleton_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (e : K.Edge) : G.graphReplacementMap (edgePathInOneSkeleton e ⟨1, ⋯⟩) = G.vertexImage (K.edgeSecond e)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceFillingsGraphAvoidInteriors {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Prop

Graph-side compatibility required for coherent cellwise assembly.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceFillingsVerticesAvoidClosedRegions_of_close {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {r : K.Face → ℝ} (hr : ∀ (f : K.Face), 0 < r f) (hsep : FaceVertexThickeningsSeparated G r) (hclose : FaceBoundariesClose G r) : FaceFillingsVerticesAvoidClosedRegions G

Facewise closeness and vertex-to-face separation put every nonincident vertex on the unbounded side of the replacement polygon. This is the locally finite form of Moise's actual Chapter 6 argument: bounded Tietze extension fills the close boundary while avoiding the outside vertex, and no-retraction detects the unbounded side.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceFillingsVerticesAvoidClosedRegions_of_comparison {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {r : K.Face → ℝ} (hr : ∀ (f : K.Face), 0 < r f) (hsep : FaceVertexThickeningsSeparated G r) (comp : K.Face → Plane → Plane) (hcompCont : ∀ (f : K.Face), ContinuousOn (comp f) standardFaceRegion) (hcompMem : ∀ (f : K.Face), ∀ p ∈ standardFaceRegion, comp f p ∈ Metric.cthickening (r f / 2) (G.map '' PlaneGraphRealization.faceInSupport f)) (hclose : ∀ (f : K.Face) (q : StandardFaceBoundary), dist (G.graphReplacementMap (faceBoundaryLift f q)) (comp f ↑q) < r f / 2) : FaceFillingsVerticesAvoidClosedRegions G

Parametrization-independent form of faceFillingsVerticesAvoidClosedRegions_of_close: the comparison map on the standard region may be ANY continuous map whose values stay within half the separation radius of the original face image, and which is within half that radius of the replacement boundary on the frontier. This absorbs the parameter misalignment between the replacement arcs' Path.trans splits and the original edge trims: an aligned comparison built from CentralPolygonalArc.curve_close can discharge the closeness at the approximation-control scale, which the crude same-parameter comparison with faceOriginalMap cannot.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacement_vertex_mem_exterior {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hvertices : FaceFillingsVerticesAvoidClosedRegions G) (f : K.Face) (v : K.Vertex) (hvf : v ∉ K.faceVertices f) : G.vertexImage v ∈ (facePolygonalCircle f).exteriorRegion

A nonincident vertex outside the polygonal closed disk lies in its unbounded component.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceFillingsGraphAvoidInteriors_of_verticesAvoid {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hvertices : FaceFillingsVerticesAvoidClosedRegions G) : FaceFillingsGraphAvoidInteriors G

Moise's vertex-side condition propagates along every edge: the complete simultaneous replacement graph avoids the bounded interior selected for each face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.disjoint_facePolygonalCircle_interiors {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hfaces : Function.Injective K.faceVertices) (hside : FaceFillingsGraphAvoidInteriors G) (f g : K.Face) (hfg : f ≠ g) : Disjoint (facePolygonalCircle f).interiorRegion (facePolygonalCircle g).interiorRegion

Once the replacement graph stays out of every selected bounded component, distinct filled face interiors are disjoint. A vertex of the second face not belonging to the first supplies the strict side witness required by polygonal Jordan separation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.cellwiseCompatibility_of_control {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hfaces : Function.Injective K.faceVertices) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hsep : SeparatesVerticesFromFaces G phi) (hregion : ∀ (f : K.Face), (facePolygonalCircle f).closedRegion ⊆ G.region) (hloc : LocallyFinite fun (f : K.Face) => {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}) : CellwiseCompatibility G

The quantitative Chapter 6 hypotheses, together with local finiteness of the selected closed polygonal disks, produce the complete compatibility package needed for cellwise assembly.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.cellwiseCompatibility_of_facewise_close {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hfaces : Function.Injective K.faceVertices) (hclose : FaceBoundariesClose G (faceVertexSeparationRadius G)) (hregion : ∀ (f : K.Face), (facePolygonalCircle f).closedRegion ⊆ G.region) (hloc : LocallyFinite fun (f : K.Face) => {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}) : CellwiseCompatibility G

Moise's original side-control interface: facewise graph closeness below the canonical vertex-to-face separation radius gives the compatibility package for all Schoenflies fillings. Unlike cellwiseCompatibility_of_control, this formulation does not force one pointwise tolerance to serve every face incident to a source point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.cellwiseCompatibility_of_comparison {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hfaces : Function.Injective K.faceVertices) (comp : K.Face → Plane → Plane) (hcompCont : ∀ (f : K.Face), ContinuousOn (comp f) standardFaceRegion) (hcompMem : ∀ (f : K.Face), ∀ p ∈ standardFaceRegion, comp f p ∈ Metric.cthickening (faceVertexSeparationRadius G f / 2) (G.map '' PlaneGraphRealization.faceInSupport f)) (hclose : ∀ (f : K.Face) (q : StandardFaceBoundary), dist (G.graphReplacementMap (faceBoundaryLift f q)) (comp f ↑q) < faceVertexSeparationRadius G f / 2) (hregion : ∀ (f : K.Face), (facePolygonalCircle f).closedRegion ⊆ G.region) (hloc : LocallyFinite fun (f : K.Face) => {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}) : CellwiseCompatibility G

The compatibility package from a parametrization-independent comparison map at the canonical separation radii. This is the entry matched to the locally finite replacement arcs: their curve_close tracking is stated against the trimmed original curve, not against the Path.trans parameter, so only a reparametrized comparison can be discharged at the approximation-control scale.