Composition-count losses in the collapse induction

The skipped-edge set is equivalently a positive composition of the inside word. This module records the two elementary exponential losses used after the fixed-shape Fubini estimate.

theorem Anderson4D.card_composition_le_two_pow (n : ℕ) : Fintype.card (Composition n) ≤ 2 ^ n

There are at most 2^n positive compositions of n.

theorem Anderson4D.sum_composition_le_two_pow_mul {n : ℕ} (F : Composition n → ℝ) (K : ℝ) (hFK : ∀ (c : Composition n), F c ≤ K) (hK : 0 ≤ K) : ∑ c : Composition n, F c ≤ 2 ^ n * K

A nonnegative summand uniformly bounded by K over compositions costs at most the paper's coarse factor 2^n.

theorem Anderson4D.nat_sq_le_two_pow {n : ℕ} (hn : 4 ≤ n) : n ^ 2 ≤ 2 ^ n

The polynomial loss in (5.47) is dominated by 2^n for n ≥ 4.

theorem Anderson4D.natCast_sq_le_two_pow {n : ℕ} (hn : 4 ≤ n) : ↑n ^ 2 ≤ 2 ^ n

Real-cast form used in the scalar factor audit.