Controlled locally finite PL replacement

This file packages the completed cellwise part of Moise Chapter 6, Theorem 3. The graph-level construction supplies quantitative face control and separation. Polygonal Schoenflies then fills every face, and local finiteness glues the fillings into a homeomorphism of supports.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.ControlsStayInRegion {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) : Prop

The closed metric controls used for a replacement are contained in the permitted open region.

Equations

• G.ControlsStayInRegion phi = ∀ (p : ↑K.support), Metric.closedBall (G.map p) (phi p) ⊆ G.region

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.UniformFrontierControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) : Prop

A global bound and a frontier-relative bound sufficient to control a locally finite family of polygonal face fillings.

Equations

• G.UniformFrontierControl phi = ((∀ (p : ↑K.support), phi p ≤ 1) ∧ (G.regionᶜ.Nonempty → ∀ (p : ↑K.support), phi p ≤ Metric.infDist (G.map p) G.regionᶜ / 4))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.closedRegions_mem_region_of_uniformFrontierControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hfrontier : G.UniformFrontierControl phi) (f : K.Face) : (facePolygonalCircle f).closedRegion ⊆ G.region

Frontier control keeps each selected polygonal disk inside the permitted open region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.locallyFinite_closedRegions_of_uniformFrontierControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hfrontier : G.UniformFrontierControl phi) : LocallyFinite fun (f : K.Face) => {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}

The filled polygonal disks of a uniformly frontier-controlled replacement are locally finite in the open perturbation region. The proof confines any disk meeting a small ball to an original face meeting a fixed compact ball, then uses relative closed-embedding transport.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_graphReplacementMap_subset_of_convex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {C : Set Plane} (hC : Convex ℝ C) (hmap : Set.range G.map ⊆ C) : Set.range G.graphReplacementMap ⊆ C

Convex target regions are preserved by the simultaneous polygonal replacement of the one-skeleton. The construction chooses each central broken line in the convex hull of its original embedded edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_graphReplacementMap_subset_halfPlane {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hmap : Set.range G.map ⊆ HalfPlaneSet) : Set.range G.graphReplacementMap ⊆ HalfPlaneSet

A source realization in the model half-plane has a replacement graph in that half-plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.mem_convexHull_edgeImage_coordZero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e : K.Edge} (A : G.CentralPolygonalArc e) (hmap : G.edgeImage e ⊆ HalfPlaneSet) {x : Plane} (hx : x ∈ A.completeCarrier) (hxZero : x.ofLp 0 = 0) : x ∈ (convexHull ℝ) (G.edgeImage e ∩ {p : Plane | p.ofLp 0 = 0})

A zero-normal point of a complete replacement arc is supported by zero-normal points of the old embedded edge. This is the exact supporting-face statement behind boundary preservation; mere half-plane containment would only give one implication.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_eq_graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) (p : ↑PlaneGraphRealization.oneSkeletonInSupport) : ↑↑(polygonalReplacementMap H ↑p) = G.graphReplacementMap p

On the source one-skeleton, the assembled cellwise replacement is exactly the previously constructed global graph replacement.

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

The source zero-normal locus already lies in the source one-skeleton.

Equations

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

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

On every source triangle, the supporting-line locus is an exposed face with at most two vertices. This is the intrinsic condition which excludes a boundary chord: the zero locus in a triangle is either empty, a vertex, or an entire edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sourceCoordZeroCarriedByOneSkeleton_of_facewiseCoordZeroExposed {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hface : G.FacewiseCoordZeroExposed) : G.SourceCoordZeroCarriedByOneSkeleton

A facewise exposed zero locus is necessarily carried by the source one-skeleton.

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

The graph replacement preserves the zero-normal locus pointwise on its source graph.

Equations

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

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

The exact edgewise alternatives needed at a supporting boundary line. On each old edge, the zero-normal locus is either the whole image, one incident vertex, or empty. In particular, this rules out an interior edge whose two endpoints lie on the model boundary while its interior does not: an arbitrary convex-hull polygonalization could otherwise create a spurious boundary segment.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCoordZeroTrichotomy_of_facewiseCoordZeroExposed {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hface : G.FacewiseCoordZeroExposed) : G.EdgeCoordZeroTrichotomy

A facewise exposed zero locus gives the edgewise full/singleton/empty alternatives.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacementPreservesCoordZero_of_edgeCoordZeroTrichotomy {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hhalf : Set.range G.map ⊆ HalfPlaneSet) (hedges : G.EdgeCoordZeroTrichotomy) : G.GraphReplacementPreservesCoordZero

The edgewise zero-locus trichotomy makes the simultaneous graph replacement preserve the supporting boundary line exactly. The forward direction uses the supporting-face theorem for the replacement convex hull; the reverse direction uses vertex fixing in the singleton case.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.graphReplacementPreservesCoordZero_of_facewiseCoordZeroExposed {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hhalf : Set.range G.map ⊆ HalfPlaneSet) (hface : G.FacewiseCoordZeroExposed) : G.GraphReplacementPreservesCoordZero

The facewise exposed-face invariant is the single source-side hypothesis needed for exact zero-coordinate preservation by the simultaneous graph replacement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph_coordZero_iff {S : Type u_1} [TopologicalSpace S] [T2Space S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) (hhalf : Set.range G.map ⊆ HalfPlaneSet) (hsource : G.SourceCoordZeroCarriedByOneSkeleton) (hgraph : G.GraphReplacementPreservesCoordZero) (p : ↑K.support) : (↑↑((polygonalReplacementHomeomorph H) p)).ofLp 0 = 0 ↔ (G.map p).ofLp 0 = 0

Once exact zero-coordinate preservation is known on the replacement graph, the polygonal Schoenflies fillings preserve it on every filled face. No filled-face interior can reach the supporting line, so the two-dimensional statement reduces completely to the one-skeleton.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph_coordZero_iff_of_facewiseCoordZeroExposed {S : Type u_1} [TopologicalSpace S] [T2Space S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) (hhalf : Set.range G.map ⊆ HalfPlaneSet) (hface : G.FacewiseCoordZeroExposed) (p : ↑K.support) : (↑↑((polygonalReplacementHomeomorph H) p)).ofLp 0 = 0 ↔ (G.map p).ofLp 0 = 0

Exact preservation on filled faces, stated directly from the facewise exposed-face invariant.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_mem_region {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) {phi : ↑K.support → ℝ} : FaceBoundariesControlled G phi → G.ControlsStayInRegion phi → ∀ (p : ↑K.support), ↑↑(polygonalReplacementMap H p) ∈ G.region

A controlled compatible cellwise replacement lands in the permitted perturbation region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_controlled_polygonalReplacement {S : Type u_1} [TopologicalSpace S] [T2Space 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}) : ∃ (H : CellwiseCompatibility G), ∀ (p : ↑K.support), dist (↑↑((polygonalReplacementHomeomorph H) p)) (G.map p) ≤ phi p

The full locally finite Chapter 6 output from its quantitative graph hypotheses.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_controlled_polygonalReplacement_of_facewise_close {S : Type u_1} [TopologicalSpace S] [T2Space S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hfaces : Function.Injective K.faceVertices) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hfrontier : G.UniformFrontierControl phi) (hclose : FaceBoundariesClose G (faceVertexSeparationRadius G)) : ∃ (H : CellwiseCompatibility G), ∀ (p : ↑K.support), dist (↑↑((polygonalReplacementHomeomorph H) p)) (G.map p) ≤ phi p

The complete locally finite Chapter 6 output in Moise's facewise side-control form. Uniform frontier control supplies target containment and local finiteness automatically.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_controlled_polygonalReplacement_of_edgeMesh {S : Type u_1} [TopologicalSpace S] [T2Space S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hfaces : Function.Injective K.faceVertices) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hfrontier : G.UniformFrontierControl phi) (hmesh : ∀ (e : K.Edge), 2 * Metric.diam (G.edgeImage e) < edgeFaceSeparationRadius G e) : ∃ (H : CellwiseCompatibility G), ∀ (p : ↑K.support), dist (↑↑((polygonalReplacementHomeomorph H) p)) (G.map p) ≤ phi p

The Chapter 6 cellwise approximation from the exact edge-mesh condition supplied by an internal edge subdivision. No independent side hypothesis remains: the incident-face minimum turns edgewise diameter control into the required facewise closeness.

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

If the replacement graph lies in the closed right half-plane, every selected polygonal face disk lies there too.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementComplex_support_subset_halfPlane {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) (hgraph : Set.range G.graphReplacementMap ⊆ HalfPlaneSet) : Subtype.val '' (polygonalReplacementComplex H).support ⊆ HalfPlaneSet

Consequently the entire assembled locally finite replacement complex stays in the closed right half-plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph_mem_halfPlane {S : Type u_1} [TopologicalSpace S] [T2Space S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (H : CellwiseCompatibility G) (hgraph : Set.range G.graphReplacementMap ⊆ HalfPlaneSet) (p : ↑K.support) : ↑↑((polygonalReplacementHomeomorph H) p) ∈ HalfPlaneSet

Pointwise half-plane preservation for the assembled replacement homeomorphism.