Strong-induction shell for Proposition 5.9

This module separates the well-founded recursion from the analytic collapse estimate. The no-eligible branch is already closed by Proposition 5.10; the its local input is a step at a chosen lowest eligible branch.

def Anderson4D.InductiveConclusion (C0 D : ℝ) (t : PlaneTree) : Prop

The quantified conclusion of Proposition 5.9 for one fixed tree.

Equations

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

def Anderson4D.EligibleCollapseStep (C0 D : ℝ) : Prop

The sole recursive input left after the no-eligible case: assuming the Proposition 5.9 conclusion for every smaller tree, prove it by collapsing a chosen lowest eligible branch.

Equations

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

theorem Anderson4D.inductiveEstimate_of_singleScale_of_eligibleStep {C0 D : ℝ} (hsingle : SingleScaleEstimate C0) (hD : D = Real.exp (C0 ^ 10)) (hstep : EligibleCollapseStep C0 D) : InductiveEstimate C0 D

Strong induction closes the full statement once the eligible collapse step is supplied.