The limit homeomorphism of the interiors

The blueprint opens this section with a sentence that is an instruction to the formalizer: "We now forget how the decompositions were constructed and use only their nesting, matching, and shrinking properties." This module takes it literally. LimitTower is a structure recording exactly those properties — a sequence of matched cell structures with two realizations each, a Realization.Refines instance between consecutive stages on each side sharing one parent map, nested skeleton homeomorphisms, and the two shrinking hypotheses of prop:shrinking-stars — and everything from the definition of F to prop:interior-homeomorphism is proved against it. Nothing below mentions a mesh, a grid, or a constructor. The still-open construction has to produce one LimitTower; none of the analysis waits for it.

What is not a field

Three things the task list expected to appear as hypotheses turned out to be derivable and are therefore proved here rather than assumed.

• lem:outer-incidence. docs/ROADMAP.md records it as done in CombinatorialInvariance.lean under outerEdge_face_corresponds; that is a different statement (assertion (vi) of lem:cellulation-invariants, transported). The real lem:outer-incidence — closure σ meets C iff some outer cell is a subcell of σ iff closure σ' meets S — is proved below as Realization.IsCellDecomposition.closure_cell_meets_outer_iff and, for stars, LimitTower.star_meets_bdry_iff. The one geometric input it needs is Realization.outerSet_eq_iUnion_cell: the realized outer cycle is exactly the union of the open cells of the outer cells, which is a consequence of the two Realization clauses cell_vertex and cell_edge and holds for any subcomplex.
• Assertion (vii) of lem:cellulation-invariants (every 2-cell boundary a Jordan curve with the open cell its bounded region). The limit argument was expected to need it, through assertion (viii). It does not: the only use is "a 2-cell is not a proper subcell of a 2-cell", and that is CombInvariants.face_maximal, which is already an inductive invariant on main. There is therefore no field for (vii) and no dependency on it.
• prop:target-skeleton-dense. The blueprint's surjectivity proof goes through the density of the target skeleton and a compactness argument in C ∪ D. That is not needed: the sets ⋂ₙ St_{Γₙ}(car_{Γ'ₙ}(y)) — the source stars of the target carriers of y — are a nested sequence of nonempty compacts, and any point of their intersection is already a preimage of y. prop:target-skeleton-dense is proved anyway, because the boundary-continuity module cites it, but it is not on the critical path to prop:F-surjective.

The two shrinking hypotheses are not symmetric

prop:shrinking-stars gives pointwise convergence of the source star diameters and uniform convergence of the target ones. The asymmetry is real and is used: F is defined, and continuous, on the whole closed domain (only the uniform bound enters), whereas injectivity and the continuity of the inverse hold on the open region (they need the pointwise bound at a point of D).

One hypothesis that the blueprint does not state is carried throughout: the closed domains are bounded. It is not optional — Metric.diam is 0 on an unbounded set, so without it the star diameter bounds are false rather than weak — and it is trivially true for a closed Jordan domain.

Blueprint

All of the following live in Schoenflies.CellStructure.

• LimitTower — the abstraction of the head of the section: "we now forget how the decompositions were constructed and use only their nesting, matching, and shrinking properties".
• The definition of F (tex "The limit homeomorphism of the interiors") — LimitTower.F, with LimitTower.iInter_tgtStar_eq its characterisation (lem:nested-compact applied to the nested stars LimitTower.tgtStar), LimitTower.F_mem_tgtStar and LimitTower.eq_F_of_mem_iInter.
• lem:outer-incidence — Realization.IsCellDecomposition.closure_cell_meets_outer_iff and Realization.IsCellDecomposition.star_meets_outer_iff, with the matched form the limit argument cites, LimitTower.star_meets_bdry_iff. Their geometric input is Realization.outerSet_eq_iUnion_cell.
• prop:skeleton-agreement — LimitTower.F_eq_skelHomeo.
• prop:F-continuous — LimitTower.continuousOn_F, on the closed domain.
• prop:image-interior — LimitTower.F_mem_region'.
• prop:F-injective — LimitTower.injOn_F.
• prop:target-skeleton-dense — LimitTower.exists_mem_tgt_skeletonSet.
• prop:F-surjective — LimitTower.exists_mem_region_F_eq, through LimitTower.preStar and LimitTower.F_eq_of_mem_iInter_preStar.
• lem:exact-cell-correspondence — LimitTower.image_cell, with the corollary the inverse argument actually uses, LimitTower.tgt_carrier_F.
• prop:inverse-continuous — LimitTower.continuousOn_inv, on the explicit inverse LimitTower.inv.
• prop:interior-homeomorphism — LimitTower.isHomeoOn_F and, with the skeleton clause, LimitTower.interior_homeomorphism; in the Schoenflies.IsHomeoOn shape that Endgame.lean and the boundary-continuity module consume.
• lem:cell-neighborhood is used, not restated: it is Realization.IsCellDecomposition.sub_carrier_of_mem_cellNbhd in RefinementStars.lean, and the cross-realization form the limit map needs is LimitTower.tgtStar_subset_of_mem_cellNbhd.

The realized skeleton and outer cycle, cell by cell

Realization.skeletonSet and Realization.outerSet are defined as point sets of drawn graphs. The limit argument needs them as unions of open cells, because that is the form in which they interact with IsCellDecomposition: "the carrier of any point of C is an outer cell" is the first sentence of the blueprint's proof of lem:outer-incidence, and it is exactly this rewriting.

theorem Schoenflies.CellStructure.outerCells_subset_cells {γ : Type u_1} {S : CellStructure γ} : S.outerCells ⊆ S.cells

Every outer cell is a cell.

theorem Schoenflies.CellStructure.mem_faces_of_notMem_skel {γ : Type u_1} {S : CellStructure γ} {σ : γ} (hσ : σ ∈ S.cells) (h : σ ∉ S.skel.vertexSet ∪ S.skel.edgeSet) : σ ∈ S.faces

A cell that is neither a 0-cell nor a 1-cell of the skeleton is a 2-cell — the three collections exhaust cells.

theorem Schoenflies.CellStructure.mem_skel_of_sub_face {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) {σ F : γ} (hσ : σ ∈ S.cells) (hsub : S.sub σ F) (hne : σ ≠ F) : σ ∈ S.skel.vertexSet ∪ S.skel.edgeSet

A proper subcell of a 2-cell is a 0- or 1-cell: nothing but the 2-cell itself is a 2-cell below it.

theorem Schoenflies.CellStructure.notMem_outerCells_of_mem_faces {γ : Type u_1} {S : CellStructure γ} {F : γ} (hF : F ∈ S.faces) : F ∉ S.outerCells

A 2-cell is never an outer cell: outer cells are 0- and 1-cells of the skeleton.

theorem Schoenflies.CellStructure.notMem_outerCells_of_nonboundary_edge {γ : Type u_1} {S : CellStructure γ} {f : γ} (hf : f ∈ S.skel.edgeSet) (h : f ∉ S.outerGraph.edgeSet) : f ∉ S.outerCells

A nonboundary edge — assertion (iii) of lem:cellulation-invariants produces one on every 2-cell boundary — is not an outer cell.

theorem Schoenflies.CellStructure.Realization.pointSet_map_eq_iUnion_cell {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) {H : Graph γ γ} (hH : H ≤ S.skel) : (Graph.map R.pos H).pointSet R.drawing = ⋃ κ ∈ H.vertexSet ∪ H.edgeSet, R.cell κ

The realized point set of a subcomplex of the skeleton is the union of the open cells of its 0- and 1-cells. A drawn edge is its open cell together with the two 0-cells at its ends, and those ends belong to the subcomplex whenever the edge does.

theorem Schoenflies.CellStructure.Realization.skeletonSet_eq_iUnion_cell {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.skeletonSet = ⋃ κ ∈ S.skel.vertexSet ∪ S.skel.edgeSet, R.cell κ

The realized 1-skeleton is the union of the open 0- and 1-cells.

theorem Schoenflies.CellStructure.Realization.outerSet_eq_iUnion_cell {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.outerSet = ⋃ κ ∈ S.outerCells, R.cell κ

The realized outer cycle is the union of the open outer cells. This is the sentence "C is exactly the union of the outer vertices and the open outer edges" at the head of the blueprint's proof of lem:outer-incidence.

theorem Schoenflies.CellStructure.Realization.cell_subset_outerSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {κ : γ} (hκ : κ ∈ S.outerCells) : R.cell κ ⊆ R.outerSet

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_disjoint_outerSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hout : σ ∉ S.outerCells) : Disjoint (R.cell σ) R.outerSet

Off the outer cycle, the open cell of a cell that is not an outer cell. Open cells are disjoint and the outer cycle is the union of the outer ones, so a cell's open part misses the outer cycle exactly when the cell is not outer.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_disjoint_biUnion {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) {K : Set γ} (hK : K ⊆ S.cells) (hnot : σ ∉ K) : Disjoint (R.cell σ) (⋃ κ ∈ K, R.cell κ)

An open cell is disjoint from the union of the open cells of any collection of cells not containing it. This is how IsCellDecomposition sees the realized skeleton and the realized outer cycle, once those have been rewritten as unions of open cells.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cell_disjoint_skeletonSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) {F : γ} (hF : F ∈ S.faces) : Disjoint (R.cell F) R.skeletonSet

An open 2-cell never meets the realized skeleton.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.skeletonSet_subset_domain {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) : R.skeletonSet ⊆ D

The realized skeleton lies in the closed domain.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_face_eq_closure {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) {F : γ} (hF : F ∈ S.faces) : R.star F = closure (R.cell F)

The closed star of a 2-cell is its own closed cell. By lem:star-face-mesh a closed star is the union of the closed 2-cells above the cell, and CombInvariants.face_maximal says the only 2-cell above a 2-cell is itself. This is the step the blueprint attributes to assertion (viii) of lem:cellulation-invariants, and it needs neither (vii) nor openness of the open 2-cell.

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

The carrier of a point of the realized outer cycle is an outer cell.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.closure_cell_meets_outer_iff {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) : (closure (R.cell τ) ∩ R.outerSet).Nonempty ↔ ∃ κ ∈ S.outerCells, S.sub κ τ

lem:outer-incidence, the closed-cell form: a closed cell meets the realized outer cycle exactly when some outer cell is one of its subcells. The middle condition is a statement of the abstract structure alone, which is what makes the equivalence transfer between the two realizations with nothing to transport.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.star_meets_outer_iff {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) (hS : S.CombInvariants) (σ : γ) : (R.star σ ∩ R.outerSet).Nonempty ↔ ∃ (τ : γ), S.sub σ τ ∧ ∃ κ ∈ S.outerCells, S.sub κ τ

lem:outer-incidence, the star form: a closed star meets the realized outer cycle exactly when some supercell of the cell has an outer subcell.

The tower of matched cellulations

Every field below is an obligation on whoever eventually constructs the sequence of decompositions, and there is nothing here that the limit argument does not use.

structure Schoenflies.CellStructure.LimitTower (γ : Type u_2) [Nonempty γ] : Type u_2

The nesting, matching and shrinking properties of a sequence of matched cellulations, and nothing else. The blueprint's "we now forget how the decompositions were constructed" is this structure.

str n is the stage-n abstract matched cell structure; src n and tgt n are its two realizations, in the closed Jordan domain dom and in the closed square dom'; skelHomeo n is the stage-n skeleton homeomorphism g_n. Consecutive stages are related by a pair of Realization.Refines instances sharing one parent map par n — that sharing is lem:refinement-compatibility(c), "corresponding cells have corresponding parents", under the representation of CombinatorialInvariance.lean, where cells are abstract names.

The shrinking clauses are prop:shrinking-stars, and they are deliberately asymmetric, exactly as the blueprint states them: the target star diameters are bounded uniformly by a null sequence eps, while the source star diameters are only assumed to tend to zero pointwise, and only at points of the open region.

• str : ℕ → CellStructure γ

  The stage-n abstract matched cell structure.

• src (n : ℕ) : (self.str n).Realization

  The source realization, in the closed Jordan domain.

• tgt (n : ℕ) : (self.str n).Realization

  The target realization, in the closed square.

• skelHomeo (n : ℕ) : SkeletonHomeo (self.src n) (self.tgt n)

  The stage-n skeleton homeomorphism g_n.

• par : ℕ → γ → γ

  The composite parent map from stage n + 1 to stage n, shared by the two sides.

• dom : Set Plane

  The closed source domain C ∪ D.

• bdry : Set Plane

  The source outer curve C.

• dom' : Set Plane

  The closed target domain Q.

• bdry' : Set Plane

  The target outer curve S.

• eps : ℕ → ℝ

  The uniform target mesh: 2 ε_n of the blueprint.

• srcDecomp (n : ℕ) : (self.src n).IsCellDecomposition self.dom

  Assertions (i) and (ii) on the source side.

• tgtDecomp (n : ℕ) : (self.tgt n).IsCellDecomposition self.dom'

  Assertions (i) and (ii) on the target side.

• comb (n : ℕ) : (self.str n).CombInvariants

  Assertions (iii), (v), (vi) and the rest of the combinatorial invariants.

• srcRefines (n : ℕ) : (self.src (n + 1)).Refines (self.src n) (self.par n)

  Consecutive source stages refine, along par n.

• tgtRefines (n : ℕ) : (self.tgt (n + 1)).Refines (self.tgt n) (self.par n)

  Consecutive target stages refine, along the same par n.

• srcOuterSet (n : ℕ) : (self.src n).outerSet = self.bdry

  The realized source outer cycle is C, at every stage.

• tgtOuterSet (n : ℕ) : (self.tgt n).outerSet = self.bdry'

  The realized target outer cycle is S, at every stage.

• isClosed_dom : IsClosed self.dom

  C ∪ D is closed.

• isClosed_dom' : IsClosed self.dom'

  Q is closed.

• isBounded_dom : Bornology.IsBounded self.dom

  C ∪ D is bounded. Not in the blueprint, and not optional: Metric.diam is 0 on an unbounded set.

• isBounded_dom' : Bornology.IsBounded self.dom'

  Q is bounded, for the same reason.

• isOpen_int : IsOpen (self.dom \ self.bdry)

  D = Int(C) is open.

• isOpen_int' : IsOpen (self.dom' \ self.bdry')

  Q° is open.

• skeletonSet_mono (n : ℕ) : (self.src n).skeletonSet ⊆ (self.src (n + 1)).skeletonSet

  The realized source skeletons grow.

• skelHomeo_succ (n : ℕ) : Set.EqOn (self.skelHomeo (n + 1)).toFun (self.skelHomeo n).toFun (self.src n).skeletonSet

  The skeleton maps are nested: "an edge subdivision leaves the skeleton map unchanged as a point map, and a 2-cell split extends it by the chosen homeomorphism on the new ear".

• diam_tgtStar_le (n : ℕ) ⦃σ : γ⦄ : σ ∈ (self.str n).cells → Metric.diam ((self.tgt n).star σ) ≤ self.eps n

  prop:shrinking-stars, the uniform half: every stage-n target star has diameter at most eps n.

• tendsto_eps : Filter.Tendsto self.eps Filter.atTop (nhds 0)

  …and eps is a null sequence.

• tendsto_diam_srcStar ⦃x : Plane⦄ : x ∈ self.dom \ self.bdry → Filter.Tendsto (fun (n : ℕ) => Metric.diam ((self.src n).star ((self.src n).carrier x))) Filter.atTop (nhds 0)

  prop:shrinking-stars, the pointwise half: at every point of the open region the source star diameters tend to zero.

def Schoenflies.CellStructure.LimitTower.region {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : Set Plane

The open source region D = Int(C).

Equations

• L.region = L.dom \ L.bdry

def Schoenflies.CellStructure.LimitTower.region' {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : Set Plane

The open target region Q°.

Equations

• L.region' = L.dom' \ L.bdry'

def Schoenflies.CellStructure.LimitTower.tgtStar {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (n : ℕ) (x : Plane) : Set Plane

St_{Γ'_n}(σ'_n(x)), written T_n(x) in the blueprint: the closed target star of the cell corresponding to the source carrier of x.

Equations

• L.tgtStar n x = (L.tgt n).star ((L.src n).carrier x)

def Schoenflies.CellStructure.LimitTower.srcStar {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (n : ℕ) (x : Plane) : Set Plane

St_{Γ_n}(x), the closed source star of the source carrier of x.

Equations

• L.srcStar n x = (L.src n).star ((L.src n).carrier x)

theorem Schoenflies.CellStructure.LimitTower.mem_region_iff {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} : x ∈ L.region ↔ x ∈ L.dom ∧ x ∉ L.bdry

theorem Schoenflies.CellStructure.LimitTower.mem_region'_iff {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} : x ∈ L.region' ↔ x ∈ L.dom' ∧ x ∉ L.bdry'

theorem Schoenflies.CellStructure.LimitTower.region_subset_dom {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} : L.region ⊆ L.dom

theorem Schoenflies.CellStructure.LimitTower.region'_subset_dom' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} : L.region' ⊆ L.dom'

theorem Schoenflies.CellStructure.LimitTower.isOpen_region {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : IsOpen L.region

theorem Schoenflies.CellStructure.LimitTower.isOpen_region' {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : IsOpen L.region'

theorem Schoenflies.CellStructure.LimitTower.tgtStar_eq {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (x : Plane) : L.tgtStar n x = (L.tgt n).star ((L.src n).carrier x)

theorem Schoenflies.CellStructure.LimitTower.srcStar_eq {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (x : Plane) : L.srcStar n x = (L.src n).star ((L.src n).carrier x)

theorem Schoenflies.CellStructure.LimitTower.exists_lt_of_tendsto_zero {f : ℕ → ℝ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} (hr : 0 < r) : ∃ (n : ℕ), f n < r

A null real sequence is eventually below any positive bound. Used with eps and with the pointwise source-star diameters.

Stars of the tower

theorem Schoenflies.CellStructure.LimitTower.srcStar_subset_dom {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (σ : γ) : (L.src n).star σ ⊆ L.dom

theorem Schoenflies.CellStructure.LimitTower.tgtStar_subset_dom' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (σ : γ) : (L.tgt n).star σ ⊆ L.dom'

theorem Schoenflies.CellStructure.LimitTower.isBounded_tgt_star {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (σ : γ) : Bornology.IsBounded ((L.tgt n).star σ)

theorem Schoenflies.CellStructure.LimitTower.isBounded_src_star {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (σ : γ) : Bornology.IsBounded ((L.src n).star σ)

theorem Schoenflies.CellStructure.LimitTower.isBounded_srcStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (x : Plane) : Bornology.IsBounded (L.srcStar n x)

theorem Schoenflies.CellStructure.LimitTower.isBounded_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (x : Plane) : Bornology.IsBounded (L.tgtStar n x)

theorem Schoenflies.CellStructure.LimitTower.mem_srcStar_self {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) (n : ℕ) : x ∈ L.srcStar n x

theorem Schoenflies.CellStructure.LimitTower.tendsto_diam_srcStar_point {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) : Filter.Tendsto (fun (n : ℕ) => Metric.diam (L.srcStar n x)) Filter.atTop (nhds 0)

theorem Schoenflies.CellStructure.LimitTower.tgtStar_succ_subset {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) (n : ℕ) : L.tgtStar (n + 1) x ⊆ L.tgtStar n x

lem:refinement-compatibility(b) at a point: T_{n+1}(x) ⊆ T_n(x).

theorem Schoenflies.CellStructure.LimitTower.tgtStar_antitone {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : Antitone fun (n : ℕ) => L.tgtStar n x

theorem Schoenflies.CellStructure.LimitTower.tgtStar_nonempty {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) (n : ℕ) : (L.tgtStar n x).Nonempty

theorem Schoenflies.CellStructure.LimitTower.isCompact_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (x : Plane) : IsCompact (L.tgtStar n x)

theorem Schoenflies.CellStructure.LimitTower.diam_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) (n : ℕ) : Metric.diam (L.tgtStar n x) ≤ L.eps n

theorem Schoenflies.CellStructure.LimitTower.tendsto_diam_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : Filter.Tendsto (fun (n : ℕ) => Metric.diam (L.tgtStar n x)) Filter.atTop (nhds 0)

The limit map

theorem Schoenflies.CellStructure.LimitTower.exists_eq_singleton_iInter_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : ∃ (p : Plane), ⋂ (n : ℕ), L.tgtStar n x = {p}

noncomputable def Schoenflies.CellStructure.LimitTower.F {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (x : Plane) : Plane

The limit map F: the unique point of ⋂ₙ T_n(x). Junk off the closed domain; every lemma about it carries x ∈ L.dom.

Equations

• L.F x = if h : ∃ (p : Schoenflies.Plane), ⋂ (n : ℕ), L.tgtStar n x = {p} then h.choose else 0

theorem Schoenflies.CellStructure.LimitTower.iInter_tgtStar_eq {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : ⋂ (n : ℕ), L.tgtStar n x = {L.F x}

The characterising property of F.

theorem Schoenflies.CellStructure.LimitTower.F_mem_iInter {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : L.F x ∈ ⋂ (n : ℕ), L.tgtStar n x

theorem Schoenflies.CellStructure.LimitTower.F_mem_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) (n : ℕ) : L.F x ∈ L.tgtStar n x

theorem Schoenflies.CellStructure.LimitTower.eq_F_of_mem_iInter {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x z : Plane} (hx : x ∈ L.dom) (hz : ∀ (n : ℕ), z ∈ L.tgtStar n x) : z = L.F x

Uniqueness: anything in every T_n(x) is F x.

theorem Schoenflies.CellStructure.LimitTower.F_mem_dom' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.dom) : L.F x ∈ L.dom'

theorem Schoenflies.CellStructure.LimitTower.dist_F_le_of_mem_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x z : Plane} {n : ℕ} (hx : x ∈ L.dom) (hz : z ∈ L.tgtStar n x) : dist (L.F x) z ≤ L.eps n

F x is within eps n of anything in the stage-n target star of x.

Agreement with the finite skeleton maps

The skeleton maps are nested, so g_n = g_N on G_N for every n ≥ N; at each such stage the skeleton map carries the carrier of x onto the corresponding target cell, which sits inside T_n(x). The intersection of the T_n(x) is the single point F x.

theorem Schoenflies.CellStructure.LimitTower.skeletonSet_mono_le {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {m n : ℕ} (hmn : m ≤ n) : (L.src m).skeletonSet ⊆ (L.src n).skeletonSet

theorem Schoenflies.CellStructure.LimitTower.skelHomeo_eqOn {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {m n : ℕ} (hmn : m ≤ n) : Set.EqOn (L.skelHomeo n).toFun (L.skelHomeo m).toFun (L.src m).skeletonSet

The skeleton maps are nested: g_n = g_m on G_m whenever m ≤ n.

theorem Schoenflies.CellStructure.LimitTower.skelHomeo_mem_tgtStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} {n : ℕ} (hx : x ∈ (L.src n).skeletonSet) : (L.skelHomeo n).toFun x ∈ L.tgtStar n x

At a stage-n skeleton point the skeleton map lands in the stage-n target star: the carrier of x is a 0- or 1-cell, and g_n carries its open cell onto the target open cell of the same abstract name.

theorem Schoenflies.CellStructure.LimitTower.F_eq_skelHomeo {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} {n : ℕ} (hx : x ∈ (L.src n).skeletonSet) (hxD : x ∈ L.dom) : L.F x = (L.skelHomeo n).toFun x

prop:skeleton-agreement: F agrees with the stage-N skeleton map on G_N ∩ (C ∪ D). Since the skeleton maps are nested, this is the blueprint's F = g_∞ on ⋃ₙ Gₙ ∩ D as well.

Continuity

theorem Schoenflies.CellStructure.LimitTower.tgtStar_subset_of_mem_cellNbhd {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x z : Plane} {n : ℕ} (hx : x ∈ L.dom) (hzD : z ∈ L.dom) (hz : z ∈ (L.src n).cellNbhd x) : L.tgtStar n z ⊆ L.tgtStar n x

The cross-realization form of lem:cell-neighborhood the limit map needs: for z in the stage-n source cell neighbourhood of x, T_n(z) ⊆ T_n(x). The subcell relation is read in the source realization and used in the target one; it is a relation of the common abstract structure, so nothing is transported.

theorem Schoenflies.CellStructure.LimitTower.continuousOn_F {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : ContinuousOn L.F L.dom

prop:F-continuous, on the whole closed domain. Only the uniform half of prop:shrinking-stars enters, so nothing here restricts x to the open region.

The image lies in the interior

theorem Schoenflies.CellStructure.LimitTower.star_meets_bdry_iff {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (n : ℕ) (σ : γ) : ((L.src n).star σ ∩ L.bdry).Nonempty ↔ ((L.tgt n).star σ ∩ L.bdry').Nonempty

lem:outer-incidence, matched form: a stage-n source star meets C exactly when the target star of the same abstract cell meets S. Both sides reduce to the middle condition of the blueprint's statement, which mentions only the abstract structure and its outer cycle.

theorem Schoenflies.CellStructure.LimitTower.exists_srcStar_subset_region {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) : ∃ (n : ℕ), L.srcStar n x ⊆ L.region

At a point of the open region the source star is eventually contained in the region: the point lies in its own star, and the star diameters tend to zero.

theorem Schoenflies.CellStructure.LimitTower.F_mem_region' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) : L.F x ∈ L.region'

prop:image-interior: F(D) ⊆ Q°.

Injectivity

theorem Schoenflies.CellStructure.LimitTower.injOn_F {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : Set.InjOn L.F L.region

prop:F-injective. This is where the pointwise half of prop:shrinking-stars is needed, and it is why injectivity is asserted on the open region rather than on the closed domain.

Density of the target skeleton

theorem Schoenflies.CellStructure.LimitTower.tgt_cell_subset_region' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) {σ : γ} (hσ : σ ∈ (L.str n).cells) (hout : σ ∉ (L.str n).outerCells) : (L.tgt n).cell σ ⊆ L.region'

An open cell that is not an outer cell lies in the open region: open cells are disjoint and S is the union of the open outer ones.

theorem Schoenflies.CellStructure.LimitTower.exists_mem_tgt_skeletonSet {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ), ∃ w ∈ (L.tgt n).skeletonSet, w ∈ L.region' ∧ dist y w < δ

prop:target-skeleton-dense: every point of Q° is approximated by target skeleton points of Q°. If y is not already on the stage-n skeleton its carrier is a 2-cell, and assertion (iii) of lem:cellulation-invariants puts a nonboundary edge on its boundary; that edge's open cell lies in the star of the carrier, of diameter at most eps n.

Surjectivity

The blueprint reaches y through the density of the target skeleton and a compactness argument in C ∪ D. The route taken here is shorter and needs neither: the source stars of the target carriers of y are themselves a nested sequence of nonempty compacts, and every point of their intersection is already a preimage of y.

def Schoenflies.CellStructure.LimitTower.preStar {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (n : ℕ) (y : Plane) : Set Plane

St_{Γ_n}(car_{Γ'_n}(y)): the source star of the target carrier of y. This is the set the blueprint calls K, read at every stage instead of at one.

Equations

• L.preStar n y = (L.src n).star ((L.tgt n).carrier y)

theorem Schoenflies.CellStructure.LimitTower.preStar_succ_subset {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.dom') (n : ℕ) : L.preStar (n + 1) y ⊆ L.preStar n y

theorem Schoenflies.CellStructure.LimitTower.preStar_nonempty {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.dom') (n : ℕ) : (L.preStar n y).Nonempty

theorem Schoenflies.CellStructure.LimitTower.isCompact_preStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) (y : Plane) : IsCompact (L.preStar n y)

theorem Schoenflies.CellStructure.LimitTower.nonempty_iInter_preStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.dom') : (⋂ (n : ℕ), L.preStar n y).Nonempty

theorem Schoenflies.CellStructure.LimitTower.F_eq_of_mem_iInter_preStar {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x y : Plane} (hy : y ∈ L.dom') (hxD : x ∈ L.dom) (hx : ∀ (n : ℕ), x ∈ L.preStar n y) : L.F x = y

The heart of surjectivity: a point lying in every preStar n y is carried to y. At each stage the source carrier of x and the target carrier of y share a supercell τ, so the two target stars meet, and both have diameter at most eps n.

theorem Schoenflies.CellStructure.LimitTower.exists_tgt_star_subset_region' {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') : ∃ (n : ℕ), (L.tgt n).star ((L.tgt n).carrier y) ⊆ L.region'

At a point of Q° the target star is eventually inside Q°. Here the uniform half of prop:shrinking-stars is what is available, and it suffices.

theorem Schoenflies.CellStructure.LimitTower.exists_mem_region_F_eq {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') : ∃ x ∈ L.region, L.F x = y

prop:F-surjective: every point of Q° is F of a point of D.

Exact cell correspondence

theorem Schoenflies.CellStructure.LimitTower.src_cell_subset_region {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) {σ : γ} (hσ : σ ∈ (L.str n).cells) (hout : σ ∉ (L.str n).outerCells) : (L.src n).cell σ ⊆ L.region

The source counterpart of tgt_cell_subset_region'.

theorem Schoenflies.CellStructure.LimitTower.src_carrier_notMem_outerCells {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) (n : ℕ) : (L.src n).carrier x ∉ (L.str n).outerCells

A point of the open region has a nonboundary carrier: an outer cell's open cell lies on the outer cycle.

theorem Schoenflies.CellStructure.LimitTower.tgt_carrier_notMem_outerCells {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') (n : ℕ) : (L.tgt n).carrier y ∉ (L.str n).outerCells

theorem Schoenflies.CellStructure.LimitTower.F_mem_cell_of_mem_cell_face {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (n : ℕ) {σ : γ} (hσ : σ ∈ (L.str n).faces) (hx : x ∈ (L.src n).cell σ) : L.F x ∈ (L.tgt n).cell σ

The half of lem:exact-cell-correspondence that carries the argument: an open source 2-cell is mapped into the corresponding open target 2-cell.

The closed star of a 2-cell is its own closed cell, so F x lies in closure σ'; if it lay on the frontier it would be a stage-n target skeleton point, and its skeleton preimage w would be a second point of D with F w = F x, contradicting injectivity — while x itself, lying in an open 2-cell, is not a skeleton point.

theorem Schoenflies.CellStructure.LimitTower.image_cell {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} (n : ℕ) {σ : γ} (hσ : σ ∈ (L.str n).cells) (hout : σ ∉ (L.str n).outerCells) : L.F '' (L.src n).cell σ = (L.tgt n).cell σ

lem:exact-cell-correspondence: F carries each nonboundary open cell of the stage-n source decomposition onto the corresponding open cell of the target decomposition. For a 0- or 1-cell this is prop:skeleton-agreement together with the skeleton homeomorphism; for a 2-cell it is the previous lemma plus surjectivity.

theorem Schoenflies.CellStructure.LimitTower.tgt_carrier_F {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) (n : ℕ) : (L.tgt n).carrier (L.F x) = (L.src n).carrier x

The corollary the inverse argument runs on: F matches carriers.

The inverse, and the interior homeomorphism

noncomputable def Schoenflies.CellStructure.LimitTower.inv {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) (y : Plane) : Plane

The inverse of F, as an explicit function Plane → Plane rather than a bundled Homeomorph: a chosen preimage in D. Surjectivity makes the choice possible and injectivity makes it irrelevant. Endgame.lean consumes the pair (F, inv) in the IsHomeoOn shape, which needs the inverse named.

Equations

• L.inv y = if h : ∃ x ∈ L.region, L.F x = y then h.choose else 0

theorem Schoenflies.CellStructure.LimitTower.inv_spec {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (h : ∃ x ∈ L.region, L.F x = y) : L.inv y ∈ L.region ∧ L.F (L.inv y) = y

theorem Schoenflies.CellStructure.LimitTower.inv_mem_region {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') : L.inv y ∈ L.region

theorem Schoenflies.CellStructure.LimitTower.F_inv {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') : L.F (L.inv y) = y

theorem Schoenflies.CellStructure.LimitTower.inv_F {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {x : Plane} (hx : x ∈ L.region) : L.inv (L.F x) = x

theorem Schoenflies.CellStructure.LimitTower.src_carrier_inv {γ : Type u_1} [Nonempty γ] {L : LimitTower γ} {y : Plane} (hy : y ∈ L.region') (n : ℕ) : (L.src n).carrier (L.inv y) = (L.tgt n).carrier y

tgt_carrier_F read at inv y.

theorem Schoenflies.CellStructure.LimitTower.continuousOn_inv {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : ContinuousOn L.inv L.region'

prop:inverse-continuous: F⁻¹ : Q° → D is continuous. lem:cell-neighborhood is applied on the target side; lem:exact-cell-correspondence, in the form src_carrier_inv, transports the resulting subcell relation to the source, where the source star of x is small.

theorem Schoenflies.CellStructure.LimitTower.isHomeoOn_F {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : IsHomeoOn L.F L.inv L.region L.region'

prop:interior-homeomorphism: F : Int(C) → Q° is a homeomorphism, in the Schoenflies.IsHomeoOn shape — the map, its explicit inverse, and the four laws on the two sets — that Endgame.lean and the boundary-continuity module consume.

theorem Schoenflies.CellStructure.LimitTower.image_region {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : L.F '' L.region = L.region'

theorem Schoenflies.CellStructure.LimitTower.interior_homeomorphism {γ : Type u_1} [Nonempty γ] (L : LimitTower γ) : IsHomeoOn L.F L.inv L.region L.region' ∧ ∀ (n : ℕ), ∀ x ∈ (L.src n).skeletonSet, x ∈ L.dom → L.F x = (L.skelHomeo n).toFun x

prop:interior-homeomorphism as the blueprint states it: a homeomorphism of Int(C) onto Q° that agrees with the stage-N skeleton map on G_N ∩ (C ∪ D) for every N.