Finite PL models for intrinsic graph replacements

This file turns the topological polygonal paths constructed in IntrinsicGraphApproximation into finite plane complexes. The first step isolates the portion of the middle PL segment model between its two last-exit parameters. Marking those parameters in the source arrangement makes the closed subsegment an exact finite subcomplex.

Piecewise-affine formulas on the intrinsic source edge

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_eq_left {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {x : K.realization} (hx : x ∈ K.faceCarrier ↑e) (ht : ↑(K.edgeParameter e x hx) ≤ 1 / 2) : K.edgeReplacementMap hcont hinj D C e x = (AffineMap.lineMap (h (K.edgeFirstPoint e)) (K.replacementArc hcont hinj D C e).leftEndpoint) (2 * ↑(K.edgeParameter e x hx))

On the first quarter-piece of Moise's concatenated parameterization, the intrinsic edge replacement is the affine spoke from the first vertex image to the left exit point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_eq_middle {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {x : K.realization} (hx : x ∈ K.faceCarrier ↑e) (ht0 : 1 / 2 ≤ ↑(K.edgeParameter e x hx)) (ht1 : ↑(K.edgeParameter e x hx) ≤ 3 / 4) : K.edgeReplacementMap hcont hinj D C e x = (K.replacementArc hcont hinj D C e).parameterization.map (planePoint (↑(K.replacementArc hcont hinj D C e).data.resolvedWalk.length * ((K.replacementArc hcont hinj D C e).exitData.left + ((K.replacementArc hcont hinj D C e).exitData.right - (K.replacementArc hcont hinj D C e).exitData.left) * (4 * ↑(K.edgeParameter e x hx) - 2))) 0)

On the middle quarter-piece, the intrinsic edge replacement is the finite PL segment model evaluated at an affine function of the barycentric edge parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_eq_right {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {x : K.realization} (hx : x ∈ K.faceCarrier ↑e) (ht : 3 / 4 ≤ ↑(K.edgeParameter e x hx)) : K.edgeReplacementMap hcont hinj D C e x = (AffineMap.lineMap (K.replacementArc hcont hinj D C e).rightEndpoint (h (K.edgeSecondPoint e))) (4 * ↑(K.edgeParameter e x hx) - 3)

On the final quarter-piece of Moise's concatenated parameterization, the intrinsic edge replacement is the affine spoke from the right exit point to the second vertex image.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCoordinateAffine (K : IntrinsicTwoComplex) (e : K.Edge) : (K.Vertex → ℝ) →ᵃ[ℝ] ℝ

The second barycentric coordinate of an intrinsic edge, as an ambient affine map.

Equations

• K.edgeCoordinateAffine e = (LinearMap.proj (K.edgeSecond e)).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCoordinateAffine_apply (K : IntrinsicTwoComplex) (e : K.Edge) (x : K.Vertex → ℝ) : (K.edgeCoordinateAffine e) x = x (K.edgeSecond e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleSourceScalarMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : (K.Vertex → ℝ) →ᵃ[ℝ] ℝ

The affine scalar which carries the middle quarter of an intrinsic source edge to the horizontal source interval of its finite polygonal model.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleSourceMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : (K.Vertex → ℝ) →ᵃ[ℝ] Plane

The plane-valued affine middle-source map.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleSourceMap_apply {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (x : K.Vertex → ℝ) : (edgeMiddleSourceMap A) x = planePoint (↑A.data.resolvedWalk.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * x (K.edgeSecond e) - 2))) 0

The finite source breakpoint family

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.rawEdgeMiddleBreakpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.parameterization.source.Vertex) : ℝ

The source-edge parameter corresponding to one vertex of the finite middle segment model, before clamping to the middle quarter.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleBreakpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.parameterization.source.Vertex) : ℝ

Clamp a middle-model breakpoint to the parameter interval on which the middle formula is used.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleBreakpoint_mem {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.parameterization.source.Vertex) : edgeMiddleBreakpoint A v ∈ Set.Icc (1 / 2) (3 / 4)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleBreakpoint_eq_raw_of_mem {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length ≤ A.exitData.right) : edgeMiddleBreakpoint A v = rawEdgeMiddleBreakpoint A v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeMiddleSourceScalar_breakpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length ≤ A.exitData.right) : ↑A.data.resolvedWalk.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * edgeMiddleBreakpoint A v - 2)) = (A.parameterization.source.position v).ofLp 0

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeBreakpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Type

All source breakpoints of one intrinsic replacement edge: the two spoke joins and every vertex of the finite middle PL model.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeBreakpoint A = Option (Option A.parameterization.source.Vertex)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeBreakpointParameter {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (b : EdgeBreakpoint A) : ℝ

The edgeBreakpointParameter declaration.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeBreakpointParameter A none = 1 / 2
• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeBreakpointParameter A (some none) = 3 / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeBreakpointParameter_mem {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (b : EdgeBreakpoint A) : edgeBreakpointParameter A b ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_affineOn_left {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {E : Set K.realization} (hE : E ⊆ K.faceCarrier ↑e) (hle : ∀ x ∈ E, ↑x (K.edgeSecond e) ≤ 1 / 2) : K.IsAffineOnSet (K.graphReplacementMap hcont hinj D C) E

The simultaneous intrinsic graph replacement is affine on any source subset contained in the first spoke piece of one edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_affineOn_right {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {E : Set K.realization} (hE : E ⊆ K.faceCarrier ↑e) (hge : ∀ x ∈ E, 3 / 4 ≤ ↑x (K.edgeSecond e)) : K.IsAffineOnSet (K.graphReplacementMap hcont hinj D C) E

The simultaneous intrinsic graph replacement is affine on any source subset contained in the final spoke piece of one edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_affineOn_middle {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} {E : Set K.realization} (hE : E ⊆ K.faceCarrier ↑e) (hmid0 : ∀ x ∈ E, 1 / 2 ≤ ↑x (K.edgeSecond e)) (hmid1 : ∀ x ∈ E, ↑x (K.edgeSecond e) ≤ 3 / 4) (hsource : ∃ s ∈ (K.replacementArc hcont hinj D C e).parameterization.source.simplexes, Set.MapsTo (fun (x : K.realization) => (edgeMiddleSourceMap (K.replacementArc hcont hinj D C e)) ↑x) E ((K.replacementArc hcont hinj D C e).parameterization.source.cellCarrier s)) : K.IsAffineOnSet (K.graphReplacementMap hcont hinj D C) E

A middle source piece is affine as soon as its affine source image lies in one face of the finite segment model. The named intrinsic edge subdivision will provide exactly this hypothesis on each of its middle faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_image_faceCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} : K.edgeReplacementMap hcont hinj D C e '' K.faceCarrier ↑e = (K.replacementArc hcont hinj D C e).completeCarrier

The edgewise replacement map has exactly the complete polygonal replacement carrier as its image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_image_faceCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} : K.graphReplacementMap hcont hinj D C '' K.faceCarrier ↑e = (K.replacementArc hcont hinj D C e).completeCarrier

The simultaneous graph replacement has the same exact edge image as the edgewise formula.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSourcePoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Plane

The leftSourcePoint declaration.

Equations

• A.leftSourcePoint = LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint (↑A.data.resolvedWalk.length * A.exitData.left) 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightSourcePoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Plane

The rightSourcePoint declaration.

Equations

• A.rightSourcePoint = LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint (↑A.data.resolvedWalk.length * A.exitData.right) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSourcePoint_mem_source {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftSourcePoint ∈ A.parameterization.source.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightSourcePoint_mem_source {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.rightSourcePoint ∈ A.parameterization.source.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSourcePoint_ne_rightSourcePoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftSourcePoint ≠ A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSourcePoint_zero_lt_right {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftSourcePoint.ofLp 0 < A.rightSourcePoint.ofLp 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimMark {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Fin 2 → Plane

The two source points at which the middle polygonal path exits the endpoint disks.

Equations

• A.trimMark ⟨0, isLt⟩ = A.leftSourcePoint
• A.trimMark ⟨1, isLt⟩ = A.rightSourcePoint

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimMark_zero {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimMark 0 = A.leftSourcePoint

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimMark_one {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimMark 1 = A.rightSourcePoint

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimSubdivision {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : PlaneComplex

The source graph refined at both last-exit points.

Equations

• A.trimSubdivision = A.parameterization.source.markedEdgeSubdivision A.trimMark

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimSource {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : PlaneComplex

The exact closed source interval between the two exits.

Equations

• A.trimSource = A.trimSubdivision.restrictedTo (segment ℝ A.leftSourcePoint A.rightSourcePoint)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimSource_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimSource.support = segment ℝ A.leftSourcePoint A.rightSourcePoint

Marking the two exits makes the interval between them an exact finite subcomplex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : PlaneComplex

Remove the unused vertices retained by restrictedTo.

Equations

• A.trimActive = A.trimSource.active

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimActive.support = segment ℝ A.leftSourcePoint A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive_vertex_mem_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : A.trimActive.Vertex) : A.trimActive.position v ∈ A.trimActive.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive_card_le_two {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (s : Finset A.trimActive.Vertex) : s ∈ A.trimActive.simplexes → s.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive_map_injective {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set.InjOn A.parameterization.map A.trimActive.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimActive_map_affine {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (s : Finset A.trimActive.Vertex) : s ∈ A.trimActive.simplexes → IsAffineOn A.parameterization.map (A.trimActive.cellCarrier s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimTarget {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : PlaneComplex

The finite target graph carried by the trimmed polygonal middle.

Equations

• A.trimTarget = A.trimActive.mapGraph A.parameterization.map ⋯ ⋯ ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.map_image_sourceSegment {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.parameterization.map '' segment ℝ A.leftSourcePoint A.rightSourcePoint = A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimTarget_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.support = A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftTrimVertex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.Vertex

The leftTrimVertex declaration.

Equations

• A.leftTrimVertex = Classical.choose ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightTrimVertex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.Vertex

The rightTrimVertex declaration.

Equations

• A.rightTrimVertex = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftTrimVertex_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : {A.leftTrimVertex} ∈ A.trimTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightTrimVertex_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : {A.rightTrimVertex} ∈ A.trimTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftTrimVertex_sourcePosition {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimActive.position A.leftTrimVertex = A.leftSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightTrimVertex_sourcePosition {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimActive.position A.rightTrimVertex = A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.map_leftSourcePoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.parameterization.map A.leftSourcePoint = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.map_rightSourcePoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.parameterization.map A.rightSourcePoint = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimTarget_position_left {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.position A.leftTrimVertex = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimTarget_position_right {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.position A.rightTrimVertex = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.isPreconnected_trimTarget_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : IsPreconnected A.trimTarget.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.middleVertexPath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimTarget.vertexGraph.Path A.leftTrimVertex A.rightTrimVertex

A simple finite graph path traversing the trimmed target arc.

Equations

• A.middleVertexPath = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : BrokenLineData Set.univ

An auxiliary broken line which lists the two spokes and every edge and vertex of the trimmed target. Connector segments between listed pieces are harmless: completeTarget below retains only arrangement faces contained in the actual replacement carrier.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain_vertex_zero {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeChain.vertex 0 = h (K.edgeFirstPoint e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain_vertex_one {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeChain.vertex ⟨1, ⋯⟩ = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain_vertex_middle {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (i : Fin (A.trimTarget.edgeChain.n + 1)) : A.completeChain.vertex ⟨↑i + 2, ⋯⟩ = A.trimTarget.edgeChain.vertex i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain_vertex_rightEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeChain.vertex ⟨A.trimTarget.edgeChain.n + 3, ⋯⟩ = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeChain_vertex_finish {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeChain.vertex (Fin.last A.completeChain.n) = h (K.edgeSecondPoint e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeTarget {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : PlaneComplex

The finite plane complex carried by one complete replacement edge.

Equations

• A.completeTarget = A.completeChain.arrangementMesh.toPlaneComplex.restrictedTo A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.exists_completeTarget_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) {x : Plane} (hx : x ∈ A.completeCarrier) : ∃ s ∈ A.completeChain.arrangementMesh.toPlaneComplex.simplexes, x ∈ A.completeChain.arrangementMesh.toPlaneComplex.cellCarrier s ∧ A.completeChain.arrangementMesh.toPlaneComplex.cellCarrier s ⊆ A.completeCarrier ∧ s.card ≤ 2

Every point of a complete replacement edge lies in a one-dimensional arrangement face subordinate to that edge. The cardinality conclusion is what permits several replacement edges to be resolved in one common line arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeTarget_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.support = A.completeCarrier

Exact finite-complex realization of the complete replacement edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeCarrier_subset_segmentCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeCarrier ⊆ A.completeChain.segmentCarrier

Every point of a complete replacement edge lies on one of the finitely listed segments of its auxiliary chain. This is the coverage input used when the three edge chains of a face are placed into one common line arrangement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeStartVertex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.Vertex

The first intrinsic endpoint as a vertex of the finite complete-edge complex.

Equations

• A.completeStartVertex = A.completeChain.arrangementVertex 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeFinishVertex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.Vertex

The second intrinsic endpoint as a vertex of the finite complete-edge complex.

Equations

• A.completeFinishVertex = A.completeChain.arrangementVertex (Fin.last A.completeChain.n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeTarget_position_start {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.position A.completeStartVertex = h (K.edgeFirstPoint e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeTarget_position_finish {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.position A.completeFinishVertex = h (K.edgeSecondPoint e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeStartVertex_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : {A.completeStartVertex} ∈ A.completeTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeFinishVertex_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : {A.completeFinishVertex} ∈ A.completeTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.isPreconnected_completeTarget_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : IsPreconnected A.completeTarget.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeVertexPath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeTarget.vertexGraph.Path A.completeStartVertex A.completeFinishVertex

A simple finite graph path whose geometric carrier runs from one intrinsic endpoint to the other inside the complete replacement edge.

Equations

• A.completeVertexPath = Classical.choice ⋯