The σ-grading count: the arithmetic that clause A actually needs

The permutation-grading estimate asks for ∑_{σ ∈ S_m} I(σ) ≤ K^m·L^{m-1} with L = |log ε| and the capped range 3 ≤ m ≤ ⌊L⌋. The proved interface R324CappedCrossGradingBoundAt factors this through a grade r : S_m → ℕ with

• a per-entity bound I(σ) ≤ C^m·L^{r σ}, and
• the graded count ∑_σ L^{r σ} ≤ C^m·L^{m-1}.

This file proves the graded count from a purely combinatorial layer hypothesis, and nothing else. It is the half of the σ-grading that is independent of any analysis.

Deriving the requirement (the arithmetic, verified below)

The identity entity really is of size ≍ C^m·L^{m-1}, so r id = m-1 is forced and the per-entity bound cannot be improved uniformly. The flat grade r ≡ m-1 gives ∑_σ L^{r σ} = m!·L^{m-1}, which is over budget exactly once m! > C^m (r324CappedCross_flatGrade_over_budget). On the capped range the order cap gives m ≤ L (r324Grade_cast_le_log below), hence

m! ≤ m^{m-1} ≤ L^{m-1} (r324Grade_factorial_le_pow),

so the flat grade is over budget by exactly one factor L^{m-1} and no more. Writing N_j = #{σ : r σ = j} the graded count reads ∑_{j≤m-1} N_j·L^j ≤ C^m·L^{m-1}, and since m ≤ L a sufficient condition, uniform in ε, is

N_j ≤ A^m·m^{m-1-j} (r324Grade_sum_pow_le),

equivalently — because (m-j)! ≤ m^{m-1-j} — the more quotable

N_j ≤ A^m·(m-j)! (r324Grade_sum_pow_le_of_factorial).

Each unit of grade must cost a factor m in the count. The two ends of this criterion are exactly the two facts one knows: at j = 0 it is the trivial N_0 ≤ m!, and at j = m-1 it is #{σ : r σ = m-1} ≤ A^m — only geometrically many entities may carry the full window power. So clause A's budget K^m·L^{m-1} is right as stated; no factorial allowance is needed, provided the analytic grade decays with the count at this factorial rate. (The m = 3 slice sits inside the criterion with room to spare: r ≡ 2 there needs 3! = 6 ≤ A³·(3-2)! = A³, true for A = 2; r324Grade_three_flat_count records it.)

The order cap

theorem Anderson4D.r324Grade_cast_le_log {ε : ℝ} {m : ℕ} (hm : m ≤ truncOrder ε) : ↑m ≤ |Real.log ε|

The order cap in analytic form. truncOrder ε = ⌊|log ε|⌋, so a capped order satisfies m ≤ L. This is the single inequality that makes the factorial count affordable.

n! ≤ n^{n-1}

theorem Anderson4D.r324Grade_factorial_le_pow (n : ℕ) : n.factorial ≤ n ^ (n - 1)

n! ≤ n^{n-1}: the factorial is below the top window power.

theorem Anderson4D.r324Grade_factorial_sub_le (m j : ℕ) (hj : j ≤ m - 1) : (m - j).factorial ≤ m ^ (m - 1 - j)

The layer form: (m-j)! ≤ m^{m-1-j} for j ≤ m-1. This is why the factorial criterion implies the power criterion.

The graded count

theorem Anderson4D.r324Grade_sum_pow_le {α : Type u_1} (E : Finset α) (grade : α → ℕ) {m : ℕ} {A L : ℝ} (hA : 0 ≤ A) (hm : 1 ≤ m) (hL : ↑m ≤ L) (hgrade : ∀ e ∈ E, grade e ≤ m - 1) (hcount : ∀ j ≤ m - 1, ↑{e ∈ E | grade e = j}.card ≤ A ^ m * ↑m ^ (m - 1 - j)) : ∑ e ∈ E, L ^ grade e ≤ (2 * A) ^ m * L ^ (m - 1)

The graded count from layer cardinalities. If every grade is at most m-1 and the j-th layer has at most A^m·m^{m-1-j} members, then the graded sum obeys clause A's budget with constant 2A, on the capped range m ≤ L.

This is the exact statement R324CappedCrossGradingBoundAt needs for its second clause; the proof is one line of power counting once the sum is fibred over the grade: ∑_j N_j·L^j ≤ ∑_j A^m·L^{m-1-j}·L^j = m·A^m·L^{m-1} ≤ (2A)^m·L^{m-1}.

theorem Anderson4D.r324Grade_sum_pow_le_of_factorial {α : Type u_1} (E : Finset α) (grade : α → ℕ) {m : ℕ} {A L : ℝ} (hA : 0 ≤ A) (hm : 1 ≤ m) (hL : ↑m ≤ L) (hgrade : ∀ e ∈ E, grade e ≤ m - 1) (hcount : ∀ j ≤ m - 1, ↑{e ∈ E | grade e = j}.card ≤ A ^ m * ↑(m - j).factorial) : ∑ e ∈ E, L ^ grade e ≤ (2 * A) ^ m * L ^ (m - 1)

The graded count from a factorial layer criterion. The quotable form: if the j-th grade layer has at most A^m·(m-j)! members then clause A's budget holds with constant 2A. At j = 0 this is the trivial N_0 ≤ A^m·m!; at j = m-1 it is the sharp requirement that only A^m entities carry the full window power.

theorem Anderson4D.r324Grade_three_flat_count : ↑(Nat.factorial 3) ≤ 2 ^ 3 * ↑(3 - 2).factorial

The m = 3 slice inside the criterion: the flat grade r ≡ 2 there needs 3! ≤ A³·(3-2)!, i.e. 6 ≤ A³, true for A = 2. So the proved order-three calibration is the j = m-1 end of the factorial criterion, with room to spare.