Finite conforming meshes on adaptive open-complex tiles

An adaptive tile is a closed face of an iterated midpoint subdivision, transported to the original intrinsic realization. Its faithful subdivision chart followed by facePlaneHomeomorph identifies it with the standard plane triangle. We mark every vertex of every touching adaptive tile on its boundary, refine the standard boundary graph at those marks, and cone that graph to an interior point. This file packages the resulting honest finite plane complex for one tile. The next layer proves that the transported tile complexes agree on overlaps and takes their locally finite union.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveClosedFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : Type

A transported adaptive tile, as a closed subspace of the original realization.

Equations

• K.AdaptiveClosedFace U t = { p : K.realization // p ∈ K.adaptiveFaceCarrier U t }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceHomeoSymm_mem_carrier (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.adaptiveFaceSourceHomeomorph (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.AdaptiveClosedFace U t ≃ₜ (K.safeSubdivision t.fst).refined.ClosedFace ↑t.snd

Remove the faithful subdivision transport from one adaptive tile.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFacePlaneHomeomorph (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.AdaptiveClosedFace U t ≃ₜ ↑standardTrianglePlaneComplex.support

The canonical standard-plane chart of an adaptive tile.

Equations

• K.adaptiveFacePlaneHomeomorph U t = (K.adaptiveFaceSourceHomeomorph U t).trans ((K.safeSubdivision t.fst).refined.facePlaneHomeomorph ↑t.snd)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.homeo_symm_mem_levelFaceEdgeCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.levelFaceEdgeCarrier t i) : (K.safeSubdivision n).homeo.symm p ∈ (K.safeSubdivision n).refined.faceCarrier ↑((K.safeSubdivision n).refined.faceEdge t i)

A point on an adaptive edge pulls back to the corresponding edge of the refined face.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveBoundaryVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : Type

The finite type of resolved boundary points of one adaptive tile.

Equations

• K.AdaptiveBoundaryVertex U hU t = ↥(K.boundaryVertices U hU t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryPlanePoint (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (p : K.AdaptiveBoundaryVertex U hU t) : Plane

A resolved boundary point in the standard plane chart of its adaptive tile.

Equations

• K.adaptiveBoundaryPlanePoint U hU t p = ↑((K.adaptiveFacePlaneHomeomorph U t) ⟨↑p, ⋯⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryPlanePoint_mem_standardOneSkeleton (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (p : K.AdaptiveBoundaryVertex U hU t) : K.adaptiveBoundaryPlanePoint U hU t p ∈ standardTrianglePlaneComplex.oneSkeleton.support

Every resolved boundary mark lies in the standard triangle's one-skeleton.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundarySubdivision (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : PlaneComplex

The standard boundary graph refined at every touching-tile vertex.

Equations

• K.adaptiveBoundarySubdivision U hU t = LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.oneSkeleton.markedEdgeSubdivision (K.adaptiveBoundaryPlanePoint U hU t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundarySubdivision_support (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : (K.adaptiveBoundarySubdivision U hU t).support = frontier standardTrianglePlaneComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryGraph (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : PlaneComplex

Remove any arrangement vertices not used by the refined boundary graph.

Equations

• K.adaptiveBoundaryGraph U hU t = (K.adaptiveBoundarySubdivision U hU t).used

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryGraph_support (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : (K.adaptiveBoundaryGraph U hU t).support = frontier standardTrianglePlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryGraph_isGraph (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (s : Finset (K.adaptiveBoundaryGraph U hU t).Vertex) : s ∈ (K.adaptiveBoundaryGraph U hU t).simplexes → s.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryGraph_vertex_mem_edge (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (v : (K.adaptiveBoundaryGraph U hU t).Vertex) : ∃ e ∈ (K.adaptiveBoundaryGraph U hU t).simplexes, v ∈ e ∧ e.card = 2

Exact support on the polygonal frontier rules out isolated used vertices: every boundary vertex belongs to a two-vertex face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveBoundaryGraph_isPureOne (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (s : Finset (K.adaptiveBoundaryGraph U hU t).Vertex) : s ∈ (K.adaptiveBoundaryGraph U hU t).simplexes → ∃ e ∈ (K.adaptiveBoundaryGraph U hU t).simplexes, s ⊆ e ∧ e.card = 2

Every simplex of the boundary graph is contained in an edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardAdaptiveConePoint : Plane

A fixed interior point of the standard triangle, used as every tile's cone vertex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardAdaptiveConePoint_mem_interior : standardAdaptiveConePoint ∈ interior standardTrianglePlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardAdaptiveConePoint_not_mem_boundaryGraph_range (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : standardAdaptiveConePoint ∉ Set.range (K.adaptiveBoundaryGraph U hU t).position

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveTilePlaneComplex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : PlaneComplex

The finite cone triangulation of one adaptive tile in standard plane coordinates.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveTilePlaneComplex_support (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : (K.adaptiveTilePlaneComplex U hU t).support = standardTrianglePlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveTilePlaneComplex_isPure2 (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : (K.adaptiveTilePlaneComplex U hU t).IsPure2

Coning a pure boundary graph produces a pure two-dimensional tile complex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveTileSupportHomeomorph (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : ↑(K.adaptiveTilePlaneComplex U hU t).support ≃ₜ K.AdaptiveClosedFace U t

Identify a tile cone's support with the corresponding adaptive closed face.

Equations

• K.adaptiveTileSupportHomeomorph U hU t = (Homeomorph.setCongr ⋯).trans (K.adaptiveFacePlaneHomeomorph U t).symm

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveTileSupportEmbed (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : ↑(K.adaptiveTilePlaneComplex U hU t).support → ↑U

Embed a tile cone support into the open subspace.

Equations

• K.adaptiveTileSupportEmbed U hU t p = ⟨↑((K.adaptiveTileSupportHomeomorph U hU t) p), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isEmbedding_adaptiveTileSupportEmbed (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : Topology.IsEmbedding (K.adaptiveTileSupportEmbed U hU t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_adaptiveTileSupportEmbed (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : Set.range (K.adaptiveTileSupportEmbed U hU t) = K.adaptiveFaceCarrierInOpen U t