Constant absorption for the collapse induction

This file isolates the constant estimate following paper (5.46). Taking fourth powers turns the residual compound-leaf factor into one factorial denominator, which is then controlled by the exponential series.

theorem Anderson4D.factorialThreeQuarters_pow_four (n : ℕ) : factorialThreeQuarters n ^ 4 = ↑n.factorial ^ 3

The fourth power of (n!)^(3/4) is (n!)^3.

noncomputable def Anderson4D.collapseDLocalFactor (C0 D : ℝ) (n : ℕ) : ℝ

The factor in (5.46) involving the new compound leaf.

Equations

• Anderson4D.collapseDLocalFactor C0 D n = D⁻¹ * C0 ^ n * (↑n.factorial)⁻¹ * Anderson4D.factorialThreeQuarters n

theorem Anderson4D.collapseDLocalFactor_le_one (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (n : ℕ) : collapseDLocalFactor C0 D n ≤ 1

The large constant D = exp(C0^10) absorbs the new compound-leaf factor uniformly in its multiplicity.

Final exponential absorption

After (5.47), the two independent 4^n ledgers combine with the single-scale half-power to give

16^n * C0^(n/2).

The paper assumes C0 > 1000, which is already more than enough to absorb this expression into C0^n. Keeping this scalar step separate prevents the collapse proof from silently spending the same geometric loss twice.

theorem Anderson4D.sixteen_mul_sqrt_le_self (C0 : ℝ) (hC0 : 1000 < C0) : 16 * √C0 ≤ C0

For the paper's range C0 > 1000, one copy of 16 * sqrt C0 is absorbed by C0.

theorem Anderson4D.sixteen_pow_mul_halfPower_le_natPower (C0 : ℝ) (hC0 : 1000 < C0) (n : ℕ) : 16 ^ n * C0 ^ (↑n / 2) ≤ C0 ^ n

The complete post-collapse exponential ledger: 16^n * C0^(n/2) ≤ C0^n.

theorem Anderson4D.pow_le_pow_mul_inv_of_succ_le (D : ℝ) (hD : 1 ≤ D) (a b : ℕ) (hab : a + 1 ≤ b) : D ^ a ≤ D ^ b * D⁻¹

A strict saving in a natural exponent extracts one inverse factor. This is the scalar form of the branch-cardinality saving in (5.45).