Final scalar ledger for the collapse induction

This file closes the numerical estimates (5.46)--(5.48). The strict branch-count saving supplies the inverse D, the new compound-leaf factor is absorbed locally, and the remaining factorial and exponential losses fit the original-tree induction coefficient.

Positivity of the unchanged induction tail

theorem Anderson4D.paperLeafProduct_nonneg {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) : 0 ≤ paperLeafProduct mu compound

theorem Anderson4D.singleScaleBranchPower_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : 0 ≤ singleScaleBranchPower Nm mu compound

theorem Anderson4D.originalParentRatioFactor_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (W : Finset t.VPos) : 0 ≤ originalParentRatioFactor Nm W

The strict D saving and local compound-leaf factor

theorem Anderson4D.collapseDLocal_power_le (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (a b k : ℕ) (hab : a + 1 ≤ b) : D ^ a * C0 ^ k * (↑k.factorial)⁻¹ * factorialThreeQuarters k ≤ D ^ b

A one-unit branch-exponent saving pays for the entire new compound-leaf factor.

Factorial and skipped-branch cardinality ledger

theorem Anderson4D.collapse_factorial_card_bound {t : PlaneTree} (r : t.VPos) (n m s : ℕ) (hn : 4 ≤ n) (hs : 1 ≤ s) (hsn : s + 1 ≤ n) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) (hw : 2 * W.card ≤ m) : sqrtFactorial (n - s) * sqrtFactorial (m + s + 1 - 2 * W.card) ≤ sqrtFactorial (n + m - 2 * (liftWPrime r s W).card) * 2 ^ n

Paper (5.47), with the cardinality of W' substituted and its polynomial loss enlarged to 2^n.

Complete scalar coefficient

theorem Anderson4D.collapse_scalar_coefficient_le (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (n m s : ℕ) (hn : 4 ≤ n) (hs : 1 ≤ s) (hsn : s + 1 ≤ n) {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) (hw : 2 * W.card ≤ m) : 2 ^ n * (4 ^ n * C0 ^ (↑n / 2) * C0 ^ (m + s + 1) * D ^ (t.contractAt ↑r).BranchNodes.card * (↑(s + 1).factorial)⁻¹ * factorialThreeQuarters (s + 1) * sqrtFactorial (n - s) * sqrtFactorial (m + s + 1 - 2 * W.card)) ≤ C0 ^ (n + m) * D ^ t.BranchNodes.card * sqrtFactorial (n + m - 2 * (liftWPrime r s W).card)

The complete scalar inequality in (5.46)--(5.48), before multiplying by the unchanged leaf/branch/ratio tail. The leading 2^n is the outer composition-count loss.

Final (5.46)--(5.48) interface

theorem Anderson4D.two_pow_mul_combinedCollapseFactored_le_inductiveRHSSummand (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (n mOutside s : ℕ) (hn : 4 ≤ n) (hs : 1 ≤ s) (hsn : s + 1 ≤ n) {t : PlaneTree} : t.isValid = true → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hr : r ∈ nonrootBranches t) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) (hWcard : 2 * W.card ≤ mOutside), 2 ^ n * combinedCollapseFactored C0 D n s (mOutside + s + 1) Nm mu compound r W ≤ C0 ^ (n + mOutside) * D ^ t.BranchNodes.card * inductiveRHSSummand (n + mOutside) t Nm mu compound (liftWPrime r s W)

Paper (5.46)--(5.48): after the outer composition count, one factored collapse term is bounded by the corresponding original-tree induction summand.