Adaptive midpoint tiles in an open polyhedron

Select the first triangle in each midpoint-descendant chain whose complete carrier lies in an open set. These triangles cover the open set and form a locally finite hierarchical tiling. Their edges need not yet form a conforming simplicial complex: a coarse edge may contain several edges of finer adjacent tiles. The next layer resolves precisely those hanging vertices.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace (K : IntrinsicTwoComplex) (n : ℕ) : Type

A maximal face at midpoint level n.

Equations

• K.LevelFace n = (K.safeSubdivision n).refined.Face

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : Set K.realization

The carrier of a level face, transported back to the original realization.

Equations

• K.levelFaceCarrier t = ⇑(K.safeSubdivision n).homeo '' (K.safeSubdivision n).refined.faceCarrier ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isCompact_levelFaceCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : IsCompact (K.levelFaceCarrier t)

class LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveSafety (K : IntrinsicTwoComplex) (U : Set K.realization) : Type

A hereditary rule selecting sufficiently small level faces inside U.

The default rule is simple containment in U. A stricter local rule can be installed as a local instance, allowing the conforming adaptive fan construction to be reused for open-cover, oscillation, separation, and boundary-control requirements.

• safe {n : ℕ} : K.LevelFace n → Prop

  The safe declaration.

• carrier_subset {n : ℕ} {t : K.LevelFace n} : safe U t → K.levelFaceCarrier t ⊆ U
• hereditary {n m : ℕ} {s : K.LevelFace n} {t : K.LevelFace m} : K.levelFaceCarrier t ⊆ K.levelFaceCarrier s → safe U s → safe U t

@[instance_reducible, instance 100]

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.defaultAdaptiveSafety (K : IntrinsicTwoComplex) (U : Set K.realization) : K.AdaptiveSafety U

The original safety rule: a face is safe exactly when its carrier lies in U. Its low priority lets a quantitative chart-control rule override it locally without changing any of the adaptive combinatorial APIs.

Equations

• K.defaultAdaptiveSafety U = { safe := fun {n : ℕ} (t : K.LevelFace n) => K.levelFaceCarrier t ⊆ U, carrier_subset := ⋯, hereditary := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsSafe (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n : ℕ} (t : K.LevelFace n) : Prop

The active safety predicate.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsSafe K U t = LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveSafety.safe U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFace_isSafe_iff (K : IntrinsicTwoComplex) (U : Set K.realization) {n : ℕ} (t : K.LevelFace n) : LevelFace.IsSafe K U t ↔ ↑t ∈ K.safeFaces U n

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelParentFace (K : IntrinsicTwoComplex) (n : ℕ) (t : K.LevelFace (n + 1)) : K.LevelFace n

The chosen parent one level above an iterated midpoint face.

Equations

• K.levelParentFace n t = id (fun (t : (K.safeSubdivision n).refined.midpointComplex.Face) => (K.safeSubdivision n).refined.midpointParentFace t) t

class LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveSafety.IsAdmissible (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] : Prop

Local attainability hypotheses for an adaptive safety rule. The first field guarantees coverage. The second says that sufficiently fine children meeting a fixed neighborhood have a safe parent; this is exactly the condition that makes first-safe faces locally finite.

• exists_safe : IsOpen U → ∀ {p : K.realization}, p ∈ U → ∃ (n : ℕ) (t : K.LevelFace n), LevelFace.IsSafe K U t ∧ p ∈ K.levelFaceCarrier t
• locally_parent_safe : IsOpen U → ∀ (p : ↑U), ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (t : K.LevelFace (n + 1)), (K.levelFaceCarrier t ∩ Metric.ball (↑p) (ε / 2)).Nonempty → LevelFace.IsSafe K U (K.levelParentFace n t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCarrier_subset_parent (K : IntrinsicTwoComplex) (n : ℕ) (t : K.LevelFace (n + 1)) : K.levelFaceCarrier t ⊆ K.levelFaceCarrier (K.levelParentFace n t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_levelFace_succ_containing (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) {p : K.realization} (hp : p ∈ K.levelFaceCarrier t) : ∃ (u : K.LevelFace (n + 1)), p ∈ K.levelFaceCarrier u ∧ K.levelFaceCarrier u ⊆ K.levelFaceCarrier t

Every point of a level face lies in a child face at the next midpoint level whose entire transported carrier remains in the parent carrier.

@[instance 100]

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.defaultAdaptiveSafety_admissible (K : IntrinsicTwoComplex) (U : Set K.realization) : AdaptiveSafety.IsAdmissible K U

Containment in an open set is an admissible adaptive safety rule.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_levelFace_add_containing (K : IntrinsicTwoComplex) (n k : ℕ) (t : K.LevelFace n) {p : K.realization} (hp : p ∈ K.levelFaceCarrier t) : ∃ (u : K.LevelFace (n + k)), p ∈ K.levelFaceCarrier u ∧ K.levelFaceCarrier u ⊆ K.levelFaceCarrier t

Iterating the preceding child-cover lemma gives a face at every later level through a chosen point, with carrier contained in the original face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCarrier_eq_iUnion_descendants (K : IntrinsicTwoComplex) (n k : ℕ) (t : K.LevelFace n) : K.levelFaceCarrier t = ⋃ (u : K.LevelFace (n + k)), ⋃ (_ : K.levelFaceCarrier u ⊆ K.levelFaceCarrier t), K.levelFaceCarrier u

A level face is exactly the union of its faces at any prescribed later midpoint level. The descendant condition is stated geometrically, which avoids choosing a combinatorial parent for faces meeting an old edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCarrier_inter (K : IntrinsicTwoComplex) {n : ℕ} (s t : K.LevelFace n) : K.levelFaceCarrier s ∩ K.levelFaceCarrier t = ⇑(K.safeSubdivision n).homeo '' (K.safeSubdivision n).refined.faceCarrier (↑s ∩ ↑t)

Exact intersection formula for two transported faces at the same midpoint level.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.card_inter_levelFace_le_two (K : IntrinsicTwoComplex) {n : ℕ} {s t : K.LevelFace n} (hst : s ≠ t) : (↑s ∩ ↑t).card ≤ 2

Distinct maximal faces at one level share at most two vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.eq_facePoint_of_mem_faceCarrier_singleton (K : IntrinsicTwoComplex) (t : K.Face) (v : ↥↑t) (x : K.realization) (hx : x ∈ K.faceCarrier {↑v}) : x = K.facePoint t v

A barycentric realization point supported on one face vertex is that face's canonical vertex point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.eq_of_card_two_of_mem_faceCarriers_not_vertex (K : IntrinsicTwoComplex) (t : K.Face) {e d : Finset K.Vertex} (het : e ⊆ ↑t) : d ⊆ ↑t → ∀ (hecard : e.card = 2) (hdcard : d.card = 2) {x : K.realization} (hxe : x ∈ K.faceCarrier e) (hxd : x ∈ K.faceCarrier d) (hxNot : ∀ (v : ↥↑t), x ≠ K.facePoint t v), e = d

Two two-vertex subfaces of a triangle which share a nonvertex point are equal.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsSafe.child (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n : ℕ} {t : K.LevelFace (n + 1)} (ht : IsSafe K U (K.levelParentFace n t)) : IsSafe K U t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceRelInterior (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : Set K.realization

Relative interior of a transported level face, expressed by positive barycentric coordinates on all three face vertices.

Equations

• K.levelFaceRelInterior t = ⇑(K.safeSubdivision n).homeo '' {x : (K.safeSubdivision n).refined.realization | x ∈ (K.safeSubdivision n).refined.faceCarrier ↑t ∧ ∀ v ∈ ↑t, 0 < ↑x v}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceRelInterior_subset_carrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : K.levelFaceRelInterior t ⊆ K.levelFaceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceRelInterior_subset_parent (K : IntrinsicTwoComplex) (n : ℕ) (t : K.LevelFace (n + 1)) : K.levelFaceRelInterior t ⊆ K.levelFaceRelInterior (K.levelParentFace n t)

Midpoint subdivision sends a child's relative interior into its parent's relative interior.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_levelFaceRelInterior_levelFaceCarrier (K : IntrinsicTwoComplex) {n : ℕ} {t u : K.LevelFace n} (htu : t ≠ u) : Disjoint (K.levelFaceRelInterior t) (K.levelFaceCarrier u)

At a fixed midpoint level, the relative interior of one maximal face misses the carrier of every distinct maximal face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelAncestor (K : IntrinsicTwoComplex) (n k : ℕ) : K.LevelFace (n + k) → K.LevelFace n

The ancestor at level n of a face at level n + k.

Equations

• K.levelAncestor n 0 t = t
• K.levelAncestor n k.succ t = K.levelAncestor n k (K.levelParentFace (n + k) t)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelAncestor_zero (K : IntrinsicTwoComplex) (n : ℕ) (t : K.LevelFace n) : K.levelAncestor n 0 t = t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelAncestor_succ (K : IntrinsicTwoComplex) (n k : ℕ) (t : K.LevelFace (n + (k + 1))) : K.levelAncestor n (k + 1) t = K.levelAncestor n k (K.levelParentFace (n + k) t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCarrier_subset_ancestor (K : IntrinsicTwoComplex) (n k : ℕ) (t : K.LevelFace (n + k)) : K.levelFaceCarrier t ⊆ K.levelFaceCarrier (K.levelAncestor n k t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceRelInterior_subset_ancestor (K : IntrinsicTwoComplex) (n k : ℕ) (t : K.LevelFace (n + k)) : K.levelFaceRelInterior t ⊆ K.levelFaceRelInterior (K.levelAncestor n k t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsSafe.ancestor_child (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n k : ℕ} {t : K.LevelFace (n + k)} (ht : IsSafe K U (K.levelAncestor n k t)) : IsSafe K U t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsFirstSafe (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n : ℕ} : K.LevelFace n → Prop

A first-safe face is safe, but at a positive level its chosen parent is not safe.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsFirstSafe K U t = LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsSafe K U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsFirstSafe.safe (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n : ℕ} {t : K.LevelFace n} (ht : IsFirstSafe K U t) : IsSafe K U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_firstSafeRelInterior_laterCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n k : ℕ} {t : K.LevelFace n} {u : K.LevelFace (n + (k + 1))} (ht : LevelFace.IsFirstSafe K U t) (hu : LevelFace.IsFirstSafe K U u) : Disjoint (K.levelFaceRelInterior t) (K.levelFaceCarrier u)

A later first-safe face cannot meet the relative interior of an earlier first-safe face. If its ancestor were the earlier face, that safe ancestor would make its immediate parent safe; otherwise the fixed-level face-to-face property separates them.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_laterFirstSafeRelInterior_firstSafeCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n k : ℕ} {t : K.LevelFace n} {u : K.LevelFace (n + (k + 1))} (ht : LevelFace.IsFirstSafe K U t) (hu : LevelFace.IsFirstSafe K U u) : Disjoint (K.levelFaceRelInterior u) (K.levelFaceCarrier t)

The relative interior of a later first-safe face also misses the entire earlier carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.isFirstSafe_of_minimal (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {n : ℕ} (t : K.LevelFace n) {p : K.realization} (hsafe : IsSafe K U t) (hp : p ∈ K.levelFaceCarrier t) (hminimal : ∀ m < n, ¬∃ (u : K.LevelFace m), IsSafe K U u ∧ p ∈ K.levelFaceCarrier u) : IsFirstSafe K U t

@[reducible, inline]

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

The countable type of first-safe adaptive triangles.

Equations

• K.AdaptiveFace U = ((n : ℕ) × { t : K.LevelFace n // LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.LevelFace.IsFirstSafe K U t })

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCommonLevel (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (F : Finset (K.AdaptiveFace U)) : ℕ

One common midpoint level dominating a finite family of adaptive tiles.

Equations

• K.adaptiveFaceCommonLevel U F = F.sup fun (t : K.AdaptiveFace U) => t.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFace_level_le_commonLevel (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (F : Finset (K.AdaptiveFace U)) {t : K.AdaptiveFace U} (ht : t ∈ F) : t.fst ≤ K.adaptiveFaceCommonLevel U F

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : Set K.realization

Carrier of one adaptive triangle in the original realization.

Equations

• K.adaptiveFaceCarrier U t = K.levelFaceCarrier ↑t.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCarrier_eq_iUnion_commonLevel_descendants (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (F : Finset (K.AdaptiveFace U)) {t : K.AdaptiveFace U} (ht : t ∈ F) : K.adaptiveFaceCarrier U t = ⋃ (u : K.LevelFace (K.adaptiveFaceCommonLevel U F)), ⋃ (_ : K.levelFaceCarrier u ⊆ K.adaptiveFaceCarrier U t), K.levelFaceCarrier u

Every tile in a finite adaptive family is a union of faces of the family's common midpoint level. This is the finite source-subcomplex reduction used in the Radó crossing weld.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCarrier_subset (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.adaptiveFaceCarrier U t ⊆ U

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceRelInterior (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : Set K.realization

Relative interior of one adaptive face.

Equations

• K.adaptiveFaceRelInterior U t = K.levelFaceRelInterior ↑t.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_adaptiveFaceRelInterior_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {s t : K.AdaptiveFace U} (hst : s ≠ t) : Disjoint (K.adaptiveFaceRelInterior U s) (K.adaptiveFaceCarrier U t)

Distinct first-safe adaptive faces meet only on their relative boundaries.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_safeLevelFace_containing (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {p : K.realization} (hp : p ∈ U) : ∃ (n : ℕ) (t : K.LevelFace n), LevelFace.IsSafe K U t ∧ p ∈ K.levelFaceCarrier t

Some safe level face contains every point of the open set.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.firstSafeLevel (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : ℕ

The least midpoint level at which a safe face carries p.

Equations

• K.firstSafeLevel U hU p = Nat.find ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_firstSafeLevelFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : ∃ (t : K.LevelFace (K.firstSafeLevel U hU p)), LevelFace.IsSafe K U t ∧ ↑p ∈ K.levelFaceCarrier t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.firstSafeFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : K.LevelFace (K.firstSafeLevel U hU p)

A chosen least-level safe face through p.

Equations

• K.firstSafeFace U hU p = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.firstSafeFace_isSafe (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : LevelFace.IsSafe K U (K.firstSafeFace U hU p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_firstSafeFaceCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : ↑p ∈ K.levelFaceCarrier (K.firstSafeFace U hU p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.firstSafeFace_isFirstSafe (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (p : ↑U) : LevelFace.IsFirstSafe K U (K.firstSafeFace U hU p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iUnion_adaptiveFaceCarrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : ⋃ (t : K.AdaptiveFace U), K.adaptiveFaceCarrier U t = U

The first-safe adaptive triangles cover the whole open set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.dist_le_pow_of_mem_levelFaceCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) {x y : K.realization} (hx : x ∈ K.levelFaceCarrier t) (hy : y ∈ K.levelFaceCarrier t) : dist x y ≤ (1 / 2) ^ n

The transported diameter of every level-n face is at most 2⁻ⁿ.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.parent_isSafe_of_inter_ball (K : IntrinsicTwoComplex) (U : Set K.realization) {n : ℕ} (t : K.LevelFace (n + 1)) {p : K.realization} {ε : ℝ} : 0 < ε → ∀ (hball : Metric.ball p ε ⊆ U) (hmesh : (1 / 2) ^ n < ε / 2) (hinter : (K.levelFaceCarrier t ∩ Metric.ball p (ε / 2)).Nonempty), LevelFace.IsSafe K U (K.levelParentFace n t)

If a child face meets a half-radius ball and its parent mesh is below that half-radius, then the parent is already safe.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.finite_adaptiveFace_level_lt (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (N : ℕ) : {t : K.AdaptiveFace U | t.fst < N}.Finite

Only finitely many adaptive faces occur below a fixed midpoint level.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCarrierInOpen (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : Set ↑U

Carrier of an adaptive face in the open subspace itself.

Equations

• K.adaptiveFaceCarrierInOpen U t = Subtype.val ⁻¹' K.adaptiveFaceCarrier U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.locallyFinite_adaptiveFaceCarrierInOpen (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : LocallyFinite (K.adaptiveFaceCarrierInOpen U)

The first-safe adaptive triangle family is locally finite in the open set.

Finite boundary data on each adaptive tile

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceVertexPoint (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (v : ↥↑t) : K.realization

The geometric point represented by one vertex of a level face.

Equations

• K.levelFaceVertexPoint t v = (K.safeSubdivision n).homeo ((K.safeSubdivision n).refined.facePoint t v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceVertexPoint_mem_carrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (v : ↥↑t) : K.levelFaceVertexPoint t v ∈ K.levelFaceCarrier t

@[reducible, inline]

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

A vertex occurrence on an adaptive tile. Geometrically equal occurrences on adjacent tiles are deliberately not quotiented here; boundaryVertices takes their finite image as actual points.

Equations

• K.AdaptiveVertexOccurrence U t = ↥↑↑t.snd

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveVertexPoint (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (v : K.AdaptiveVertexOccurrence U t) : K.realization

The adaptiveVertexPoint declaration.

Equations

• K.adaptiveVertexPoint U t v = K.levelFaceVertexPoint (↑t.snd) v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveVertexPoint_mem_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (v : K.AdaptiveVertexOccurrence U t) : K.adaptiveVertexPoint U t v ∈ K.adaptiveFaceCarrier U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isCompact_adaptiveFaceCarrierInOpen (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : IsCompact (K.adaptiveFaceCarrierInOpen U t)

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

Adaptive tiles touching a fixed tile.

Equations

• K.TouchingFace U t = { u : K.AdaptiveFace U // (K.adaptiveFaceCarrierInOpen U u ∩ K.adaptiveFaceCarrierInOpen U t).Nonempty }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.finite_touchingFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) : Finite (K.TouchingFace U t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.selfTouchingFace (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.TouchingFace U t

Every tile touches itself.

Equations

• K.selfTouchingFace U t = ⟨t, ⋯⟩

@[reducible, inline]

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

All vertex occurrences belonging to tiles which touch t.

Equations

• K.TouchingVertexOccurrence U t = ((u : K.TouchingFace U t) × K.AdaptiveVertexOccurrence U ↑u)

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

The finite set of all touching-tile vertices which lie in t. It contains the original three corners of t and every hanging midpoint introduced by a finer neighboring tile.

Equations

• K.boundaryVertices U hU t = {p ∈ Finset.image (fun (v : K.TouchingVertexOccurrence U t) => K.adaptiveVertexPoint U (↑v.fst) v.snd) Finset.univ | p ∈ K.adaptiveFaceCarrier U t}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_boundaryVertices_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (p : K.realization) : p ∈ K.boundaryVertices U hU t ↔ p ∈ K.adaptiveFaceCarrier U t ∧ ∃ (u : K.TouchingFace U t) (v : K.AdaptiveVertexOccurrence U ↑u), K.adaptiveVertexPoint U (↑u) v = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_boundaryVertices_iff_of_mem_adaptiveFaceCarrier_inter (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (s t : K.AdaptiveFace U) {p : K.realization} (hps : p ∈ K.adaptiveFaceCarrier U s) (hpt : p ∈ K.adaptiveFaceCarrier U t) : p ∈ K.boundaryVertices U hU s ↔ p ∈ K.boundaryVertices U hU t

On the overlap of two adaptive tiles, their finite sets of collected boundary marks agree pointwise. Indeed a vertex occurrence whose tile touches one of the two tiles at the shared point also touches the other there.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCarrier_inter_subset_relativeBoundaries (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] {s t : K.AdaptiveFace U} (hst : s ≠ t) : K.adaptiveFaceCarrier U s ∩ K.adaptiveFaceCarrier U t ⊆ K.adaptiveFaceCarrier U s \ K.adaptiveFaceRelInterior U s ∩ (K.adaptiveFaceCarrier U t \ K.adaptiveFaceRelInterior U t)

Distinct first-safe tiles meet only in the relative boundary of each tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceVertexPoint_not_mem_relInterior (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (v : ↥↑t) : K.levelFaceVertexPoint t v ∉ K.levelFaceRelInterior t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveVertexPoint_not_mem_relInterior (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (v : K.AdaptiveVertexOccurrence U t) : K.adaptiveVertexPoint U t v ∉ K.adaptiveFaceRelInterior U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryVertices_not_mem_relInterior (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.boundaryVertices U hU t) : p ∉ K.adaptiveFaceRelInterior U t

Every collected touching vertex lies on the relative boundary of the fixed tile.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveVertexPoint_mem_boundaryVertices (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (v : K.AdaptiveVertexOccurrence U t) : K.adaptiveVertexPoint U t v ∈ K.boundaryVertices U hU t

All three original corners of a tile occur in its resolved boundary vertex set.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeCarrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) : Set K.realization

Carrier of one cyclic edge of a level face.

Equations

• K.levelFaceEdgeCarrier t i = ⇑(K.safeSubdivision n).homeo '' (K.safeSubdivision n).refined.faceCarrier ↑((K.safeSubdivision n).refined.faceEdge t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeCarrier_subset (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) : K.levelFaceEdgeCarrier t i ⊆ K.levelFaceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_levelFaceEdge_of_mem_not_relInterior (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) {p : K.realization} (hp : p ∈ K.levelFaceCarrier t) (hpInt : p ∉ K.levelFaceRelInterior t) : ∃ (i : ZMod 3), p ∈ K.levelFaceEdgeCarrier t i

Every point of a closed level face outside its relative interior lies on a cyclic edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertices (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : Finset K.realization

Resolved boundary vertices lying on one cyclic edge.

Equations

• K.boundaryEdgeVertices U hU t i = {p ∈ K.boundaryVertices U hU t | p ∈ K.levelFaceEdgeCarrier (↑t.snd) i}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_boundaryEdgeVertices_iff (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) : p ∈ K.boundaryEdgeVertices U hU t i ↔ p ∈ K.boundaryVertices U hU t ∧ p ∈ K.levelFaceEdgeCarrier (↑t.snd) i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) (p : K.realization) : ℝ

Barycentric parameter along a cyclic level-face edge, from vertex i to vertex i+1.

Equations

• K.levelFaceEdgeParameter t i p = ↑((K.safeSubdivision n).homeo.symm p) ((K.safeSubdivision n).refined.faceVertex t (i + 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_injOn (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) : Set.InjOn (K.levelFaceEdgeParameter t i) (K.levelFaceEdgeCarrier t i)

@[reducible, inline]

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

A resolved vertex on one adaptive edge.

Equations

• K.BoundaryEdgeVertex U hU t i = ↥(K.boundaryEdgeVertices U hU t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeParameter_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : Function.Injective fun (p : K.BoundaryEdgeVertex U hU t i) => K.levelFaceEdgeParameter (↑t.snd) i ↑p

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLE (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) (p q : K.BoundaryEdgeVertex U hU t i) : Prop

The parameter order on the finite set of vertices of one resolved edge.

Equations

• K.boundaryEdgeVertexLE U hU t i p q = (K.levelFaceEdgeParameter (↑t.snd) i ↑p ≤ K.levelFaceEdgeParameter (↑t.snd) i ↑q)

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLEDecidable (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : DecidableRel (K.boundaryEdgeVertexLE U hU t i)

Equations

• K.boundaryEdgeVertexLEDecidable U hU t i p q = LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLEDecidable._aux_1 K U hU t i p q

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLE_total (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : Std.Total (K.boundaryEdgeVertexLE U hU t i)

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLE_antisymm (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : Std.Antisymm (K.boundaryEdgeVertexLE U hU t i)

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexLE_isTrans (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : IsTrans (K.BoundaryEdgeVertex U hU t i) (K.boundaryEdgeVertexLE U hU t i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexList (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : List K.realization

Canonically ordered vertices on one resolved adaptive edge.

Equations

• K.boundaryEdgeVertexList U hU t i = List.map Subtype.val ((K.boundaryEdgeVertices U hU t i).attach.sort (K.boundaryEdgeVertexLE U hU t i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_boundaryEdgeVertexList_iff (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) : p ∈ K.boundaryEdgeVertexList U hU t i ↔ p ∈ K.boundaryEdgeVertices U hU t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexList_nodup (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : (K.boundaryEdgeVertexList U hU t i).Nodup

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexList_pairwise_parameter_le (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : List.Pairwise (fun (p q : K.realization) => K.levelFaceEdgeParameter (↑t.snd) i p ≤ K.levelFaceEdgeParameter (↑t.snd) i q) (K.boundaryEdgeVertexList U hU t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_adjacent_get_of_pairwise_le {α : Type u_1} (L : List α) (f : α → ℝ) (hlength : 2 ≤ L.length) (hpair : List.Pairwise (fun (a b : α) => f a ≤ f b) L) {r : ℝ} (hfirst : f (L.get ⟨0, ⋯⟩) ≤ r) (hlast : r ≤ f (L.get ⟨L.length - 1, ⋯⟩)) : ∃ (j : Fin (L.length - 1)), f (L.get ⟨↑j, ⋯⟩) ≤ r ∧ r ≤ f (L.get ⟨↑j + 1, ⋯⟩)

A monotone finite list with at least two entries covers every parameter between its endpoints by one of its consecutive intervals.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeFirstCorner (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : K.realization

The first corner of a cyclic adaptive edge.

Equations

• K.adaptiveEdgeFirstCorner U t i = K.levelFaceVertexPoint ↑t.snd ⟨(K.safeSubdivision t.fst).refined.faceVertex (↑t.snd) i, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeSecondCorner (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : K.realization

The second corner of a cyclic adaptive edge.

Equations

• K.adaptiveEdgeSecondCorner U t i = K.levelFaceVertexPoint ↑t.snd ⟨(K.safeSubdivision t.fst).refined.faceVertex (↑t.snd) (i + 1), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeFirstCorner_mem_boundaryEdgeVertices (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : K.adaptiveEdgeFirstCorner U t i ∈ K.boundaryEdgeVertices U hU t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeSecondCorner_mem_boundaryEdgeVertices (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : K.adaptiveEdgeSecondCorner U t i ∈ K.boundaryEdgeVertices U hU t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeFirstCorner_ne_second (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : K.adaptiveEdgeFirstCorner U t i ≠ K.adaptiveEdgeSecondCorner U t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.two_le_boundaryEdgeVertices_card (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : 2 ≤ (K.boundaryEdgeVertices U hU t i).card

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.two_le_boundaryEdgeVertexList_length (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : 2 ≤ (K.boundaryEdgeVertexList U hU t i).length

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_adaptiveEdgeFirstCorner (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeFirstCorner U t i) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_adaptiveEdgeSecondCorner (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) (i : ZMod 3) : K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeSecondCorner U t i) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeParameter_mem_Icc (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.levelFaceEdgeCarrier t i) : K.levelFaceEdgeParameter t i p ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexList_first_parameter (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : K.levelFaceEdgeParameter (↑t.snd) i ((K.boundaryEdgeVertexList U hU t i).get ⟨0, ⋯⟩) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.boundaryEdgeVertexList_last_parameter (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) : K.levelFaceEdgeParameter (↑t.snd) i ((K.boundaryEdgeVertexList U hU t i).get ⟨(K.boundaryEdgeVertexList U hU t i).length - 1, ⋯⟩) = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenterSimplex (K : IntrinsicTwoComplex) (t : K.Face) : ↑(stdSimplex ℝ ↥↑t)

The equal-weight point of the standard simplex on an intrinsic face.

Equations

• K.faceCenterSimplex t = ⟨fun (x : ↥↑t) => 1 / 3, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenterSimplex_apply (K : IntrinsicTwoComplex) (t : K.Face) (v : ↥↑t) : (K.faceCenterSimplex t) v = 1 / 3

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCenter (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : K.realization

The barycentric center of an arbitrary level face, transported to the original realization.

Equations

• K.levelFaceCenter t = (K.safeSubdivision n).homeo ((K.safeSubdivision n).refined.faceStandardMap t ((K.safeSubdivision n).refined.faceCenterSimplex t))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCenter_mem_relInterior (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : K.levelFaceCenter t ∈ K.levelFaceRelInterior t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceCenter_mem_carrier (K : IntrinsicTwoComplex) {n : ℕ} (t : K.LevelFace n) : K.levelFaceCenter t ∈ K.levelFaceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.levelFaceEdgeCarrier_subset_of_common_not_vertex (K : IntrinsicTwoComplex) (n k : ℕ) (s : K.LevelFace n) (t : K.LevelFace (n + k)) (i : ZMod 3) {p : K.realization} (hdisjoint : Disjoint (K.levelFaceRelInterior t) (K.levelFaceCarrier s)) (hps : p ∈ K.levelFaceCarrier s) (hpt : p ∈ K.levelFaceEdgeCarrier t i) (hpNot : ∀ (v : ↥↑t), p ≠ K.levelFaceVertexPoint t v) : K.levelFaceEdgeCarrier t i ⊆ K.levelFaceCarrier s

If a later-level edge meets an earlier face at a point which is not a later-level vertex, and the two face interiors are disjoint, then the whole later edge lies in the earlier face. This is the no-crossing fact for nested midpoint subdivisions.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFace_edgeCarrier_subset_of_level_le_of_common_not_boundaryVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {s t : K.AdaptiveFace U} (hst : s ≠ t) (hlevel : s.fst ≤ t.fst) (i : ZMod 3) {p : K.realization} (hps : p ∈ K.adaptiveFaceCarrier U s) (hpt : p ∈ K.levelFaceEdgeCarrier (↑t.snd) i) (hpNot : p ∉ K.boundaryVertices U hU t) : K.levelFaceEdgeCarrier (↑t.snd) i ⊆ K.adaptiveFaceCarrier U s

Adaptive-tile specialization of nested-edge no crossing. At a common point which is not a resolved vertex of the later tile, the later edge is contained in the earlier tile.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.realization

The barycentric center of one adaptive tile, transported to the original realization.

Equations

• K.adaptiveFaceCenter U t = (K.safeSubdivision t.fst).homeo ((K.safeSubdivision t.fst).refined.faceStandardMap (↑t.snd) ((K.safeSubdivision t.fst).refined.faceCenterSimplex ↑t.snd))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_mem_relInterior (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.adaptiveFaceCenter U t ∈ K.adaptiveFaceRelInterior U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_mem_carrier (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] (t : K.AdaptiveFace U) : K.adaptiveFaceCenter U t ∈ K.adaptiveFaceCarrier U t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_ne_boundaryVertex (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.boundaryVertices U hU t) : K.adaptiveFaceCenter U t ≠ p

@[reducible, inline]

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

One of the consecutive intervals in the ordered subdivision of an adaptive edge.

Equations

• K.AdaptiveEdgeInterval U hU t i = Fin ((K.boundaryEdgeVertexList U hU t i).length - 1)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalFirst (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.realization

First endpoint of a resolved adaptive-edge interval.

Equations

• K.adaptiveEdgeIntervalFirst U hU t i j = (K.boundaryEdgeVertexList U hU t i).get ⟨↑j, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalSecond (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.realization

Second endpoint of a resolved adaptive-edge interval.

Equations

• K.adaptiveEdgeIntervalSecond U hU t i j = (K.boundaryEdgeVertexList U hU t i).get ⟨↑j + 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalFirst_mem_boundaryEdgeVertices (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.adaptiveEdgeIntervalFirst U hU t i j ∈ K.boundaryEdgeVertices U hU t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalSecond_mem_boundaryEdgeVertices (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.adaptiveEdgeIntervalSecond U hU t i j ∈ K.boundaryEdgeVertices U hU t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeIntervalFirst_ne_second (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.adaptiveEdgeIntervalFirst U hU t i j ≠ K.adaptiveEdgeIntervalSecond U hU t i j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveEdgeInterval_parameter_lt (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.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalFirst U hU t i j) < K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalSecond U hU t i j)

Consecutive vertices in the resolved edge order have strictly increasing edge parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_adaptiveEdgeInterval_parameter_mem_Icc (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : ∃ (j : K.AdaptiveEdgeInterval U hU t i), r ∈ Set.Icc (K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalFirst U hU t i j)) (K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalSecond U hU t i j))

Every parameter on an adaptive edge lies between the parameters of two consecutive resolved boundary vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.not_parameter_mem_Ioo_adaptiveEdgeInterval (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) {p : K.realization} (hp : p ∈ K.boundaryEdgeVertices U hU t i) : K.levelFaceEdgeParameter (↑t.snd) i p ∉ Set.Ioo (K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalFirst U hU t i j)) (K.levelFaceEdgeParameter (↑t.snd) i (K.adaptiveEdgeIntervalSecond U hU t i j))

No resolved boundary mark lies strictly between the two consecutive marks of an adaptive edge interval.

@[reducible, inline]

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

The countable family of fan triangles before identifying their shared geometric edges.

Equations

• K.AdaptiveFanFace U hU = ((t : K.AdaptiveFace U) × (i : ZMod 3) × K.AdaptiveEdgeInterval U hU t i)

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

The finite family of all resolved fan triangles over one adaptive tile.

Equations

• K.adaptiveFanFacesOver U hU t = Finset.map { toFun := fun (p : (i : ZMod 3) × K.AdaptiveEdgeInterval U hU t i) => ⟨t, p⟩, inj' := ⋯ } (Finset.univ.sigma fun (i : ZMod 3) => Finset.univ)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_adaptiveFanFacesOver_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (t : K.AdaptiveFace U) (f : K.AdaptiveFanFace U hU) : f ∈ K.adaptiveFanFacesOver U hU t ↔ f.fst = t

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

The adaptiveFanFaceVertices declaration.

Equations

• K.adaptiveFanFaceVertices U hU f = {K.adaptiveFaceCenter U f.fst, K.adaptiveEdgeIntervalFirst U hU f.fst f.snd.fst f.snd.snd, K.adaptiveEdgeIntervalSecond U hU f.fst f.snd.fst f.snd.snd}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceVertices_card (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).card = 3