Factorial bookkeeping for the collapse induction

This file isolates equation (5.47) in the proof of Proposition 5.9. The paper distinguishes the case of one skipped edge, where the collapsed branch is inserted into W', from the case of at least two skipped edges.

theorem Anderson4D.factorial_mul_factorial_le_pow_mul_factorial_add_sub (a b k : ℕ) (hk : k ≤ a) : a.factorial * b.factorial ≤ a ^ k * (a + b - k).factorial

Removing k factors from the first factorial costs at most a^k.

The sharper intermediate factor is a.descFactorial k; the remaining two factorials form a binomial coefficient.

theorem Anderson4D.collapse_factorial_sq_bound (n m s w : ℕ) (hs : 1 ≤ s) (hsn : s + 1 ≤ n) (hn : 4 ≤ n) (hw : 2 * w ≤ m) : (n - s).factorial * (m + s + 1 - 2 * w).factorial ≤ n ^ 4 * (n + m - 2 * if s = 1 then w + 1 else w).factorial

Natural-number square of paper (5.47).

Here w' = w + 1 when s = 1, and w' = w when s > 1. Squaring the printed inequality turns its factor n² into n⁴.

theorem Anderson4D.collapse_factorial_sqrt_bound (n m s w : ℕ) (hs : 1 ≤ s) (hsn : s + 1 ≤ n) (hn : 4 ≤ n) (hw : 2 * w ≤ m) : √↑(n - s).factorial * √↑(m + s + 1 - 2 * w).factorial ≤ √↑(n + m - 2 * if s = 1 then w + 1 else w).factorial * ↑n ^ 2

Paper (5.47), with the two definitions of W' encoded by the conditional in the target factorial.