From a sequence of transferred stages to a LimitTower

Two interfaces in this library were designed from opposite ends and have never met.

• Schoenflies.GeneratedPair (FiniteTransfer.lean) is what thm:finite-transfer consumes and produces: one abstract cell structure, its two realizations, the skeleton homeomorphism, the two cell decompositions, and weak admissibility on both sides.
• Schoenflies.CellStructure.LimitTower (LimitMap.lean) is what the limit section consumes: the same data indexed by ℕ, plus the nesting and the two halves of prop:shrinking-stars.

This module joins them. Schoenflies.StageSequence is a sequence of GeneratedPairs carrying exactly the extra data the recursion of quantitative-refinement produces at each step — the shared parent map, the growth of the source skeleton, the nesting of the skeleton maps, and the two shrinking estimates — and StageSequence.limitTower turns one into a LimitTower for the concrete source and target of the problem.

Every field is either read off a GeneratedPair or is one of the four recorded facts about the concrete domains. The point of writing it before the recursion exists is that it pins the interface down: the recursion now has a single named target, and any mismatch between what thm:finite-transfer delivers and what the limit section demands shows up here rather than at the end. Two such mismatches would otherwise have been easy to miss, and both check out:

• LimitTower wants the same parent map on both sides (srcRefines and tgtRefines along one par n). IsPartialTransferOf delivers exactly that — its refines_src and refines_tgt share par — which is lem:refinement-compatibility(c).
• LimitTower wants the two cell decompositions against closed domains C ∪ D and Q, and GeneratedPair is parametrized by exactly those two sets.

The four facts about the concrete domains

LimitTower asks for the source domain to be closed and bounded and its interior open, and the same for the target. On the source side IsSeparating C gives all three: Schoenflies.isClosed_union_inside, Schoenflies.union_inside_sdiff with IsSeparating.isOpen_inside, and boundedness through C = frontier (inside C) ⊆ closure (inside C) — which is why isBounded_dom needs no extra hypothesis, though LimitMap.lean warns that it is not optional (Metric.diam is 0 on an unbounded set). On the target side they are the standard facts about the square.

Blueprint

• Schoenflies.StageSequence — the output of the recursion of the section Quantitative refinement: the stage-n matched cellulations (Γ_n, Γ'_n) with their parent maps and the two convergence statements of prop:shrinking-stars.
• Schoenflies.StageSequence.limitTower — the passage to the head of the section The limit homeomorphism of the interiors, i.e. to tex 2568's "we now forget how the decompositions were constructed".
• Schoenflies.StageSequence.isHomeoOn_F, .interior_homeomorphism — prop:interior-homeomorphism for a stage sequence, which is the third conjunct of Schoenflies.HasLimitHomeomorphism.

The concrete domains

LimitTower is stated for arbitrary closed domains; the construction uses two. These are the facts it asks about them, collected so that limitTower below reads as a repackaging.

theorem Schoenflies.isBounded_union_inside {C : Set Plane} (hC : IsSeparating C) : Bornology.IsBounded (C ∪ inside C)

The closed Jordan domain is bounded. IsSeparating does not say so directly — it says the inside is bounded — but C is the frontier of the inside, hence inside its closure.

theorem Schoenflies.isOpen_union_inside_sdiff {C : Set Plane} (hC : IsSeparating C) : IsOpen ((C ∪ inside C) \ C)

The interior of the closed Jordan domain is open — after the rewriting LimitTower needs, which asks for IsOpen (dom \ bdry) rather than IsOpen (inside C).

theorem Schoenflies.isOpen_closedSquare_sdiff_modelCurve : IsOpen (Plane.closedSquare 0 1 \ modelCurve)

The interior of the closed square is open, in the same shape.

A sequence of transferred stages

structure Schoenflies.StageSequence (γ : Type u_2) [Nonempty γ] (S₀ : CellStructure γ) (C : Set Plane) : Type u_2

The output of the recursion of Quantitative refinement.

A sequence of generated matched cellulations of the closed Jordan domain and the closed square, each refining its predecessor along one parent map shared by the two sides, with growing source skeletons, nested skeleton maps, and the two convergence statements of prop:shrinking-stars.

Every field beyond stage and base is something the recursion establishes at the step that produces it; none is a property of a single stage, which is why they cannot live in GeneratedPair.

• stage : ℕ → GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

  The stage-n matched cellulation (Γ_n, Γ'_n), with both realizations.

• par : ℕ → γ → γ

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

• transition (n : ℕ) : StageTransition (self.stage (n + 1)) (self.stage n) (self.par n)

  Both compatible refinements, source-skeleton growth, and nesting of the skeleton maps.

• eps : ℕ → ℝ

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

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

  prop:shrinking-stars, the uniform half.

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

  …and the mesh tends to zero.

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

  prop:shrinking-stars, the pointwise half.

• base : S₀.CombInvariants

  The combinatorial invariants hold at the base of def:generated-structure; every stage inherits them by GeneratedPair.combInvariants.

• isSeparating : IsSeparating C

  C separates the plane — thm:jordan, which the caller has.

theorem Schoenflies.StageSequence.refines_src {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) (n : ℕ) : (T.stage (n + 1)).src.Refines (T.stage n).src (T.par n)

Consecutive source realizations refine along the recorded parent map.

theorem Schoenflies.StageSequence.refines_tgt {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) (n : ℕ) : (T.stage (n + 1)).tgt.Refines (T.stage n).tgt (T.par n)

The target realizations refine along the same parent map.

theorem Schoenflies.StageSequence.skeletonSet_mono {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) (n : ℕ) : (T.stage n).src.skeletonSet ⊆ (T.stage (n + 1)).src.skeletonSet

The realized source skeletons grow from one stage to the next.

theorem Schoenflies.StageSequence.skelHomeo_succ {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) (n : ℕ) : Set.EqOn (T.stage (n + 1)).homeo.toFun (T.stage n).homeo.toFun (T.stage n).src.skeletonSet

Consecutive skeleton homeomorphisms agree on the preceding source skeleton.

def Schoenflies.StageSequence.limitTower {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) : CellStructure.LimitTower γ

The tower the limit section consumes. Every field is read off the stages or is one of the four facts about the two concrete domains; there is no mathematics here beyond the two recorded above.

Equations

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

@[simp]

theorem Schoenflies.StageSequence.limitTower_region {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) : T.limitTower.region = inside C

@[simp]

theorem Schoenflies.StageSequence.limitTower_region' {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) : T.limitTower.region' = Plane.openSquare 0 1

theorem Schoenflies.StageSequence.isHomeoOn_F {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) : IsHomeoOn T.limitTower.F T.limitTower.inv (inside C) (Plane.openSquare 0 1)

prop:interior-homeomorphism for a stage sequence, in the Schoenflies.IsHomeoOn shape Schoenflies.HasLimitHomeomorphism asks for: the limit map is a homeomorphism of the open Jordan domain onto the open square.

theorem Schoenflies.StageSequence.F_eq_skelHomeo {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} (T : StageSequence γ S₀ C) {n : ℕ} {x : Plane} (hx : x ∈ (T.stage n).src.skeletonSet) (hxD : x ∈ C ∪ inside C) : T.limitTower.F x = (T.stage n).homeo.toFun x

prop:skeleton-agreement for a stage sequence: on the closed domain the limit map agrees with every stage's skeleton homeomorphism wherever that stage's skeleton reaches.

This is the bridge that will discharge Schoenflies.HasAnchorCrosscuts: the crosscut a stage produces between two anchors lies in that stage's skeleton, so F carries it to the target crosscut by the finite map, and Schoenflies.image_sdiff_eq_of_eqOn finishes.