Ready-to-use analytic calls in the Proposition 5.9 collapse

This file discharges the structural and geometric side conditions needed for the two analytic estimates used after a collapse: Proposition 5.10 on the selected rooted subtree, and the induction hypothesis on the contracted tree.

Proposition 5.10 on the restricted subtree

theorem Anderson4D.singleScaleEstimate_restrict {C0 : ℝ} (hsingle : SingleScaleEstimate C0) {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (hcompound : compound ⊆ t.Leaves) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) {r : t.VPos} (hr : IsLowestCollapseEligible Nm mu r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) : paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) d.adjacentCutIndices) ≤ singleScaleRHS C0 d.insideLength d.adjacentCutIndices.card (scaleN Nm (PlaneTree.parentV r)) (t.subtreeAt ↑r) (restrictMarking Nm r) (restrictMultiplicities mu r) (restrictCompound r compound)

A lowest eligible branch supplies every hypothesis of Proposition 5.10 on the restricted tree. The scale parameter is exactly the original parent scale and the skipped set is the canonical composition-cut set.

Contracted induction data

theorem Anderson4D.contracted_induction_hypotheses {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (hcompound : compound ⊆ t.Leaves) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) : let s := collapseCutCount d; have hs := ⋯; (t.contractAt ↑r).isValid = true ∧ (t.contractAt ↑r).rootV ∈ (t.contractAt ↑r).BranchNodes ∧ contractCompound r compound ⊆ (t.contractAt ↑r).Leaves ∧ totalMultiplicity (contractMultiplicities mu r s hs) = d.collapsed.length ∧ IsSeparatedEmbedding (contractMarking Nm r) (contractEmbedding z r lstar) ∧ SatisfiesSubtreeDiameter (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractEmbedding z r lstar) ∧ (t.contractAt ↑r).size < t.size

All non-recursive hypotheses needed to apply Proposition 5.9 to the contracted tree, including strict decrease of the induction measure.