The per-face comparison map for locally finite side preservation

This file discharges the side-preservation entry of the locally finite Chapter 6 replacement through the parametrization-independent interface cellwiseCompatibility_of_comparison.

The canonical replacement arcs only track the trimmed original edge curve (CentralPolygonalArc.curve_close), with the Path.trans parameter misaligned against the original face parametrization, so no same-parameter estimate can beat the mesh scale. The comparison map built here is the original face chart composed with a clamped radial reparametrization of the standard triangle (sidePiece, glued over three closed sectors in facewiseComparison): on each side the boundary parameter is redistributed so that the middle replacement range covers exactly the matched trim window, and the spoke ranges cover the two trimmed-off end pieces. All values lie in the original face image, so the cthickening membership required by cellwiseCompatibility_of_comparison is automatic.

The key quantitative input is exists_comparisonScale: the original face chart and its inverse are both uniformly continuous on the compact standard triangle, so once the vertex isolation disk and central tube of an edge are small in the image, the endpoints of each trimmed-off piece have close images, hence (inverse modulus) close standard parameters, hence (forward modulus) the whole reparametrized piece stays within a quarter separation radius of the vertex image. In particular the last-exit trim cannot make the trimmed-off original curve wander once the controls undercut the comparison scale — the wandering is bounded by the two-sided modulus, not by any mesh estimate.

Everything is arranged for a realization with shrunken approximation controls (withApproximationControls), which changes neither the embedded map nor the face separation radii; the resulting entry point is exists_controlled_polygonalReplacement_of_comparison.

Barycentric coordinates on the standard triangle

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.stdTriBasis : AffineBasis (Fin 3) ℝ Plane

The standard triangle vertices as an affine basis of the plane.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.stdTriBasis_apply (j : Fin 3) : stdTriBasis j = standardTriangleVertex j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_stdTriBasis : Set.range ⇑stdTriBasis = Set.range standardTriangleVertex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord (j : Fin 3) (x : Plane) : ℝ

The barycentric coordinate of a plane point with respect to a standard triangle vertex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord j x = (LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.stdTriBasis.coord j) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_triCoord (j : Fin 3) : Continuous (triCoord j)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_vertex_self (j : Fin 3) : triCoord j (standardTriangleVertex j) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_vertex_ne {j k : Fin 3} (hjk : j ≠ k) : triCoord j (standardTriangleVertex k) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sum_triCoord (x : Plane) : ∑ j : Fin 3, triCoord j x = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_lineMap (j : Fin 3) (a b : Plane) (t : ℝ) : triCoord j ((AffineMap.lineMap a b) t) = (AffineMap.lineMap (triCoord j a) (triCoord j b)) t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceRegion_eq_convexHull : standardFaceRegion = (convexHull ℝ) (Set.range standardTriangleVertex)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.convex_standardFaceRegion : Convex ℝ standardFaceRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_standardFaceRegion_iff {x : Plane} : x ∈ standardFaceRegion ↔ ∀ (j : Fin 3), 0 ≤ triCoord j x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.interior_standardFaceRegion : interior standardFaceRegion = {x : Plane | ∀ (j : Fin 3), 0 < triCoord j x}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_frontier_standardFaceRegion_iff {x : Plane} : x ∈ frontier standardFaceRegion ↔ x ∈ standardFaceRegion ∧ ∃ (j : Fin 3), triCoord j x = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_frontier_of_triCoord_eq_zero {x : Plane} (hx : x ∈ standardFaceRegion) {j : Fin 3} (hj : triCoord j x = 0) : x ∈ frontier standardFaceRegion

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCenter : Plane

The barycenter of the standard triangle.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCenter = Finset.centroid ℝ Finset.univ LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_triCenter (j : Fin 3) : triCoord j triCenter = 1 / 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCenter_mem_standardFaceRegion : triCenter ∈ standardFaceRegion

The clamped unit parameter

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp (t : ℝ) : ℝ

Clamp a real parameter into [0, 1].

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp t = max 0 (min 1 t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_unitClamp : Continuous unitClamp

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_nonneg (t : ℝ) : 0 ≤ unitClamp t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_le_one (t : ℝ) : unitClamp t ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_mem (t : ℝ) : unitClamp t ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : unitClamp t = t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_zero : unitClamp 0 = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_one : unitClamp 1 = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.lineMap_unitClamp_mem {s : Set Plane} (hs : Convex ℝ s) {a b : Plane} (ha : a ∈ s) (hb : b ∈ s) (t : ℝ) : (AffineMap.lineMap a b) (unitClamp t) ∈ s

A clamped line-map combination of two points of a convex set stays in the set.

Coordinates along one oriented standard side

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeFirstIndex_ne_secondIndex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : K.faceEdgeFirstIndex f i ≠ K.faceEdgeSecondIndex f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_secondIndex_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ℝ) : triCoord (K.faceEdgeSecondIndex f i) (K.faceEdgeSourcePoint f i r) = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_firstIndex_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ℝ) : triCoord (K.faceEdgeFirstIndex f i) (K.faceEdgeSourcePoint f i r) = 1 - r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_other_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) {j : Fin 3} (hj₁ : j ≠ K.faceEdgeFirstIndex f i) (hj₂ : j ≠ K.faceEdgeSecondIndex f i) (r : ℝ) : triCoord j (K.faceEdgeSourcePoint f i r) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : K.faceEdgeSourcePoint f i 0 = standardTriangleVertex (K.faceEdgeFirstIndex f i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : K.faceEdgeSourcePoint f i 1 = standardTriangleVertex (K.faceEdgeSecondIndex f i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_mem_region {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : K.faceEdgeSourcePoint f i r ∈ standardFaceRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_faceEdgeSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : Continuous (K.faceEdgeSourcePoint f i)

The original face chart along a source side

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceOriginalMap_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : faceOriginalMap G f (K.faceEdgeSourcePoint f i r) = G.chartEdgeCurve (K.faceEdge f i) r

The original face chart carries the oriented standard side to the charted edge curve with the identical parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceOriginalMap_injOn {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : Set.InjOn (faceOriginalMap G f) standardFaceRegion

The original face chart is injective on the closed standard triangle.

The comparison scale of a face

The face separation radius bounds the target tolerance; the two-sided uniform continuity of the original face chart converts image smallness into segment-image smallness. The resulting scale is what the shrunken approximation controls must undercut.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_comparisonScale {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : ∃ (eta : ℝ), 0 < eta ∧ eta ≤ faceVertexSeparationRadius G f / 8 ∧ ∀ x ∈ standardFaceRegion, ∀ y ∈ standardFaceRegion, dist (faceOriginalMap G f x) (faceOriginalMap G f y) ≤ 2 * eta → ∀ t ∈ Set.Icc 0 1, dist (faceOriginalMap G f ((AffineMap.lineMap x y) t)) (faceOriginalMap G f x) ≤ faceVertexSeparationRadius G f / 4

Two-sided modulus: once two standard points have images within twice this scale, the whole straight segment between them has image within a quarter separation radius of either end.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : ℝ

A canonical positive comparison scale for every face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale G f = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : 0 < comparisonScale G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : comparisonScale G f ≤ faceVertexSeparationRadius G f / 8

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale_segment {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) {x y : Plane} (hx : x ∈ standardFaceRegion) (hy : y ∈ standardFaceRegion) (hclose : dist (faceOriginalMap G f x) (faceOriginalMap G f y) ≤ 2 * comparisonScale G f) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : dist (faceOriginalMap G f ((AffineMap.lineMap x y) t)) (faceOriginalMap G f x) ≤ faceVertexSeparationRadius G f / 4

The standard index opposite a cyclic side

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex (i : ZMod 3) : Fin 3

The standard corner index not lying on cyclic side i.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex i = (ZMod.finEquiv 3).symm (i + 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.finEquiv_symm_injective : Function.Injective ⇑(ZMod.finEquiv 3).symm

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_index_cases {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : K.faceEdgeFirstIndex f i = (ZMod.finEquiv 3).symm i ∧ K.faceEdgeSecondIndex f i = (ZMod.finEquiv 3).symm (i + 1) ∨ K.faceEdgeFirstIndex f i = (ZMod.finEquiv 3).symm (i + 1) ∧ K.faceEdgeSecondIndex f i = (ZMod.finEquiv 3).symm i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_ne_symm (i : ZMod 3) : standardOppIndex i ≠ (ZMod.finEquiv 3).symm i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_ne_symm_succ (i : ZMod 3) : standardOppIndex i ≠ (ZMod.finEquiv 3).symm (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_ne_firstIndex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardOppIndex i ≠ K.faceEdgeFirstIndex f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_ne_secondIndex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardOppIndex i ≠ K.faceEdgeSecondIndex f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_oppIndex_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ℝ) : triCoord (standardOppIndex i) (K.faceEdgeSourcePoint f i r) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.triCoord_side_sum {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (x : Plane) : triCoord (K.faceEdgeFirstIndex f i) x + triCoord (K.faceEdgeSecondIndex f i) x + triCoord (standardOppIndex i) x = 1

The three coordinates named by one side enumerate the whole coordinate sum.

The matched trim parameters of one side

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideTrimLeft {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : ℝ

The original edge parameter matched to the polygonal arc's left exit.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideTrimRight {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : ℝ

The original edge parameter matched to the polygonal arc's right exit.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideTrim_left_le_right {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : sideTrimLeft G f i ≤ sideTrimRight G f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideTrimLeft_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : sideTrimLeft G f i ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideTrimRight_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : sideTrimRight G f i ∈ Set.Icc 0 1

The matched boundary parameter profile of one side

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideParamProfile {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) (u : ℝ) : ℝ

The piecewise-affine reparametrization of one side matched to the complete replacement path: the left spoke range covers the trimmed-off initial edge piece, the middle range covers the matched trim window, and the right spoke range covers the trimmed-off final piece.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_sideParamProfile {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : Continuous (sideParamProfile G f i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideParamProfile_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : sideParamProfile G f i 0 = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideParamProfile_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : sideParamProfile G f i 1 = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideParamProfile_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : sideParamProfile G f i u ∈ Set.Icc 0 1

The comparison piece adapted to one side

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideDepth (i : ZMod 3) (x : Plane) : ℝ

The barycentric depth of a point relative to one side: 1 on the side, 0 at the barycenter.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_sideDepth (i : ZMod 3) : Continuous (sideDepth i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideRawParam {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (x : Plane) : ℝ

The raw radial side parameter of a point: on the side itself it is the oriented affine side parameter; near the barycenter the clamped denominator keeps it continuous.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_sideRawParam {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : Continuous (sideRawParam f i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) (x : Plane) : Plane

The comparison piece adapted to side i: the original face chart evaluated on the clamped radial interpolation from the barycenter to the reparametrized side point.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_arg_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) (x : Plane) : (AffineMap.lineMap triCenter (K.faceEdgeSourcePoint f i (sideParamProfile G f i (unitClamp (sideRawParam f i x))))) (unitClamp (3 * sideDepth i x - 1)) ∈ standardFaceRegion

The domain point fed to the original chart by a side piece.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_mem_faceImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) (x : Plane) : sidePiece G f i x ∈ G.map '' PlaneGraphRealization.faceInSupport f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_sidePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) : Continuous (sidePiece G f i)

Evaluation of a side piece

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_of_nonpos {t : ℝ} (ht : t ≤ 0) : unitClamp t = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.unitClamp_of_one_le {t : ℝ} (ht : 1 ≤ t) : unitClamp t = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideRawParam_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ℝ) : sideRawParam f i (K.faceEdgeSourcePoint f i r) = r

On the side itself the raw parameter is the oriented affine side parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sideDepth_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ℝ) : sideDepth i (K.faceEdgeSourcePoint f i r) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : sidePiece G f i (K.faceEdgeSourcePoint f i r) = faceOriginalMap G f (K.faceEdgeSourcePoint f i (sideParamProfile G f i r))

A side piece evaluated on its own side is the reparametrized original boundary chart.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_of_firstCoord_eq {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) {x : Plane} (hcc : triCoord (K.faceEdgeFirstIndex f i) x = triCoord (standardOppIndex i) x) : sidePiece G f i x = faceOriginalMap G f ((AffineMap.lineMap triCenter (standardTriangleVertex (K.faceEdgeSecondIndex f i))) (unitClamp (3 * sideDepth i x - 1)))

The first-corner evaluation: whenever the first endpoint coordinate agrees with the opposite coordinate, the side piece interpolates toward the second corner.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_of_secondCoord_eq {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) {x : Plane} (hcc : triCoord (K.faceEdgeSecondIndex f i) x = triCoord (standardOppIndex i) x) : sidePiece G f i x = faceOriginalMap G f ((AffineMap.lineMap triCenter (standardTriangleVertex (K.faceEdgeFirstIndex f i))) (unitClamp (3 * sideDepth i x - 1)))

The second-corner evaluation: whenever the second endpoint coordinate agrees with the opposite coordinate, the side piece interpolates toward the first corner.

Agreement of adjacent side pieces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_succ (i : ZMod 3) : standardOppIndex (i + 1) = (ZMod.finEquiv 3).symm i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardOppIndex_succ_succ (i : ZMod 3) : standardOppIndex (i + 2) = (ZMod.finEquiv 3).symm (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.sidePiece_interface {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) {i i' : ZMod 3} (hne : i ≠ i') {x : Plane} (heq : triCoord (standardOppIndex i) x = triCoord (standardOppIndex i') x) : sidePiece G f i x = sidePiece G f i' x

Two side pieces agree wherever their opposite coordinates agree. This is the closed interface condition of the sector decomposition; no minimality is required.

The assembled facewise comparison map

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facewiseComparison {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (x : Plane) : Plane

The comparison map of one face: the three side pieces glued over the closed sectors on which the corresponding opposite coordinate is minimal.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facewiseComparison_mem_faceImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (x : Plane) : facewiseComparison G f x ∈ G.map '' PlaneGraphRealization.faceInSupport f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuousOn_facewiseComparison {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : ContinuousOn (facewiseComparison G f) standardFaceRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facewiseComparison_eq_sidePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) {x : Plane} (hx : x ∈ standardFaceRegion) (hzero : triCoord (standardOppIndex i) x = 0) : facewiseComparison G f x = sidePiece G f i x

On the closed sector of side i — in fact anywhere the opposite coordinate of side i vanishes — the comparison map is the side-i piece.

The boundary estimate

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.dist_completePath_comparison_lt {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (i : ZMod 3) (hiso₁ : G.vertexIsolationRadius (K.edgeFirst (K.faceEdge f i)) ≤ comparisonScale G f) (hiso₂ : G.vertexIsolationRadius (K.edgeSecond (K.faceEdge f i)) ≤ comparisonScale G f) (htube : G.centralTubeRadius (K.faceEdge f i) ≤ comparisonScale G f) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : dist ((G.replacementArc (K.faceEdge f i)).completePath ⟨r, hr⟩) (faceOriginalMap G f (K.faceEdgeSourcePoint f i (sideParamProfile G f i r))) < faceVertexSeparationRadius G f / 2

The complete replacement path of one side stays within half the face separation radius of the reparametrized original boundary chart, once the vertex isolation disks and the central tube are below the comparison scale.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facewiseComparison_close {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (hiso : ∀ (i : ZMod 3), G.vertexIsolationRadius (K.edgeFirst (K.faceEdge f i)) ≤ comparisonScale G f ∧ G.vertexIsolationRadius (K.edgeSecond (K.faceEdge f i)) ≤ comparisonScale G f) (htube : ∀ (i : ZMod 3), G.centralTubeRadius (K.faceEdge f i) ≤ comparisonScale G f) (q : StandardFaceBoundary) : dist (G.graphReplacementMap (faceBoundaryLift f q)) (facewiseComparison G f ↑q) < faceVertexSeparationRadius G f / 2

The graph replacement on one face boundary stays within half the face separation radius of the facewise comparison map.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.cellwiseCompatibility_of_comparisonScale {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hfaces : Function.Injective K.faceVertices) (hiso : ∀ (f : K.Face) (i : ZMod 3), G.vertexIsolationRadius (K.edgeFirst (K.faceEdge f i)) ≤ comparisonScale G f ∧ G.vertexIsolationRadius (K.edgeSecond (K.faceEdge f i)) ≤ comparisonScale G f) (htube : ∀ (f : K.Face) (i : ZMod 3), G.centralTubeRadius (K.faceEdge f i) ≤ comparisonScale G f) (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 complete cellwise compatibility package from comparison-scale-small approximation data. This is the honest side-preservation discharge for the locally finite Chapter 6 replacement: no same-parameter mesh estimate enters.

Choosing the approximation controls below every incident comparison scale

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexSupportPoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : ↑K.support

The support point of a global vertex.

Equations

• K.vertexSupportPoint v = ⟨K.vertexPoint v, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonVertexControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : ℝ

The minimum comparison scale among the finitely many faces through a vertex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonVertexControl_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : 0 < comparisonVertexControl G v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonVertexControl_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {v : K.Vertex} {f : K.Face} (hv : v ∈ K.faceVertices f) : comparisonVertexControl G v ≤ comparisonScale G f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonEdgeControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ℝ

The minimum comparison scale among the finitely many faces meeting an edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonEdgeControl_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : 0 < comparisonEdgeControl G e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonEdgeControl_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e : K.Edge} {f : K.Face} (hf : f ∈ K.edgeMeetingFaces e) : comparisonEdgeControl G e ≤ comparisonScale G f

Invariance of the comparison data under control shrinking

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexSeparationRadius_withApproximationControls {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (vc : K.Vertex → ℝ) (hvc : ∀ (v : K.Vertex), 0 < vc v) (ec : K.Edge → ℝ) (hec : ∀ (e : K.Edge), 0 < ec e) (f : K.Face) : faceVertexSeparationRadius (G.withApproximationControls vc hvc ec hec) f = faceVertexSeparationRadius G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.comparisonScale_withApproximationControls {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (vc : K.Vertex → ℝ) (hvc : ∀ (v : K.Vertex), 0 < vc v) (ec : K.Edge → ℝ) (hec : ∀ (e : K.Edge), 0 < ec e) (f : K.Face) : comparisonScale (G.withApproximationControls vc hvc ec hec) f = comparisonScale G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_controls_cellwiseCompatibility {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (hfaces : Function.Injective K.faceVertices) : ∃ (vc : K.Vertex → ℝ) (hvc : ∀ (v : K.Vertex), 0 < vc v) (ec : K.Edge → ℝ) (hec : ∀ (e : K.Edge), 0 < ec e), (∀ (f : K.Face), (facePolygonalCircle f).closedRegion ⊆ (G.withApproximationControls vc hvc ec hec).region) → (LocallyFinite fun (f : K.Face) => {q : ↑(G.withApproximationControls vc hvc ec hec).region | ↑q ∈ (facePolygonalCircle f).closedRegion}) → Nonempty (CellwiseCompatibility (G.withApproximationControls vc hvc ec hec))

The side-preservation discharge with shrunken controls. For every locally finite realization there are strictly positive replacement controls below which the complete cellwise compatibility package holds; the shrunken realization keeps the same map, region and separation radii.