The inductive permutation-sum estimate

This module closes Proposition 5.9. At a lowest eligible branch, the raw word sum is partitioned by active collapse shape. The valid-word Fubini bound and the two analytic calls control each shape, while the composition count is absorbed by the 2^n factor in the fixed-shape scalar ledger. Strong induction on tree size then closes the theorem.

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

The local eligible-branch step used by the strong-induction shell.

theorem Anderson4D.inductive_estimate : ∃ (C0 : ℝ) (D : ℝ), InductiveEstimate C0 D

Proposition 5.9 / (5.32)--(5.33).