Quantitative forward local-grid stages

The local-grid attachment supplies a complete raw grid in the source skeleton. This module turns that containment into the pointwise source-star estimate used by prop:shrinking-stars, and records that the target face mesh from the preceding reverse stage survives the forward refinement.

theorem Schoenflies.localGrid_frame_subset {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : p.closedSquare s \ p.openSquare s ⊆ cover (localGridEdges p s k)

The frame of a positive local-grid square is contained in its raw grid carrier.

theorem Schoenflies.LocalGridForwardStageData.face_subset_openSquare {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {s epsilon : ℝ} (w : LocalGridForwardStageData P p s epsilon) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C) {x : Plane} (hx : x ∈ p.openSquare s) {F : γ} (hF : F ∈ w.pair.str.faces) (hsub : w.pair.str.sub (w.pair.src.carrier x) F) : w.pair.src.cell F ⊆ p.openSquare s

Every new source face incident with a point in the open grid window stays inside that window. Its connected open cell cannot cross the grid's outer frame, which is now part of the source skeleton.

theorem Schoenflies.LocalGridForwardStageData.diam_closure_face_le {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {s epsilon : ℝ} (w : LocalGridForwardStageData P p s epsilon) (hs : 0 < s) (hepsilon : 0 < epsilon) (hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C) {x : Plane} (hx : x ∈ p.openSquare s) {F : γ} (hF : F ∈ w.pair.str.faces) (hsub : w.pair.str.sub (w.pair.src.carrier x) F) : Metric.diam (closure (w.pair.src.cell F)) ≤ epsilon

Every source face incident with a point in the open window has closed diameter at most the chosen local-grid mesh bound.

theorem Schoenflies.LocalGridForwardStageData.diam_sourceStar_le {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {s epsilon : ℝ} (w : LocalGridForwardStageData P p s epsilon) (hC : IsSeparating C) (hs : 0 < s) (hepsilon : 0 < epsilon) (hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C) {x : Plane} (hx : x ∈ p.openSquare s) : Metric.diam (w.pair.src.star (w.pair.src.carrier x)) ≤ 2 * epsilon

lem:grid-star-estimate. At a point in the open grid window, the new source star has diameter at most twice the selected mesh bound.

theorem Schoenflies.LocalGridForwardStageData.targetFaceMesh {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {s epsilon : ℝ} (w : LocalGridForwardStageData P p s epsilon) {bound : ℝ} (hmesh : TargetFaceMesh P bound) : TargetFaceMesh w.pair bound

A target face-mesh estimate survives the forward local-grid stage.

theorem Schoenflies.GeneratedPair.exists_localGridForwardStageData_window {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) {p : Plane} (hp : p ∈ inside C) {windowEpsilon meshEpsilon : ℝ} (hwindowEpsilon : 0 < windowEpsilon) (_hmeshEpsilon : 0 < meshEpsilon) (hsource : IsConnected P.src.nonboundary) : Nonempty (LocalGridForwardStageData P p (windowRadius C windowEpsilon p) meshEpsilon)

The window used by quantitative refinement automatically satisfies every geometric hypothesis of the local-grid forward constructor.

structure Schoenflies.QuantitativeForwardStage {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (p : Plane) (windowEpsilon meshEpsilon targetBound : ℝ) : Type u_1

One quantitative forward successor: the local-grid refinement together with the target face-mesh estimate inherited from the preceding reverse stage.

• forward : LocalGridForwardStageData P p (windowRadius C windowEpsilon p) meshEpsilon

  Local source-grid refinement at the prescribed scale.

• targetFaceMesh : TargetFaceMesh self.forward.pair targetBound

@[reducible, inline]

abbrev Schoenflies.QuantitativeForwardStage.pair {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {windowEpsilon meshEpsilon targetBound : ℝ} (w : QuantitativeForwardStage P p windowEpsilon meshEpsilon targetBound) : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

The generated pair at the forward successor.

Equations

• w.pair = w.forward.pair

@[reducible, inline]

abbrev Schoenflies.QuantitativeForwardStage.parent {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {windowEpsilon meshEpsilon targetBound : ℝ} (w : QuantitativeForwardStage P p windowEpsilon meshEpsilon targetBound) : γ → γ

The shared parent map to the preceding stage.

Equations

• w.parent = w.forward.parent

theorem Schoenflies.QuantitativeForwardStage.transition {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {windowEpsilon meshEpsilon targetBound : ℝ} (w : QuantitativeForwardStage P p windowEpsilon meshEpsilon targetBound) : StageTransition w.pair P w.parent

The forward successor exposes the common transition interface.

theorem Schoenflies.QuantitativeForwardStage.diam_sourceStar_le {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {p : Plane} {windowEpsilon meshEpsilon targetBound : ℝ} (w : QuantitativeForwardStage P p windowEpsilon meshEpsilon targetBound) (hC : IsSeparating C) (hp : p ∈ inside C) (hwindowEpsilon : 0 < windowEpsilon) (hmeshEpsilon : 0 < meshEpsilon) {x : Plane} (hx : x ∈ openWindow C windowEpsilon p) : Metric.diam (w.pair.src.star (w.pair.src.carrier x)) ≤ 2 * meshEpsilon

The local-grid estimate in the window form used by prop:shrinking-stars.

theorem Schoenflies.GeneratedPair.exists_quantitativeForwardStage {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) {p : Plane} (hp : p ∈ inside C) {windowEpsilon meshEpsilon targetBound : ℝ} (hwindowEpsilon : 0 < windowEpsilon) (hmeshEpsilon : 0 < meshEpsilon) (hsource : IsConnected P.src.nonboundary) (hmesh : TargetFaceMesh P targetBound) : Nonempty (QuantitativeForwardStage P p windowEpsilon meshEpsilon targetBound)

Construct a quantitative forward successor from any target face-mesh estimate on the preceding stage.

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

One complete quantitative successor consists of the uniform reverse target refinement and the pointwise forward source-grid refinement.

• reverse : QuantitativeReverseStage P anchors targetBound

  Uniform target refinement performed first.

• forward : QuantitativeForwardStage self.reverse.pair p windowEpsilon sourceBound self.reverse.overlay.delta

  Source-grid refinement of the reverse stage output.

@[reducible, inline]

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

The generated pair at the end of the two half-steps.

Equations

• w.pair = w.forward.pair

@[reducible, inline]

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

The composite shared parent map to the preceding full stage.

Equations

• w.parent = w.reverse.parent ∘ w.forward.parent

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

The reverse and forward transitions compose to one full-stage transition.

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

The uniform target-star estimate survives the following forward refinement.

theorem Schoenflies.QuantitativeSuccessor.diam_sourceStar_le {γ : Type u_1} [Nonempty γ] {S₀ : CellStructure γ} {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} {anchors : List Plane} {p : Plane} {windowEpsilon sourceBound targetBound : ℝ} (w : QuantitativeSuccessor P anchors p windowEpsilon sourceBound targetBound) (hC : IsSeparating C) (hp : p ∈ inside C) (hwindowEpsilon : 0 < windowEpsilon) (hsourceBound : 0 < sourceBound) {x : Plane} (hx : x ∈ openWindow C windowEpsilon p) : Metric.diam (w.pair.src.star (w.pair.src.carrier x)) ≤ 2 * sourceBound

The pointwise source-star estimate at every point caught by this stage's window.

theorem Schoenflies.GeneratedPair.exists_quantitativeSuccessor {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) {p : Plane} (hp : p ∈ inside C) {windowEpsilon sourceBound targetBound : ℝ} (hwindowEpsilon : 0 < windowEpsilon) (hsourceBound : 0 < sourceBound) (htargetBound : 0 < targetBound) : Nonempty (QuantitativeSuccessor P anchors p windowEpsilon sourceBound targetBound)

Quantitative successor. Starting from any generated stage, construct a refinement with the requested target-star bound and a source-star bound throughout the selected window.