Carriers, refinement compatibility, and the star lemmas

The interface between the construction of the nested cellulations and the abstraction the limit homeomorphism uses. The blueprint says at the head of that section (tex, "The limit homeomorphism of the interiors") that it "forgets how the decompositions were constructed and uses only their nesting, matching, and shrinking properties"; everything below is therefore stated for an abstract refinement relation Realization.Refines between two realizations of two generated structures, and not for either elementary constructor. The two constructors enter only at the very end, as the two theorems that produce a Refines from them.

The carrier is a function

Realization.carrier is car_Γ(x) of the blueprint, exported as a total function Plane → γ rather than as an existential: σ_n(x) is used on every line of the limit argument. Outside the closed domain it is junk (whence the [Nonempty γ]), and every lemma about it carries the hypothesis x ∈ D that makes it meaningful. Its characterising property is IsCellDecomposition.carrier_eq: any cell whose open part contains x is the carrier.

What Refines is, and why it is the right shape

R'.Refines R par says: par maps cells of the finer structure to cells of the coarser one and 2-cells to 2-cells, it is compatible with ≼_abs (assertion (iv) of lem:cellulation-invariants), and each open cell of the finer realization sits inside the open cell of its parent. The last clause is the geometric content of the blueprint's proof of lem:refinement-compatibility(a) — "a point in either new subedge or at the new vertex had the old open edge as its old carrier" — and it implies the weaker closure (R'.cell σ) ⊆ closure (R.cell (par σ)) that part (b) needs.

Refines is a relation between two realizations of two different abstract structures over the same name type γ, parametrised by the composite parent map. Refines.trans composes them, so "a finite sequence of elementary refinements" needs no separate treatment: a consumer that builds its stages one operation at a time gets the composite by iterating trans.

Part (c) of lem:refinement-compatibility — "corresponding cells have corresponding parents" — is, under the representation of CombinatorialInvariance.lean, the statement that one and the same par : γ → γ serves both realizations: cells are abstract names, and two Refines instances sharing a par is exactly a compatible matched refinement. There is nothing to transport, and the substance of (c) is its consequence, Refines.carrier_congr.

Blueprint

• Schoenflies.CellStructure.Realization.carrier — car_Γ(x), with Schoenflies.CellStructure.Realization.IsCellDecomposition.carrier_eq its characterisation.
• Schoenflies.CellStructure.Realization.Refines — a refinement of one generated matched cell structure by another, with Refines.trans for a finite sequence of them.
• lem:refinement-compatibility:
  • (a) Schoenflies.CellStructure.Realization.Refines.parent_carrier;
  • (b) Schoenflies.CellStructure.Realization.Refines.star_subset (cells) and Schoenflies.CellStructure.Realization.Refines.star_carrier_subset (points);
  • (c) Schoenflies.CellStructure.SkeletonHomeo.carrier_congr (corresponding skeleton points have corresponding carriers, via Schoenflies.CellStructure.SkeletonHomeo.image_cell), Schoenflies.CellStructure.Realization.Refines.carrier_congr (and then at every earlier stage), and the form the limit argument actually cites, Schoenflies.CellStructure.Realization.Refines.target_star_subset (T_{n+1}(x) ⊆ T_n(x)).
• lem:star-intersection — Schoenflies.CellStructure.Realization.star_inter_nonempty_congr.
• lem:star-face-mesh — Schoenflies.CellStructure.Realization.IsCellDecomposition.star_eq_faces, with (a) …diam_star_le, …diam_star_lt, …diam_star_carrier_lt and (b) Schoenflies.CellStructure.Realization.Refines.diam_cell_le, Schoenflies.CellStructure.Realization.Refines.diam_cell_le_of_forall.
• lem:cell-neighborhood — Schoenflies.CellStructure.Realization.cellNbhd and Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_neighborhood.
• rem:inductive-invariants — honoured: nothing here is proved by a case check on the constructors. The inductive content lives in GeneratedStructure.lean; the two bridge theorems Schoenflies.CellStructure.SubdivData.IsRefinement.refines and Schoenflies.CellStructure.SplitData.refines are the only declarations that mention a constructor at all.

Schoenflies.CellStructure.refines_of_elementary is the shared bridge: both elementary operations replace a single cell c by a set N of fresh cells and send N to c, so one lemma serves both.

theorem Schoenflies.CellStructure.finite_cells {γ : Type u_1} (S : CellStructure γ) : S.cells.Finite

A cell structure has finitely many cells.

Elementary facts about the closed star

Realization.star is the St of the blueprint and is defined in CombinatorialInvariance.lean; these are the membership and containment lemmas its consumers need.

theorem Schoenflies.CellStructure.Realization.mem_star_iff {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {σ : γ} {y : Plane} : y ∈ R.star σ ↔ ∃ (τ : γ), S.sub σ τ ∧ y ∈ closure (R.cell τ)

theorem Schoenflies.CellStructure.Realization.closure_cell_subset_star {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {σ τ : γ} (h : S.sub σ τ) : closure (R.cell τ) ⊆ R.star σ

A closed supercell sits inside the star.

theorem Schoenflies.CellStructure.Realization.finite_supercells {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (σ : γ) : (S.supercells σ).Finite

The index set of a star is finite: it consists of cells.

theorem Schoenflies.CellStructure.Realization.isClosed_star {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {σ : γ} (hS : S.CombInvariants) : IsClosed (R.star σ)

A star is a finite union of closed sets, hence closed.

The carrier of a point

car_Γ(x), the unique open cell containing x. It is a total function; off the closed domain its value is junk, and every lemma below supplies x ∈ D.

noncomputable def Schoenflies.CellStructure.Realization.carrier {γ : Type u_1} {S : CellStructure γ} [Nonempty γ] (R : S.Realization) (x : Plane) : γ

The carrier car_Γ(x) of a point: the unique cell whose open cell contains x. Uniqueness, and the fact that there is one at all for x in the closed domain, are assertion (i) of lem:cellulation-invariants — see IsCellDecomposition.carrier_eq and IsCellDecomposition.mem_cell_carrier.

Equations

• R.carrier x = if h : ∃ σ ∈ S.cells, x ∈ R.cell σ then h.choose else Classical.arbitrary γ

theorem Schoenflies.CellStructure.Realization.carrier_spec {γ : Type u_1} {S : CellStructure γ} [Nonempty γ] (R : S.Realization) (x : Plane) (h : ∃ σ ∈ S.cells, x ∈ R.cell σ) : R.carrier x ∈ S.cells ∧ x ∈ R.cell (R.carrier x)

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_subset_domain {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) : R.cell σ ⊆ D

Every open cell lies in the closed domain.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.exists_cell {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x : Plane} (h : R.IsCellDecomposition D) (hx : x ∈ D) : ∃ σ ∈ S.cells, x ∈ R.cell σ

A point of the closed domain lies in some open cell — the covering half of assertion (i).

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.mem_cells_carrier {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hx : x ∈ D) : R.carrier x ∈ S.cells

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.mem_cell_carrier {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hx : x ∈ D) : x ∈ R.cell (R.carrier x)

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.carrier_eq {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} {x : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hx : x ∈ R.cell σ) : R.carrier x = σ

The characterising property of the carrier: any cell whose open part contains x is the carrier of x. This is the uniqueness half of assertion (i), and it is the lemma every computation of a carrier goes through.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.mem_star_carrier {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hx : x ∈ D) : x ∈ R.star (R.carrier x)

A point lies in the star of its own carrier.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_nonempty {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) : (R.star σ).Nonempty

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_subset_closure_domain {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) : R.star σ ⊆ closure D

A star lies in the closure of the domain, so a bounded domain bounds every star.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.isBounded_star {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) : Bornology.IsBounded (R.star σ)

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.isCompact_star {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) : IsCompact (R.star σ)

A star is compact: it is closed, and bounded once the domain is. The limit argument needs this to intersect a nested sequence of stars.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_anti_of_sub {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ ρ : γ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hσ : σ ∈ S.cells) (hρ : ρ ∈ S.cells) (hsub : S.sub σ ρ) : R.star ρ ⊆ R.star σ

Stars are antitone in the subcell relation. The transitivity this needs is not assumed of a CellStructure; it is read off assertion (i) by IsCellDecomposition.sub_trans.

Refinement

The abstract relation "R' refines R with parent map par". It is deliberately not tied to either elementary operation: the limit argument uses only these three clauses.

structure Schoenflies.CellStructure.Realization.Refines {γ : Type u_1} {S' S : CellStructure γ} (R' : S'.Realization) (R : S.Realization) (par : γ → γ) : Prop

R' refines R along the parent map par.

R' and R realize two different abstract structures over the same name type; par is the composite parent map of lem:cellulation-invariants(iv). The three combinatorial clauses say that par takes cells to cells, 2-cells to 2-cells, and respects ≼_abs; the geometric clause says that each open cell of the finer stage lies inside the open cell of its parent, which is what makes carriers refine (part (a)).

• parent_mem_cells ⦃σ : γ⦄ : σ ∈ S'.cells → par σ ∈ S.cells

  The parent of a cell is a cell.

• parent_mem_faces ⦃F : γ⦄ : F ∈ S'.faces → par F ∈ S.faces

  The parent of a 2-cell is a 2-cell.

• sub_parent ⦃σ τ : γ⦄ : S'.sub σ τ → S.sub (par σ) (par τ)

  Assertion (iv): the parent map is compatible with the subcell relation.

• cell_subset ⦃σ : γ⦄ : σ ∈ S'.cells → R'.cell σ ⊆ R.cell (par σ)

  Each open cell lies inside the open cell of its parent.

theorem Schoenflies.CellStructure.Realization.Refines.refl {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.Refines R id

Every realization refines itself along the identity: the empty sequence of elementary refinements.

theorem Schoenflies.CellStructure.Realization.Refines.trans {γ : Type u_1} {S S' S'' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {R'' : S''.Realization} {par par' : γ → γ} (h' : R''.Refines R' par') (h : R'.Refines R par) : R''.Refines R (par ∘ par')

Refinements compose. This is what turns lem:refinement-compatibility from a statement about one elementary refinement into a statement about "a finite sequence of elementary refinements": a consumer that builds its stages one operation at a time iterates this.

theorem Schoenflies.CellStructure.Realization.Refines.closure_cell_subset {γ : Type u_1} {S S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} (h : R'.Refines R par) {σ : γ} (hσ : σ ∈ S'.cells) : closure (R'.cell σ) ⊆ closure (R.cell (par σ))

The closed cells refine along with the open ones.

theorem Schoenflies.CellStructure.Realization.Refines.parent_carrier {γ : Type u_1} {S : CellStructure γ} {D : Set Plane} {S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} {D' : Set Plane} [Nonempty γ] (href : R'.Refines R par) (h : R.IsCellDecomposition D) (h' : R'.IsCellDecomposition D') {x : Plane} (hx : x ∈ D') : par (R'.carrier x) = R.carrier x

lem:refinement-compatibility(a): the parent of the carrier of x at the finer stage is its carrier at the coarser stage.

theorem Schoenflies.CellStructure.Realization.Refines.star_subset {γ : Type u_1} {S S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} (href : R'.Refines R par) (hS' : S'.CombInvariants) {σ : γ} : R'.star σ ⊆ R.star (par σ)

lem:refinement-compatibility(b), the cell-star inclusion: once a star is small it stays small.

theorem Schoenflies.CellStructure.Realization.Refines.star_carrier_subset {γ : Type u_1} {S : CellStructure γ} {D : Set Plane} {S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} {D' : Set Plane} [Nonempty γ] (href : R'.Refines R par) (hS' : S'.CombInvariants) (h : R.IsCellDecomposition D) (h' : R'.IsCellDecomposition D') {x : Plane} (hx : x ∈ D') : R'.star (R'.carrier x) ⊆ R.star (R.carrier x)

lem:refinement-compatibility(b), pointwise: closed stars of a fixed point are monotone under refinement.

Matched refinements: part (c)

Two realizations of one abstract structure are matched; a compatible matched refinement is a pair of Refines instances sharing one parent map. That sharing is the blueprint's "corresponding cells have corresponding parents": the parent map is a map of abstract names, so there is only ever one of it. The substance is the consequence recorded here.

theorem Schoenflies.CellStructure.Realization.Refines.carrier_congr {γ : Type u_1} {S S' : CellStructure γ} {R₁ R₂ : S.Realization} {R₁' R₂' : S'.Realization} {par : γ → γ} {D₁ D₂ D₁' D₂' : Set Plane} [Nonempty γ] (h₁ : R₁'.Refines R₁ par) (h₂ : R₂'.Refines R₂ par) (hd₁ : R₁.IsCellDecomposition D₁) (hd₁' : R₁'.IsCellDecomposition D₁') (hd₂ : R₂.IsCellDecomposition D₂) (hd₂' : R₂'.IsCellDecomposition D₂') {x y : Plane} (hx : x ∈ D₁') (hy : y ∈ D₂') (hxy : R₁'.carrier x = R₂'.carrier y) : R₁.carrier x = R₂.carrier y

lem:refinement-compatibility(c): if x and y have corresponding carriers at the finer stage — corresponding means equal as abstract cells — then they have corresponding carriers at the coarser stage, and hence at every earlier stage by iteration.

theorem Schoenflies.CellStructure.Realization.Refines.target_star_subset {γ : Type u_1} {S S' : CellStructure γ} {R₁ R₂ : S.Realization} {R₁' R₂' : S'.Realization} {par : γ → γ} {D₁ D₁' : Set Plane} [Nonempty γ] (h₁ : R₁'.Refines R₁ par) (h₂ : R₂'.Refines R₂ par) (hS' : S'.CombInvariants) (hd₁ : R₁.IsCellDecomposition D₁) (hd₁' : R₁'.IsCellDecomposition D₁') {x : Plane} (hx : x ∈ D₁') : R₂'.star (R₁'.carrier x) ⊆ R₂.star (R₁.carrier x)

The nesting the limit map runs on. With R₁ the source realization and R₂ the target one, T_n(x) = R₂.star (R₁.carrier x) is the closed target star of the cell corresponding to σ_n(x), and this says T_{n+1}(x) ⊆ T_n(x).

Only the source decompositions are needed: the parent map is abstract, so the target stage inherits the inclusion from the source carrier.

Intersection of corresponding stars

theorem Schoenflies.CellStructure.Realization.star_inter_nonempty_of_star_inter_nonempty {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ : Set Plane} (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) (hS : S.CombInvariants) {σ τ : γ} (hne : (R₁.star σ ∩ R₁.star τ).Nonempty) : (R₂.star σ ∩ R₂.star τ).Nonempty

One direction of lem:star-intersection. The two realizations are realizations of the same abstract structure, so "the corresponding cells" are literally σ and τ again.

theorem Schoenflies.CellStructure.Realization.star_inter_nonempty_congr {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ : Set Plane} (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) (hS : S.CombInvariants) {σ τ : γ} : (R₁.star σ ∩ R₁.star τ).Nonempty ↔ (R₂.star σ ∩ R₂.star τ).Nonempty

lem:star-intersection: corresponding stars meet on one side exactly when they meet on the other. This is what makes the limit map injective.

Stars and the face mesh

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_eq_faces {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hσ : σ ∈ S.cells) : R.star σ = ⋃ F ∈ {F : γ | F ∈ S.faces ∧ S.sub σ F}, closure (R.cell F)

lem:star-face-mesh, the displayed equality: a closed star is the union of the closed 2-cells incident with the cell. Every supercell is a subcell of some 2-cell by assertion (v), and its closure is then inside that closed 2-cell.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.mem_closure_face {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} {x : Plane} (h : R.IsCellDecomposition D) {F : γ} (hσ : σ ∈ S.cells) (hF : F ∈ S.faces) (hsub : S.sub σ F) (hx : x ∈ R.cell σ) : x ∈ closure (R.cell F)

Every closed 2-cell incident with σ contains every point of the open cell σ.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.dist_le_of_mem_star {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} {x y : Plane} {η : ℝ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) (hσ : σ ∈ S.cells) (hdiam : ∀ ⦃F : γ⦄, F ∈ S.faces → S.sub σ F → Metric.diam (closure (R.cell F)) ≤ η) (hx : x ∈ R.cell σ) (hy : y ∈ R.star σ) : dist x y ≤ η

Every point of the star of σ is within η of every point of the open cell σ, when the closed 2-cells incident with σ all have diameter at most η.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.diam_star_le {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} {η : ℝ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) (hσ : σ ∈ S.cells) (hdiam : ∀ ⦃F : γ⦄, F ∈ S.faces → S.sub σ F → Metric.diam (closure (R.cell F)) ≤ η) : Metric.diam (R.star σ) ≤ 2 * η

lem:star-face-mesh(a), in its non-strict form: a mesh bound on the closed 2-cells incident with a cell doubles to a bound on the diameter of its star.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.diam_star_lt {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} {η : ℝ} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) (hσ : σ ∈ S.cells) (hdiam : ∀ ⦃F : γ⦄, F ∈ S.faces → S.sub σ F → Metric.diam (closure (R.cell F)) < η) : Metric.diam (R.star σ) < 2 * η

lem:star-face-mesh(a): if every closed 2-cell incident with σ has diameter strictly less than η, the star has diameter strictly less than 2η.

Strictness costs the finiteness of the set of incident 2-cells: the bound is realised at the largest of them, and there are finitely many.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.diam_star_carrier_lt {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x : Plane} {η : ℝ} [Nonempty γ] (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hD : Bornology.IsBounded D) (hx : x ∈ D) (hdiam : ∀ ⦃F : γ⦄, F ∈ S.faces → S.sub (R.carrier x) F → Metric.diam (closure (R.cell F)) < η) : Metric.diam (R.star (R.carrier x)) < 2 * η

lem:star-face-mesh(a) at a point: the form the shrinking-stars proposition consumes.

theorem Schoenflies.CellStructure.Realization.Refines.diam_cell_le {γ : Type u_1} {S S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} {D : Set Plane} (href : R'.Refines R par) (h : R.IsCellDecomposition D) (hD : Bornology.IsBounded D) {F : γ} (hF : F ∈ S'.cells) : Metric.diam (closure (R'.cell F)) ≤ Metric.diam (closure (R.cell (par F)))

lem:star-face-mesh(b): a new 2-cell is contained in its parent 2-cell, so refinement cannot increase the diameter of a 2-cell.

theorem Schoenflies.CellStructure.Realization.Refines.diam_cell_le_of_forall {γ : Type u_1} {S S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} {D : Set Plane} {η : ℝ} (href : R'.Refines R par) (h : R.IsCellDecomposition D) (hD : Bornology.IsBounded D) (hdiam : ∀ ⦃F : γ⦄, F ∈ S.faces → Metric.diam (closure (R.cell F)) ≤ η) {F : γ} (hF : F ∈ S'.faces) : Metric.diam (closure (R'.cell F)) ≤ η

lem:star-face-mesh(b): refinement cannot increase the maximum diameter of the 2-cells.

Finite cell neighborhoods

def Schoenflies.CellStructure.Realization.cellNbhd {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (x : Plane) : Set Plane

The finite cell neighbourhood of lem:cell-neighborhood: the complement of the union of all closed cells that do not contain x. It is open, contains x, and its points have carriers above the carrier of x.

Equations

• R.cellNbhd x = (⋃ τ ∈ {τ : γ | τ ∈ S.cells ∧ x ∉ closure (R.cell τ)}, closure (R.cell τ))ᶜ

theorem Schoenflies.CellStructure.Realization.isOpen_cellNbhd {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (x : Plane) : IsOpen (R.cellNbhd x)

theorem Schoenflies.CellStructure.Realization.mem_cellNbhd_self {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (x : Plane) : x ∈ R.cellNbhd x

theorem Schoenflies.CellStructure.Realization.cellNbhd_mem_nhds {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (x : Plane) : R.cellNbhd x ∈ nhds x

theorem Schoenflies.CellStructure.Realization.mem_closure_of_mem_cellNbhd {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {x z : Plane} {τ : γ} (hτ : τ ∈ S.cells) (hz : z ∈ R.cellNbhd x) (hzτ : z ∈ closure (R.cell τ)) : x ∈ closure (R.cell τ)

Every closed cell that meets the neighbourhood contains x.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_carrier_of_mem_cellNbhd {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x z : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hx : x ∈ D) (hz : z ∈ R.cellNbhd x) (hzD : z ∈ D) : S.sub (R.carrier x) (R.carrier z)

lem:cell-neighborhood, the carrier half: for z in the neighbourhood, the carrier of x is a subcell of the carrier of z.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_neighborhood {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {x z : Plane} [Nonempty γ] (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (hx : x ∈ D) (hz : z ∈ R.cellNbhd x) (hzD : z ∈ D) : S.sub (R.carrier x) (R.carrier z) ∧ R.star (R.carrier z) ⊆ R.star (R.carrier x)

lem:cell-neighborhood: R.cellNbhd x ∩ D is a relative neighbourhood of x in the closed domain on which the carrier of x is a subcell of every carrier, so that the stars there are all contained in the star of x.

For the cross-realization form the limit map needs — T_n(z) ⊆ T_n(x), the target star of the source carrier — combine sub_carrier_of_mem_cellNbhd in the source realization with star_anti_of_sub in the target one: the subcell relation is a relation of the common abstract structure, so it moves between realizations without transport.

Corresponding skeleton points

The second sentence of lem:refinement-compatibility(c). A point of the realized skeleton lies in an open 0-cell or an open 1-cell, and the skeleton homeomorphism carries each of those onto the open cell of the same abstract name; so corresponding skeleton points have carriers that correspond, with nothing to transport.

theorem Schoenflies.CellStructure.Realization.pos_pair_subset_edgeArc {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) {e a b : γ} (hl : S.skel.IsLink e a b) : {R.pos a, R.pos b} ⊆ Graph.edgeArc R.drawing e

The two ends of a drawn edge lie on its arc. Needed to cut the two endpoints out of the arc on both sides of the skeleton homeomorphism at once.

theorem Schoenflies.CellStructure.SkeletonHomeo.image_cell {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {σ : γ} (g : SkeletonHomeo R₁ R₂) (hσ : σ ∈ S.skel.vertexSet ∪ S.skel.edgeSet) : g.toFun '' R₁.cell σ = R₂.cell σ

The skeleton homeomorphism carries open skeleton cells onto open skeleton cells of the same abstract name. For a 0-cell this is pos_apply; for a 1-cell it is edgeArc_image with the two endpoints removed from both sides, which is legitimate because g is injective on the skeleton.

theorem Schoenflies.CellStructure.SkeletonHomeo.carrier_congr {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ : Set Plane} {σ : γ} {x : Plane} [Nonempty γ] (g : SkeletonHomeo R₁ R₂) (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) (hσ : σ ∈ S.skel.vertexSet ∪ S.skel.edgeSet) (hx : x ∈ R₁.cell σ) : R₂.carrier (g.toFun x) = R₁.carrier x

lem:refinement-compatibility(c), the skeleton clause: corresponding skeleton points have corresponding carriers — the same abstract cell on both sides.

The two elementary operations produce refinements

Both operations have the same shape: a single cell c is replaced by a set N of fresh cells, and the parent map sends N to c and fixes everything else. refines_of_elementary proves the geometric clause of Refines from that shape alone — the fresh cells must land inside c, because any other cell of the old stage survives and is unmoved, and open cells of one stage are disjoint.

theorem Schoenflies.CellStructure.refines_of_elementary {γ : Type u_1} {S S' : CellStructure γ} {R : S.Realization} {R' : S'.Realization} {par : γ → γ} {c : γ} {N : Set γ} {D : Set Plane} (hc : c ∈ S.cells) (hcells : S'.cells = S.cells \ {c} ∪ N) (hfresh : ∀ ⦃σ : γ⦄, σ ∈ N → σ ∉ S.cells) (hpar_new : ∀ ⦃σ : γ⦄, σ ∈ N → par σ = c) (hpar_old : ∀ ⦃σ : γ⦄, σ ∈ S.cells → par σ = σ) (hfaces : ∀ ⦃F : γ⦄, F ∈ S'.faces → par F ∈ S.faces) (hsub : ∀ ⦃σ τ : γ⦄, S'.sub σ τ → S.sub (par σ) (par τ)) (hcell_eq : ∀ ⦃σ : γ⦄, σ ∈ S.cells → σ ≠ c → R'.cell σ = R.cell σ) (h : R.IsCellDecomposition D) (h' : R'.IsCellDecomposition D) : R'.Refines R par

The shape shared by the two elementary operations. Given that the refined cells are the old ones minus c together with the fresh set N, that par collapses N to c and fixes old cells, and that both stages decompose the same closed domain with the surviving cells unmoved, the refined realization refines the old one.

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.refines {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} (hS : S.CombInvariants) {R : S.Realization} {R' : (S.subdivideEdge d).Realization} (href : d.IsRefinement R R') : R'.Refines R d.parent

An edge subdivision is a refinement. SubdivData.IsRefinement already carries everything the geometric clause needs, so no cell decomposition is required here.

theorem Schoenflies.CellStructure.SplitData.refines {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} (hS : S.CombInvariants) {R : S.Realization} {R' : (S.splitFace d).Realization} {D : Set Plane} (h : R.IsCellDecomposition D) (h' : R'.IsCellDecomposition D) (hcell_eq : ∀ ⦃σ : γ⦄, σ ∈ S.cells → σ ≠ d.face → R'.cell σ = R.cell σ) : R'.Refines R d.parent

A 2-cell split is a refinement. The geometric input is assertion (i) at the refined stage together with "the split leaves the other cells where they were"; both are supplied by the consumer, since the split analogue of SubdivData.IsRefinement is not yet on main.

The interface, exercised

The limit homeomorphism opens with: "the sets T_n(x) are nonempty and compact … the cell-star inclusion gives T_{n+1}(x) ⊆ T_n(x) … their diameters tend to zero … by lem:nested-compact their intersection is one point". This anonymous example is a machine-checked statement that the four facts that sentence needs come out of this module for an abstract nested sequence: nothing below mentions how the stages were built, and the mesh hypothesis is read in the target realization while the carrier is read in the source one.