Conforming fan maps on adaptive midpoint tiles

Each first-safe adaptive triangle has finitely many resolved vertices on its boundary. Coning successive boundary vertices to the positive barycentric center gives a locally finite family of parametrized triangles in the open subpolyhedron. This file constructs those maps before proving the global face-to-face intersection theorem.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPreconnected_subset_edgeSegment_of_avoids_vertices (J : PolygonalCircle) (A : Set Plane) (i : ZMod J.n) (hA : IsPreconnected A) (hcarrier : A ⊆ J.carrier) (hvertices : ∀ (j : ZMod J.n), J.vertex j ∉ A) (hmeet : (A ∩ J.edgeSegment i).Nonempty) : A ⊆ J.edgeSegment i

A preconnected subset of a polygonal circle which avoids every polygon vertex cannot pass from one open edge to another. Thus meeting one edge forces the whole set to lie in that edge. This is the elementary component fact used to compare hanging-edge subdivisions.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertex_mem_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) {p : K.realization} (hp : p ∈ K.adaptiveFanFaceVertices U hU f) : p ∈ K.adaptiveFaceCarrier U f.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.homeo_symm_mem_levelFaceCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) {p : K.realization} (hp : p ∈ K.levelFaceCarrier t) : (K.safeSubdivision n).homeo.symm p ∈ (K.safeSubdivision n).refined.faceCarrier ↑t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertexSource (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (p : ↥(K.adaptiveFanFaceVertices U hU f)) : (K.safeSubdivision f.fst.fst).refined.realization

The source point of a geometric fan vertex in the refined realization carrying its tile.

Equations

• K.adaptiveFanVertexSource U hU f p = (K.safeSubdivision f.fst.fst).homeo.symm ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertexSource_mem_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (p : ↥(K.adaptiveFanFaceVertices U hU f)) : K.adaptiveFanVertexSource U hU f p ∈ (K.safeSubdivision f.fst.fst).refined.faceCarrier ↑↑f.fst.snd

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanCenterVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↥(K.adaptiveFanFaceVertices U hU f)

The distinguished cone-center vertex of a fan triangle.

Equations

• K.adaptiveFanCenterVertex U hU f = ⟨K.adaptiveFaceCenter U f.fst, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFirstVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↥(K.adaptiveFanFaceVertices U hU f)

The first base vertex of a fan triangle.

Equations

• K.adaptiveFanFirstVertex U hU f = ⟨K.adaptiveEdgeIntervalFirst U hU f.fst f.snd.fst f.snd.snd, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSecondVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↥(K.adaptiveFanFaceVertices U hU f)

The second base vertex of a fan triangle.

Equations

• K.adaptiveFanSecondVertex U hU f = ⟨K.adaptiveEdgeIntervalSecond U hU f.fst f.snd.fst f.snd.snd, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertex_univ (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Finset.univ = {K.adaptiveFanCenterVertex U hU f, K.adaptiveFanFirstVertex U hU f, K.adaptiveFanSecondVertex U hU f}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanCenterVertex_ne_first (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanCenterVertex U hU f ≠ K.adaptiveFanFirstVertex U hU f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanCenterVertex_ne_second (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanCenterVertex U hU f ≠ K.adaptiveFanSecondVertex U hU f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFirstVertex_ne_second (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanFirstVertex U hU f ≠ K.adaptiveFanSecondVertex U hU f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanWeights_sum (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : ↑x (K.adaptiveFanCenterVertex U hU f) + ↑x (K.adaptiveFanFirstVertex U hU f) + ↑x (K.adaptiveFanSecondVertex U hU f) = 1

The three distinguished fan weights sum to one.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))

The canonical interval parametrization of the resolved base of a fan triangle.

Equations

• K.adaptiveFanBaseSimplexPath U hU f r = ⟨(AffineMap.lineMap ⇑(stdSimplex.vertex (K.adaptiveFanFirstVertex U hU f)) ⇑(stdSimplex.vertex (K.adaptiveFanSecondVertex U hU f))) ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_adaptiveFanBaseSimplexPath (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Continuous (K.adaptiveFanBaseSimplexPath U hU f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_apply_first (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : (K.adaptiveFanBaseSimplexPath U hU f r) (K.adaptiveFanFirstVertex U hU f) = 1 - ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_apply_second (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : (K.adaptiveFanBaseSimplexPath U hU f r) (K.adaptiveFanSecondVertex U hU f) = ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_apply_center (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : (K.adaptiveFanBaseSimplexPath U hU f r) (K.adaptiveFanCenterVertex U hU f) = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBaseParameter (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : ↑(Set.Icc 0 1)

The normalized parameter of the boundary point obtained by radially projecting a noncenter fan point away from the cone center.

Equations

• K.adaptiveFanNormalizedBaseParameter U hU f x hxCenter = ⟨↑x (K.adaptiveFanSecondVertex U hU f) / (1 - ↑x (K.adaptiveFanCenterVertex U hU f)), ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBasePoint (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))

The radial projection of a noncenter fan point to its resolved base interval.

Equations

• K.adaptiveFanNormalizedBasePoint U hU f x hxCenter = K.adaptiveFanBaseSimplexPath U hU f (K.adaptiveFanNormalizedBaseParameter U hU f x hxCenter)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBasePoint_apply_center (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : (K.adaptiveFanNormalizedBasePoint U hU f x hxCenter) (K.adaptiveFanCenterVertex U hU f) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBasePoint_apply_second (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : (K.adaptiveFanNormalizedBasePoint U hU f x hxCenter) (K.adaptiveFanSecondVertex U hU f) = ↑x (K.adaptiveFanSecondVertex U hU f) / (1 - ↑x (K.adaptiveFanCenterVertex U hU f))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBasePoint_apply_first (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : (K.adaptiveFanNormalizedBasePoint U hU f x hxCenter) (K.adaptiveFanFirstVertex U hU f) = ↑x (K.adaptiveFanFirstVertex U hU f) / (1 - ↑x (K.adaptiveFanCenterVertex U hU f))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Function.Injective (K.adaptiveFanBaseSimplexPath U hU f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : (K.safeSubdivision f.fst.fst).refined.realization

Barycentric combination of a fan face's three geometric vertices, formed in the faithful refined realization before transporting back to the original complex.

Equations

• K.adaptiveFanSourcePoint U hU f x = ⟨fun (v : (K.safeSubdivision f.fst.fst).refined.Vertex) => ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), x p * ↑(K.adaptiveFanVertexSource U hU f p) v, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_mem_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : K.adaptiveFanSourcePoint U hU f x ∈ (K.safeSubdivision f.fst.fst).refined.faceCarrier ↑↑f.fst.snd

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSimplexLineMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (r : ↑(Set.Icc 0 1)) : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))

The canonical line segment between two barycentric points of one fan face.

Equations

• K.adaptiveFanSimplexLineMap U hU f x y r = ⟨(AffineMap.lineMap ↑x ↑y) ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_simplexLineMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (r : ↑(Set.Icc 0 1)) : ↑(K.adaptiveFanSourcePoint U hU f (K.adaptiveFanSimplexLineMap U hU f x y r)) = (AffineMap.lineMap ↑(K.adaptiveFanSourcePoint U hU f x) ↑(K.adaptiveFanSourcePoint U hU f y)) ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_vertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (p : ↥(K.adaptiveFanFaceVertices U hU f)) : K.adaptiveFanSourcePoint U hU f (stdSimplex.vertex p) = K.adaptiveFanVertexSource U hU f p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.homeo_symm_apply_eq_zero_of_mem_levelFaceEdgeCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.levelFaceEdgeCarrier t i) {v : (K.safeSubdivision n).refined.Vertex} (hv : v ∉ ↑((K.safeSubdivision n).refined.faceEdge t i)) : ↑((K.safeSubdivision n).homeo.symm p) v = 0

Pulling an edge point back through the faithful subdivision gives zero in every coordinate outside that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertex_add_two_not_mem_faceEdge (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) : (K.safeSubdivision n).refined.faceVertex t (i + 2) ∉ ↑((K.safeSubdivision n).refined.faceEdge t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalFirst_source_opposite (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (j : K.AdaptiveEdgeInterval U hU t i) : ↑((K.safeSubdivision t.fst).homeo.symm (K.adaptiveEdgeIntervalFirst U hU t i j)) ((K.safeSubdivision t.fst).refined.faceVertex (↑t.snd) (i + 2)) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalSecond_source_opposite (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (j : K.AdaptiveEdgeInterval U hU t i) : ↑((K.safeSubdivision t.fst).homeo.symm (K.adaptiveEdgeIntervalSecond U hU t i j)) ((K.safeSubdivision t.fst).refined.faceVertex (↑t.snd) (i + 2)) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_source_apply (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : ↑((K.safeSubdivision t.fst).homeo.symm (K.adaptiveFaceCenter U t)) ((K.safeSubdivision t.fst).refined.faceVertex (↑t.snd) i) = 1 / 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_opposite (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : ↑(K.adaptiveFanSourcePoint U hU f x) ((K.safeSubdivision f.fst.fst).refined.faceVertex (↑f.fst.snd) (f.snd.fst + 2)) = ↑x (K.adaptiveFanCenterVertex U hU f) / 3

The coordinate opposite a fan triangle's base edge is exactly one third of its cone-center weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_faceVertex_lower_bound (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (i : ZMod 3) : ↑x (K.adaptiveFanCenterVertex U hU f) / 3 ≤ ↑(K.adaptiveFanSourcePoint U hU f x) ((K.safeSubdivision f.fst.fst).refined.faceVertex (↑f.fst.snd) i)

The cone-center contribution is a lower bound for every barycentric coordinate of a fan point in its ambient refined face. At the coordinate opposite the fan base this bound is an equality.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_eq_lineMap_normalizedBase (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU f) < 1) : ↑(K.adaptiveFanSourcePoint U hU f x) = (AffineMap.lineMap ↑(K.adaptiveFanVertexSource U hU f (K.adaptiveFanCenterVertex U hU f)) ↑(K.adaptiveFanSourcePoint U hU f (K.adaptiveFanNormalizedBasePoint U hU f x hxCenter))) (1 - ↑x (K.adaptiveFanCenterVertex U hU f))

A noncenter fan point is the affine combination of the cone center and its normalized radial projection to the base.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.eq_faceVertex_add_two_of_mem_face_not_mem_faceEdge (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) {v : (K.safeSubdivision n).refined.Vertex} (hvt : v ∈ ↑t) (hve : v ∉ ↑((K.safeSubdivision n).refined.faceEdge t i)) : v = (K.safeSubdivision n).refined.faceVertex t (i + 2)

A vertex of a triangular intrinsic face outside one cyclic edge is the opposite vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFace_faceEdge_injective (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : Function.Injective fun (i : ZMod 3) => (K.safeSubdivision n).refined.faceEdge t i

The three cyclic edges of a triangular level face are pairwise distinct.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalSecond_parameter_le_first_of_lt (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (a b : K.AdaptiveEdgeInterval U hU t i) (hab : ↑a < ↑b) : K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalSecond U hU t i a) ≤ K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalFirst U hU t i b)

Earlier resolved intervals on one ordered tile edge end no later than later intervals begin.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_mem_baseEdge_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : K.adaptiveFanSourcePoint U hU f x ∈ (K.safeSubdivision f.fst.fst).refined.faceCarrier ↑((K.safeSubdivision f.fst.fst).refined.faceEdge (↑f.fst.snd) f.snd.fst)

Zero cone-center weight places a fan source point on its resolved base edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseWeights_sum_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : x (K.adaptiveFanFirstVertex U hU f) + x (K.adaptiveFanSecondVertex U hU f) = 1

When the cone-center weight vanishes, the two ordered base weights sum to one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertexSource_val_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Function.Injective fun (p : ↥(K.adaptiveFanFaceVertices U hU f)) => ↑(K.adaptiveFanVertexSource U hU f p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.affineIndependent_adaptiveFanVertexSource_val (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : AffineIndependent ℝ fun (p : ↥(K.adaptiveFanFaceVertices U hU f)) => ↑(K.adaptiveFanVertexSource U hU f p)

The three pulled-back vertices of a fan face are affinely independent. The two boundary vertices lie in the affine coordinate hyperplane opposite their common edge, while the positive center does not.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.affineCombination_injective_of_affineIndependent {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] (source : ι → E) (hsource : AffineIndependent ℝ source) : Function.Injective fun (x : ↑(stdSimplex ℝ ι)) => (Finset.affineCombination ℝ Finset.univ source) ⇑x

The affine combination map is injective when its source points are affinely independent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.simplex_eq_of_weighted_sum_eq_of_affineIndependent {ι : Type u_1} {α : Type u_2} [Fintype ι] (source : ι → α → ℝ) (hsource : AffineIndependent ℝ source) {x y : ↑(stdSimplex ℝ ι)} (hxy : (fun (v : α) => ∑ p : ι, x p * source p v) = fun (v : α) => ∑ p : ι, y p * source p v) : x = y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_val (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : ↑(K.adaptiveFanSourcePoint U hU f x) = fun (v : (K.safeSubdivision f.fst.fst).refined.Vertex) => ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), x p * ↑(K.adaptiveFanVertexSource U hU f p) v

The coordinate function underlying an adaptive fan source point.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSimplex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Set (↥(K.adaptiveFanFaceVertices U hU f) → ℝ)

The standard simplex parametrizing one adaptive fan face.

Equations

• K.adaptiveFanSimplex U hU f = stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePointVal (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↑(K.adaptiveFanSimplex U hU f) → (K.safeSubdivision f.fst.fst).refined.Vertex → ℝ

The coordinate-valued source-point map used for injectivity.

Equations

• K.adaptiveFanSourcePointVal U hU f x = ↑(K.adaptiveFanSourcePoint U hU f x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_val_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Function.Injective (K.adaptiveFanSourcePointVal U hU f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↑(K.adaptiveFanSimplex U hU f) → ↑U

One parametrized fan triangle in the open subspace.

Equations

• K.adaptiveFanFaceMap U hU f x = ⟨(K.safeSubdivision f.fst.fst).homeo (K.adaptiveFanSourcePoint U hU f x), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_vertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (p : ↥(K.adaptiveFanFaceVertices U hU f)) : K.adaptiveFanFaceMap U hU f (stdSimplex.vertex p) = ⟨↑p, ⋯⟩

A fan parametrization sends each abstract vertex to its declared geometric point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Function.Injective (K.adaptiveFanFaceMap U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanCenterWeight_eq_of_faceMap_eq_of_tile_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y) : ↑x (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, a⟩⟩) = ↑y (K.adaptiveFanCenterVertex U hU ⟨t, ⟨j, b⟩⟩)

Within one adaptive tile, a geometric point determines its cone-center weight. This is the minimum-coordinate characterization of radial coordinates in a triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanNormalizedBaseFaceMap_eq_of_same_tile (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y) (hxCenter : ↑x (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, a⟩⟩) < 1) (hyCenter : ↑y (K.adaptiveFanCenterVertex U hU ⟨t, ⟨j, b⟩⟩) < 1) : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ (K.adaptiveFanNormalizedBasePoint U hU ⟨t, ⟨i, a⟩⟩ x hxCenter) = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ (K.adaptiveFanNormalizedBasePoint U hU ⟨t, ⟨j, b⟩⟩ y hyCenter)

After removing the common cone-center contribution, equal points in one tile have equal radial projections to the tile boundary. The shared tile is explicit to avoid dependent transport through the two interval types.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_adaptiveFanSourcePoint (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Continuous (K.adaptiveFanSourcePoint U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_adaptiveFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Continuous (K.adaptiveFanFaceMap U hU f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↑(Set.Icc 0 1) → ↑U

The geometric interval path along a resolved fan base.

Equations

• K.adaptiveFanBasePath U hU f = K.adaptiveFanFaceMap U hU f ∘ K.adaptiveFanBaseSimplexPath U hU f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_adaptiveFanBasePath (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Continuous (K.adaptiveFanBasePath U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Function.Injective (K.adaptiveFanBasePath U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSourcePoint_baseSimplexPath_val (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : ↑(K.adaptiveFanSourcePoint U hU f (K.adaptiveFanBaseSimplexPath U hU f r)) = (AffineMap.lineMap ↑(K.adaptiveFanVertexSource U hU f (K.adaptiveFanFirstVertex U hU f)) ↑(K.adaptiveFanVertexSource U hU f (K.adaptiveFanSecondVertex U hU f))) ↑r

In refined barycentric coordinates, the canonical fan-base path is the line segment between the two pulled-back endpoint vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_val_eq_lineMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : ↑↑(K.adaptiveFanBasePath U hU f r) = (AffineMap.lineMap ↑↑(K.adaptiveFanFirstVertex U hU f) ↑↑(K.adaptiveFanSecondVertex U hU f)) ↑r

Faithfulness of the iterated subdivision makes every geometric fan-base path the literal ambient affine segment between its two declared endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanBaseSimplexPath U hU f ⟨0, ⋯⟩ = stdSimplex.vertex (K.adaptiveFanFirstVertex U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_one (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanBaseSimplexPath U hU f ⟨1, ⋯⟩ = stdSimplex.vertex (K.adaptiveFanSecondVertex U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanBasePath U hU f ⟨0, ⋯⟩ = ⟨↑(K.adaptiveFanFirstVertex U hU f), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_one (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : K.adaptiveFanBasePath U hU f ⟨1, ⋯⟩ = ⟨↑(K.adaptiveFanSecondVertex U hU f), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_eq_of_secondWeight (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (r : ↑(Set.Icc 0 1)) (hr : ↑r = x (K.adaptiveFanSecondVertex U hU f)) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : K.adaptiveFanBaseSimplexPath U hU f r = x

A zero-center barycentric point is determined by its second base weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseSimplexPath_secondWeight (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : K.adaptiveFanBaseSimplexPath U hU f ⟨x (K.adaptiveFanSecondVertex U hU f), ⋯⟩ = x

Every zero-center barycentric point has its declared second base weight as the canonical base-path parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_mem_baseEdge (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) : ↑(K.adaptiveFanBasePath U hU f r) ∈ K.levelFaceEdgeCarrier (↑f.fst.snd) f.snd.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_adaptiveFanFaceMap_subset_tile (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Set.range (K.adaptiveFanFaceMap U hU f) ⊆ K.adaptiveFaceCarrierInOpen U f.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFacePlaneHomeomorph_mem_edge (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) {p : K.realization} (hpEdge : p ∈ K.levelFaceEdgeCarrier (↑t.snd) i) : ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨p, ⋯⟩) ∈ standardTriangleCircle.edgeSegment i

The adaptive face chart takes a transported cyclic edge to the matching standard edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFacePlaneHomeomorph_mem_edge_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.adaptiveFaceCarrier U t) : ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨p, hp⟩) ∈ standardTriangleCircle.edgeSegment i ↔ p ∈ K.levelFaceEdgeCarrier (↑t.snd) i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFacePlaneCenter_mem_interior (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨K.adaptiveFaceCenter U t, ⋯⟩) ∈ interior standardTrianglePlaneComplex.support

The adaptive tile barycenter is an interior point in the standard plane chart.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceSourceHomeomorph_val_eq_planeInverseAffine (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (p : K.AdaptiveClosedFace U t) : ↑↑((K.adaptiveFaceSourceHomeomorph U t) p) = ((K.safeSubdivision t.fst).refined.facePlaneInverseAffine ↑t.snd) ↑((K.adaptiveFacePlaneHomeomorph U t) p)

The inverse adaptive face chart is given by the explicit affine inverse in refined barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceSource_val_eq_lineMap_of_plane_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (p q : K.AdaptiveClosedFace U t) (r : ℝ) (hplane : ↑((K.adaptiveFacePlaneHomeomorph U t) p) = (AffineMap.lineMap ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨K.adaptiveFaceCenter U t, ⋯⟩) ↑((K.adaptiveFacePlaneHomeomorph U t) q)) r) : ↑((K.safeSubdivision t.fst).homeo.symm ↑p) = (AffineMap.lineMap ↑((K.safeSubdivision t.fst).homeo.symm (K.adaptiveFaceCenter U t)) ↑((K.safeSubdivision t.fst).homeo.symm ↑q)) r

A radial segment in the plane tile chart pulls back to the corresponding affine segment in the refined barycentric face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFacePlaneHomeomorph_mem_standardCircle_of_not_relInterior (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) {p : K.realization} (hp : p ∈ K.adaptiveFaceCarrier U t) (hpNot : p ∉ K.adaptiveFaceRelInterior U t) : ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨p, hp⟩) ∈ standardTriangleCircle.carrier

The adaptive face chart carries the relative boundary of a tile into the standard polygonal triangle boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_boundaryVertices_of_adaptiveFacePlaneHomeomorph_eq_vertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) {p : K.realization} (hp : p ∈ K.adaptiveFaceCarrier U t) (j : ZMod 3) (hpj : ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨p, hp⟩) = standardTriangleCircle.vertex j) : p ∈ K.boundaryVertices U hU t

A point which an adaptive face chart sends to a standard triangle corner is one of that tile's collected boundary marks.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_levelFaceEdgeParameter (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) : Continuous (K.levelFaceEdgeParameter t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_adaptiveFanFaceMap_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFaceMap U hU f x) = x (K.adaptiveFanFirstVertex U hU f) * K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFirstVertex U hU f) + x (K.adaptiveFanSecondVertex U hU f) * K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanSecondVertex U hU f)

Along a fan base, the ambient edge parameter is the convex combination of the two endpoint parameters with the two remaining simplex weights.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_adaptiveFanFaceMap_mem_Icc_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFaceMap U hU f x) ∈ Set.Icc (K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFirstVertex U hU f)) (K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanSecondVertex U hU f))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_adaptiveFanBasePath_eq_of_mem_levelFaceEdgeCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.levelFaceEdgeCarrier (↑t.snd) i) : ∃ (j : K.AdaptiveEdgeInterval U hU t i) (r : ↑(Set.Icc 0 1)), K.adaptiveFanBasePath U hU ⟨t, ⟨i, j⟩⟩ r = ⟨p, ⋯⟩

Every point of a resolved adaptive edge is represented by one of its consecutive fan-base paths.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_adaptiveFanFaceMap_eq_of_mem_adaptiveFaceCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) {p : K.realization} (hp : p ∈ K.adaptiveFaceCarrier U t) : ∃ (i : ZMod 3) (j : K.AdaptiveEdgeInterval U hU t i) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, j⟩⟩))), K.adaptiveFanFaceMap U hU ⟨t, ⟨i, j⟩⟩ x = ⟨p, ⋯⟩

The fan triangles over one adaptive tile cover the whole closed tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_adaptiveFanFaceMap_mem_Ioo_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU f)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU f)) : K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFaceMap U hU f x) ∈ Set.Ioo (K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanFirstVertex U hU f)) (K.levelFaceEdgeParameter (↑f.fst.snd) f.snd.fst ↑(K.adaptiveFanSecondVertex U hU f))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_not_mem_boundaryVertices_of_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU f)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU f)) : ↑(K.adaptiveFanFaceMap U hU f x) ∉ K.boundaryVertices U hU f.fst

A point in the relative interior of a resolved fan base is not one of the tile's collected boundary marks.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanSide_eq_of_faceMap_eq_of_same_tile_of_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y) (hxCenter : x (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, a⟩⟩) = 0) (hyCenter : y (K.adaptiveFanCenterVertex U hU ⟨t, ⟨j, b⟩⟩) = 0) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU ⟨t, ⟨i, a⟩⟩)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU ⟨t, ⟨i, a⟩⟩)) : 0 < y (K.adaptiveFanFirstVertex U hU ⟨t, ⟨j, b⟩⟩) → 0 < y (K.adaptiveFanSecondVertex U hU ⟨t, ⟨j, b⟩⟩) → i = j

Relative-interior points of resolved bases in one adaptive tile can agree only when the bases lie on the same cyclic tile edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanInterval_eq_of_faceMap_eq_of_same_edge_of_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (a b : K.AdaptiveEdgeInterval U hU t i) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨i, b⟩⟩ y) (hxCenter : x (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, a⟩⟩) = 0) (hyCenter : y (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, b⟩⟩) = 0) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU ⟨t, ⟨i, a⟩⟩)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU ⟨t, ⟨i, a⟩⟩)) (hyFirst : 0 < y (K.adaptiveFanFirstVertex U hU ⟨t, ⟨i, b⟩⟩)) (hySecond : 0 < y (K.adaptiveFanSecondVertex U hU ⟨t, ⟨i, b⟩⟩)) : a = b

Relative interiors of two consecutive-list intervals on the same tile edge are disjoint unless the interval indices are equal.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBasePath_not_mem_boundaryVertices_of_mem_Ioo (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (r : ↑(Set.Icc 0 1)) (hr : ↑r ∈ Set.Ioo 0 1) : ↑(K.adaptiveFanBasePath U hU f r) ∉ K.boundaryVertices U hU f.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_mem_relInterior_of_center_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : 0 < x (K.adaptiveFanCenterVertex U hU f)) : ↑(K.adaptiveFanFaceMap U hU f x) ∈ K.adaptiveFaceRelInterior U f.fst

Positive weight at the cone center places a fan point in the relative interior of its adaptive tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanCenterWeight_eq_zero_of_faceMap_eq_of_tile_ne (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) : x (K.adaptiveFanCenterVertex U hU f) = 0

A point common to fan triangles from distinct adaptive tiles has zero cone-center weight in the first triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanLaterBaseEdge_subset_earlierTile_of_faceMap_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) (hlevel : f.fst.fst ≤ g.fst.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) (hyFirst : 0 < y (K.adaptiveFanFirstVertex U hU g)) (hySecond : 0 < y (K.adaptiveFanSecondVertex U hU g)) : K.levelFaceEdgeCarrier (↑g.fst.snd) g.snd.fst ⊆ K.adaptiveFaceCarrier U f.fst

At a common nonvertex point, the base edge belonging to the later adaptive tile lies in the earlier tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanLaterBasePath_subset_earlierBaseEdge_of_faceMap_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) (hlevel : f.fst.fst ≤ g.fst.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) : 0 < x (K.adaptiveFanFirstVertex U hU f) → 0 < x (K.adaptiveFanSecondVertex U hU f) → ∀ (hyFirst : 0 < y (K.adaptiveFanFirstVertex U hU g)) (hySecond : 0 < y (K.adaptiveFanSecondVertex U hU g)) (r : ↑(Set.Icc 0 1)), ↑(K.adaptiveFanBasePath U hU g r) ∈ K.levelFaceEdgeCarrier (↑f.fst.snd) f.snd.fst

If interiors of two resolved fan bases meet and the second tile is no earlier in the adaptive hierarchy, then the entire second resolved interval lies in the first base edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseEndpoints_eq_or_swap_of_faceMap_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) (hlevel : f.fst.fst ≤ g.fst.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU f)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU f)) (hyFirst : 0 < y (K.adaptiveFanFirstVertex U hU g)) (hySecond : 0 < y (K.adaptiveFanSecondVertex U hU g)) : ↑(K.adaptiveFanFirstVertex U hU g) = ↑(K.adaptiveFanFirstVertex U hU f) ∧ ↑(K.adaptiveFanSecondVertex U hU g) = ↑(K.adaptiveFanSecondVertex U hU f) ∨ ↑(K.adaptiveFanFirstVertex U hU g) = ↑(K.adaptiveFanSecondVertex U hU f) ∧ ↑(K.adaptiveFanSecondVertex U hU g) = ↑(K.adaptiveFanFirstVertex U hU f)

Two resolved fan intervals whose relative interiors meet have the same geometric endpoints, possibly with opposite order.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.extendFaceCoordinates_adaptiveFanFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = Pi.single (↑(K.adaptiveFanCenterVertex U hU f)) (x (K.adaptiveFanCenterVertex U hU f)) + Pi.single (↑(K.adaptiveFanFirstVertex U hU f)) (x (K.adaptiveFanFirstVertex U hU f)) + Pi.single (↑(K.adaptiveFanSecondVertex U hU f)) (x (K.adaptiveFanSecondVertex U hU f))

Extended coordinates of a fan triangle are the sum of its three vertex-weight spikes.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.extendFaceCoordinates_eq_center_add_smul_normalizedBase (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) < 1) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = Pi.single (↑(K.adaptiveFanCenterVertex U hU f)) (x (K.adaptiveFanCenterVertex U hU f)) + (1 - x (K.adaptiveFanCenterVertex U hU f)) • extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) (K.adaptiveFanNormalizedBasePoint U hU f x hxCenter)

Radial projection to the fan base recovers the original global coordinates after restoring the cone-center weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanExtendedCoordinates_eq_of_faceMap_eq_of_tile_ne_of_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) (hlevel : f.fst.fst ≤ g.fst.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) (hxFirst : 0 < x (K.adaptiveFanFirstVertex U hU f)) (hxSecond : 0 < x (K.adaptiveFanSecondVertex U hU f)) (hyFirst : 0 < y (K.adaptiveFanFirstVertex U hU g)) (hySecond : 0 < y (K.adaptiveFanSecondVertex U hU g)) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) y

Cross-tile interior overlap is face-to-face not only as a set: the two affine parametrizations assign the same global barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanEndpointData_of_center_eq_zero_of_not_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) (hxNot : ¬(0 < x (K.adaptiveFanFirstVertex U hU f) ∧ 0 < x (K.adaptiveFanSecondVertex U hU f))) : ↑(K.adaptiveFanFaceMap U hU f x) = ↑(K.adaptiveFanFirstVertex U hU f) ∧ extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = Pi.single (↑(K.adaptiveFanFirstVertex U hU f)) 1 ∨ ↑(K.adaptiveFanFaceMap U hU f x) = ↑(K.adaptiveFanSecondVertex U hU f) ∧ extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = Pi.single (↑(K.adaptiveFanSecondVertex U hU f)) 1

A zero-center fan point which is not in the relative interior of its base is one of the two declared base vertices, both geometrically and in extended barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_mem_boundaryVertices_of_center_zero_of_not_base_weights_pos (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) (hxPos : ¬(0 < x (K.adaptiveFanFirstVertex U hU f) ∧ 0 < x (K.adaptiveFanSecondVertex U hU f))) : ↑(K.adaptiveFanFaceMap U hU f x) ∈ K.boundaryVertices U hU f.fst

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) : K.AdaptiveFanFace U hU

The resolved fan face assembled from a tile, edge, and interval.

Equations

• K.adaptiveFanFace U hU t i a = ⟨t, ⟨i, a⟩⟩

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceSimplex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) : Set (↥(K.adaptiveFanFaceVertices U hU (K.adaptiveFanFace U hU t i a)) → ℝ)

The simplex parametrizing a resolved fan face.

Equations

• K.adaptiveFanFaceSimplex U hU t i a = stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU (K.adaptiveFanFace U hU t i a))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanBaseWeights_pos_of_faceMap_eq_of_same_tile (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f g : K.AdaptiveFanFace U hU) (hfg : f.fst = g.fst) {x : ↑(K.adaptiveFanSimplex U hU f)} {y : ↑(K.adaptiveFanSimplex U hU g)} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) (hyCenter : y (K.adaptiveFanCenterVertex U hU g) = 0) (hxPos : 0 < x (K.adaptiveFanFirstVertex U hU f) ∧ 0 < x (K.adaptiveFanSecondVertex U hU f)) : 0 < y (K.adaptiveFanFirstVertex U hU g) ∧ 0 < y (K.adaptiveFanSecondVertex U hU g)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanExtendedCoordinates_eq_of_faceMap_eq_of_same_tile_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y) (hxCenter : x (K.adaptiveFanCenterVertex U hU ⟨t, ⟨i, a⟩⟩) = 0) (hyCenter : y (K.adaptiveFanCenterVertex U hU ⟨t, ⟨j, b⟩⟩) = 0) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩) y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanExtendedCoordinates_eq_of_faceMap_eq_of_same_tile (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩) y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanExtendedCoordinates_eq_of_faceMap_eq_of_tile_ne (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) y

Fan triangles belonging to distinct adaptive tiles assign the same global barycentric coordinates to every common geometric point. Interior points use the resolved-interval compatibility theorem; endpoint points are the common boundary marks collected by both tiles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanExtendedCoordinates_eq_of_faceMap_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) y

All adaptive fan faces use one global barycentric coordinate system on their overlaps.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_eq_of_extendedCoordinates_eq_of_same_tile (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i j : ZMod 3) (a : K.AdaptiveEdgeInterval U hU t i) (b : K.AdaptiveEdgeInterval U hU t j) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩))} (hxy : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨i, a⟩⟩) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU ⟨t, ⟨j, b⟩⟩) y) : K.adaptiveFanFaceMap U hU ⟨t, ⟨i, a⟩⟩ x = K.adaptiveFanFaceMap U hU ⟨t, ⟨j, b⟩⟩ y

In one adaptive tile, equal global coordinates have equal pulled-back barycentric sums and hence equal images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_not_mem_adaptiveFanFaceVertices_of_ne (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) : K.adaptiveFaceCenter U f.fst ∉ K.adaptiveFanFaceVertices U hU g

The center of one adaptive tile is not a fan vertex of a distinct tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_val_eq_weightedVertices_of_center_eq_zero (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) (hxCenter : x (K.adaptiveFanCenterVertex U hU f) = 0) : ↑↑(K.adaptiveFanFaceMap U hU f x) = fun (v : K.Vertex) => ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), x p * ↑↑p v

On a fan base, the parametrization is the literal weighted sum of its declared geometric vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_eq_of_extendedCoordinates_eq_of_tile_ne (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} (hfg : f.fst ≠ g.fst) {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) y) : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y

Across distinct adaptive tiles, equal global coordinates describe the same point on their common resolved boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_eq_of_extendedCoordinates_eq (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} {x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU g))} (hxy : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) y) : K.adaptiveFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU g y

Equal global barycentric coordinates are sufficient for equality of adaptive fan images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.locallyFinite_adaptiveFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : LocallyFinite fun (f : K.AdaptiveFanFace U hU) => Set.range (K.adaptiveFanFaceMap U hU f)

The fan-triangle family is locally finite because it has finitely many faces over each adaptive tile and the adaptive tile family is locally finite.