The common output of one transferred stage

Both directions of finite transfer produce the four pieces of data needed between consecutive matched cellulations: compatible source and target refinements, growth of the realized source skeleton, and agreement of the new skeleton homeomorphism with the old one. StageTransition packages that shared output and proves that transitions compose.

Blueprint

• Schoenflies.StageTransition — one step of the quantitative-refinement recursion, stripped of the particular ambient graph used to construct it.
• Schoenflies.IsPartialTransferOf.stageTransition, Schoenflies.IsTargetPartialTransferOf.stageTransition — both finite-transfer directions expose the same stage interface.
• Schoenflies.StageTransition.trans — consecutive transferred refinements compose.

structure Schoenflies.StageTransition {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ) : Prop

The information about consecutive generated pairs consumed by StageSequence.

• refines_src : T.src.Refines P.src par

  The new source realization refines the preceding source realization.

• refines_tgt : T.tgt.Refines P.tgt par

  The target realizations refine along the same abstract parent map.

• sourceSkeletonSet_subset : P.src.skeletonSet ⊆ T.src.skeletonSet

  The realized source skeleton grows.

• homeo_eqOn : Set.EqOn T.homeo.toFun P.homeo.toFun P.src.skeletonSet

  The new skeleton homeomorphism extends the preceding one.

theorem Schoenflies.StageTransition.targetSkeletonSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {par : γ → γ} (h : StageTransition T P par) : P.tgt.skeletonSet ⊆ T.tgt.skeletonSet

Target skeletons grow as well. This follows from source-skeleton growth and agreement of the two skeleton homeomorphisms on the old source skeleton.

theorem Schoenflies.StageTransition.trans {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P Q T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {par₁ par₂ : γ → γ} (h₂ : StageTransition T Q par₂) (h₁ : StageTransition Q P par₁) : StageTransition T P (par₁ ∘ par₂)

Consecutive stage transitions compose their parent maps and their nesting data.

theorem Schoenflies.IsPartialTransferOf.stageTransition {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (h : IsPartialTransferOf T P B Hdraw par) : StageTransition T P par

Direction (a)'s induction invariant supplies one stage transition.

theorem Schoenflies.IsTargetPartialTransferOf.stageTransition {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (h : IsTargetPartialTransferOf T P B Hdraw par) : StageTransition T P par

Direction (b)'s induction invariant supplies the identical stage transition.

theorem Schoenflies.IsTransferOf.stageTransition {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (h : IsTransferOf T P H Hdraw par) : StageTransition T P par

The admissible conclusion of direction (a) forgets to the same stage transition.

theorem Schoenflies.IsTargetTransferOf.stageTransition {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (h : IsTargetTransferOf T P H Hdraw par) : StageTransition T P par

The admissible conclusion of direction (b) forgets to the same stage transition.