Quantitative successor stages

The reverse half of the quantitative-refinement recursion is now a closed construction. From one generated pair over the closed Jordan domain and one requested positive bound, it selects an exact finite target-segment cover, a sufficiently fine square-mesh overlay, finitely many clean accessible boundary anchors, and the reverse finite transfer. Its target stars are smaller than the requested bound.

Blueprint

• Schoenflies.QuantitativeReverseStage — all construction data for one reverse quantitative successor.
• Schoenflies.exists_quantitativeReverseStage — construction from separation and the persistent outer-cycle invariant.
• Schoenflies.QuantitativeReverseStage.transition — the output is a StageTransition.
• Schoenflies.QuantitativeReverseStage.diam_targetStar_lt_bound — the uniform half of prop:shrinking-stars at this successor.
• Schoenflies.TargetFaceMesh.refine — subsequent forward transfers preserve the target face-mesh estimate.

def Schoenflies.TargetFaceMesh {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (bound : ℝ) : Prop

A uniform mesh bound on the closed target 2-cells of a generated pair.

Equations

• Schoenflies.TargetFaceMesh P bound = ∀ {F : γ}, F ∈ P.str.faces → Metric.diam (closure (P.tgt.cell F)) < bound

theorem Schoenflies.TargetFaceMesh.refine {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P T : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {par : γ → γ} {bound : ℝ} (hmesh : TargetFaceMesh P bound) (href : T.tgt.Refines P.tgt par) : TargetFaceMesh T bound

A target face-mesh bound survives any compatible refinement.

theorem Schoenflies.TargetFaceMesh.forwardTransfer {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P T : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {par : γ → γ} {bound : ℝ} (hmesh : TargetFaceMesh P bound) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (h : IsTransferOf T P H Hdraw par) : TargetFaceMesh T bound

In particular, direction (a) of finite transfer preserves the target mesh bound.

theorem Schoenflies.TargetFaceMesh.diam_star_lt {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {bound : ℝ} (hmesh : TargetFaceMesh P bound) {σ : γ} (hσ : σ ∈ P.str.cells) : Metric.diam (P.tgt.star σ) < 2 * bound

A target face-mesh estimate gives the corresponding factor-two bound on every star.

structure Schoenflies.QuantitativeReverseStage {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (anchors : List Plane) (bound : ℝ) : Type u_1

The complete output of one quantitatively bounded reverse-transfer successor.

• cover : TargetSegmentCover P

  A finite exact segment presentation of the old target skeleton.

• overlay : self.cover.MeshOverlayTransferData anchors

  The chosen overlay and transferred generated pair.

• delta_lt_half_bound : self.overlay.delta < bound / 2

  Half the requested bound leaves room for the factor two in the star estimate.

@[reducible, inline]

abbrev Schoenflies.QuantitativeReverseStage.pair {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {bound : ℝ} (w : QuantitativeReverseStage P anchors bound) : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

The generated pair at the new successor stage.

Equations

• w.pair = w.overlay.pair

@[reducible, inline]

abbrev Schoenflies.QuantitativeReverseStage.parent {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {bound : ℝ} (w : QuantitativeReverseStage P anchors bound) : γ → γ

The common abstract parent map from the successor to the old stage.

Equations

• w.parent = w.overlay.parent

theorem Schoenflies.QuantitativeReverseStage.transition {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {bound : ℝ} (w : QuantitativeReverseStage P anchors bound) : StageTransition w.pair P w.parent

Reverse finite transfer supplies exactly the common transition interface used by the tower.

theorem Schoenflies.QuantitativeReverseStage.diam_targetStar_lt_bound {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {bound : ℝ} (w : QuantitativeReverseStage P anchors bound) {σ : γ} (hσ : σ ∈ w.pair.str.cells) : Metric.diam (w.pair.tgt.star σ) < bound

Every target star at the successor has diameter below the prescribed bound.

theorem Schoenflies.QuantitativeReverseStage.targetFaceMesh {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {bound : ℝ} (w : QuantitativeReverseStage P anchors bound) : TargetFaceMesh w.pair w.overlay.delta

The stronger face-level estimate retained by later forward refinements.

theorem Schoenflies.exists_quantitativeReverseStage {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hsep : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) {bound : ℝ} (hbound : 0 < bound) : Nonempty (QuantitativeReverseStage P anchors bound)

Quantitative reverse successor. Every generated stage over the closed Jordan domain admits a reverse transferred refinement whose target stars are smaller than any specified positive bound.