The coincidence gluing count

This file proves R324GradeCoincidenceCount, the second combinatorial input of the σ-grading: for every prescribed set S of coincidences,

#{τ : S ⊆ r324GradeCoincidence τ} ≤ 2^m·(m - |S|)!.

The mechanism

A coincidence i ∈ S says that the labels i and i+1 occupy adjacent slots of the τ-order. Prescribing |S| coincidences glues the labels into m - |S| blocks of consecutive labels, each of which must occupy a block of consecutive slots; the arrangement is determined by the order of the blocks ((m-|S|)! choices) and the orientation of each block (≤ 2^m choices).

The proof implements the gluing one coincidence at a time: the contraction r324LayerContract merges the two glued labels into one and the two occupied slots into one, producing a permutation of Fin (m-1) that realises the shifted coincidence set, and the original permutation is recovered from the contracted one together with a single orientation bit. This gives N(m,S) ≤ 2·N(m-1,S') with |S'| = |S|-1, hence N(m,S) ≤ 2^{|S|}·(m-|S|)! by induction on m — no loss at all, the 2^m of the interface is slack.

Positions

def Anderson4D.r324LayerPos {m : ℕ} (π : Equiv.Perm (Fin m)) (i : ℕ) : ℕ

The slot occupied by label i under the arrangement π (junk outside the range). r324GradePos τ = r324LayerPos τ.symm.

Equations

• Anderson4D.r324LayerPos π i = if h : i < m then ↑(π ⟨i, h⟩) else 0

theorem Anderson4D.r324LayerPos_eq_gradePos {m : ℕ} (τ : Equiv.Perm (Fin m)) (i : ℕ) : r324LayerPos (Equiv.symm τ) i = r324GradePos τ i

theorem Anderson4D.r324LayerPos_lt {m : ℕ} (π : Equiv.Perm (Fin m)) {i : ℕ} (h : i < m) : r324LayerPos π i < m

theorem Anderson4D.r324LayerPos_inj {m : ℕ} (π : Equiv.Perm (Fin m)) {i j : ℕ} (hi : i < m) (hj : j < m) (h : r324LayerPos π i = r324LayerPos π j) : i = j

theorem Anderson4D.r324LayerPos_ext {m : ℕ} {π σ : Equiv.Perm (Fin m)} (h : ∀ i < m, r324LayerPos π i = r324LayerPos σ i) : π = σ

Two arrangements with the same slot function agree.

The glued sets

def Anderson4D.r324LayerGlued (m : ℕ) (S : Finset ℕ) : Finset (Equiv.Perm (Fin m))

The arrangements realising all the prescribed coincidences in S: for each i ∈ S the labels i and i+1 occupy adjacent slots.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.r324LayerGlued_mem {m : ℕ} {S : Finset ℕ} {π : Equiv.Perm (Fin m)} : π ∈ r324LayerGlued m S ↔ ∀ i ∈ S, i + 1 < m ∧ (r324LayerPos π (i + 1) + 1 = r324LayerPos π i ∨ r324LayerPos π i + 1 = r324LayerPos π (i + 1))

theorem Anderson4D.r324LayerGlued_empty (m : ℕ) : (r324LayerGlued m ∅).card = m.factorial

Label and slot merging

def Anderson4D.r324LayerHat (i₀ j : ℕ) : ℕ

Label map: Fin (m-1) → ℕ skipping the merged label i₀+1.

Equations

• Anderson4D.r324LayerHat i₀ j = if j ≤ i₀ then j else j + 1

def Anderson4D.r324LayerKap (p v : ℕ) : ℕ

Slot map: merge the slots p and p+1.

Equations

• Anderson4D.r324LayerKap p v = if v ≤ p then v else v - 1

def Anderson4D.r324LayerBase {m : ℕ} (π : Equiv.Perm (Fin m)) (i₀ : ℕ) : ℕ

The lower of the two slots occupied by the glued labels.

Equations

• Anderson4D.r324LayerBase π i₀ = min (Anderson4D.r324LayerPos π i₀) (Anderson4D.r324LayerPos π (i₀ + 1))

theorem Anderson4D.r324LayerHat_ne {i₀ j : ℕ} : r324LayerHat i₀ j ≠ i₀ + 1

theorem Anderson4D.r324LayerHat_inj {i₀ j₁ j₂ : ℕ} (h : r324LayerHat i₀ j₁ = r324LayerHat i₀ j₂) : j₁ = j₂

theorem Anderson4D.r324LayerHat_lt {m i₀ j : ℕ} (hi₀ : i₀ + 1 < m) (hj : j < m - 1) : r324LayerHat i₀ j < m

theorem Anderson4D.r324LayerHat_le {i₀ j : ℕ} (h : j ≤ i₀) : r324LayerHat i₀ j = j

theorem Anderson4D.r324LayerHat_gt {i₀ j : ℕ} (h : i₀ < j) : r324LayerHat i₀ j = j + 1

theorem Anderson4D.r324LayerBase_spec {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) : r324LayerPos π i₀ = r324LayerBase π i₀ ∧ r324LayerPos π (i₀ + 1) = r324LayerBase π i₀ + 1 ∨ r324LayerPos π i₀ = r324LayerBase π i₀ + 1 ∧ r324LayerPos π (i₀ + 1) = r324LayerBase π i₀

The two glued labels occupy the slots base and base+1.

theorem Anderson4D.r324LayerBase_lt {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hi₀ : i₀ + 1 < m) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) : r324LayerBase π i₀ + 1 < m

theorem Anderson4D.r324LayerPos_ne_base {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ j : ℕ} (hi₀ : i₀ + 1 < m) (hj : j < m) (hj1 : j ≠ i₀) (hj2 : j ≠ i₀ + 1) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) : r324LayerPos π j ≠ r324LayerBase π i₀ ∧ r324LayerPos π j ≠ r324LayerBase π i₀ + 1

Only the two glued labels sit in the merged slots.

theorem Anderson4D.r324LayerKap_le {m p v : ℕ} (hp : p + 1 < m) (hv : v < m) : r324LayerKap p v ≤ m - 2

theorem Anderson4D.r324LayerKap_eq_of_mem {p v : ℕ} (h : v = p ∨ v = p + 1) : r324LayerKap p v = p

theorem Anderson4D.r324LayerKap_adj {p a b : ℕ} (hmem : ¬((a = p ∨ a = p + 1) ∧ (b = p ∨ b = p + 1))) (hab : a + 1 = b ∨ b + 1 = a) : r324LayerKap p a + 1 = r324LayerKap p b ∨ r324LayerKap p b + 1 = r324LayerKap p a

Slot merging preserves adjacency of two slots not both merged.

theorem Anderson4D.r324LayerKap_inj {p a b : ℕ} (_ha : a ≠ p ∧ a ≠ p + 1) (_hb : b ≠ p ∧ b ≠ p + 1) (h : r324LayerKap p a = r324LayerKap p b) : a = b

Slot merging is injective away from the merged slots.

The contracted arrangement

def Anderson4D.r324LayerContractFun {m : ℕ} (π : Equiv.Perm (Fin m)) (i₀ : ℕ) (j : Fin (m - 1)) : Fin (m - 1)

The contracted arrangement as a function: drop the label i₀+1 and merge its slot with the slot of i₀.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.r324LayerContractFun_val {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hi₀ : i₀ + 1 < m) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) (j : Fin (m - 1)) : ↑(r324LayerContractFun π i₀ j) = r324LayerKap (r324LayerBase π i₀) (r324LayerPos π (r324LayerHat i₀ ↑j))

theorem Anderson4D.r324LayerContract_dichotomy {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hi₀ : i₀ + 1 < m) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) {j : ℕ} (hj : j < m - 1) : r324LayerHat i₀ j = i₀ ∨ r324LayerPos π (r324LayerHat i₀ j) ≠ r324LayerBase π i₀ ∧ r324LayerPos π (r324LayerHat i₀ j) ≠ r324LayerBase π i₀ + 1

Every label other than the two glued ones avoids the merged slots.

theorem Anderson4D.r324LayerContractFun_injective {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hi₀ : i₀ + 1 < m) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) : Function.Injective (r324LayerContractFun π i₀)

noncomputable def Anderson4D.r324LayerContract {m : ℕ} (π : Equiv.Perm (Fin m)) (i₀ : ℕ) : Equiv.Perm (Fin (m - 1))

The contracted arrangement.

Equations

• Anderson4D.r324LayerContract π i₀ = if h : Function.Injective (Anderson4D.r324LayerContractFun π i₀) then Equiv.ofBijective (Anderson4D.r324LayerContractFun π i₀) ⋯ else 1

theorem Anderson4D.r324LayerContract_pos {m : ℕ} {π : Equiv.Perm (Fin m)} {i₀ : ℕ} (hi₀ : i₀ + 1 < m) (hadj : r324LayerPos π (i₀ + 1) + 1 = r324LayerPos π i₀ ∨ r324LayerPos π i₀ + 1 = r324LayerPos π (i₀ + 1)) {j : ℕ} (hj : j < m - 1) : r324LayerPos (r324LayerContract π i₀) j = r324LayerKap (r324LayerBase π i₀) (r324LayerPos π (r324LayerHat i₀ j))

The slot function of the contracted arrangement.

Coincidences survive the contraction

def Anderson4D.r324LayerShift (i₀ i : ℕ) : ℕ

Relabelling after the merge.

Equations

• Anderson4D.r324LayerShift i₀ i = if i < i₀ then i else i - 1

theorem Anderson4D.r324LayerShift_injOn {i₀ i j : ℕ} (hi : i ≠ i₀) (hj : j ≠ i₀) (h : r324LayerShift i₀ i = r324LayerShift i₀ j) : i = j

theorem Anderson4D.r324LayerContract_mem {m : ℕ} {π : Equiv.Perm (Fin m)} {S : Finset ℕ} (hπ : π ∈ r324LayerGlued m S) {i₀ : ℕ} (hi₀S : i₀ ∈ S) : r324LayerContract π i₀ ∈ r324LayerGlued (m - 1) (Finset.image (r324LayerShift i₀) (S.erase i₀))

The contraction realises the shifted coincidences.

The contraction is two-to-one

theorem Anderson4D.r324LayerHat_shift {i₀ j : ℕ} (h1 : j ≠ i₀) (h2 : j ≠ i₀ + 1) : r324LayerHat i₀ (r324LayerShift i₀ j) = j

theorem Anderson4D.r324LayerShift_lt {m i₀ j : ℕ} (hi₀ : i₀ + 1 < m) (hj : j < m) : r324LayerShift i₀ j < m - 1

theorem Anderson4D.r324LayerGlue_ext {m : ℕ} {S : Finset ℕ} {i₀ : ℕ} (hi₀S : i₀ ∈ S) {π σ : Equiv.Perm (Fin m)} (hπ : π ∈ r324LayerGlued m S) (hσ : σ ∈ r324LayerGlued m S) (hbit : r324LayerPos π (i₀ + 1) < r324LayerPos π i₀ ↔ r324LayerPos σ (i₀ + 1) < r324LayerPos σ i₀) (hcon : r324LayerContract π i₀ = r324LayerContract σ i₀) : π = σ

The arrangement is recovered from its contraction and one orientation bit.

The gluing count

theorem Anderson4D.r324LayerGlued_card_le (m : ℕ) (S : Finset ℕ) : (r324LayerGlued m S).card ≤ 2 ^ S.card * (m - S.card).factorial

The gluing count. At most 2^{|S|}·(m-|S|)! arrangements realise all the prescribed coincidences in S.

The proved coincidence interface

theorem Anderson4D.r324Layer_mem_glued_of_subset {m : ℕ} {τ : Equiv.Perm (Fin m)} {S : Finset (Fin m)} (h : S ⊆ r324GradeCoincidence τ) : Equiv.symm τ ∈ r324LayerGlued m (Finset.image Fin.val S)

theorem Anderson4D.r324Layer_gradeCoincidenceCount (m : ℕ) : R324GradeCoincidenceCount m

The coincidence gluing count. This is the remaining combinatorial obligation of R324GradeCoincidence: a prescribed set S of coincidences is realised by at most 2^m·(m-|S|)! bijections.

theorem Anderson4D.r324Layer_permLayerCount_of_dominated {m : ℕ} {gradeP : Equiv.Perm (Fin m) → ℕ} (hm : 1 ≤ m) (hgle : ∀ (τ : Equiv.Perm (Fin m)), gradeP τ ≤ m - 1) (hdom : ∀ (τ : Equiv.Perm (Fin m)), gradeP τ ≤ (r324GradeCoincidence τ).card + 1) : R324GradePermLayerCount 8 m gradeP

The σ-grading layer count, with only the grade domination left. Combining the gluing count with r324Grade_permLayerCount_of_coincidence: any grade dominated by the coincidence count obeys the permutation layer count at constant 8, hence — through r324Grade_layeredAt_of_collapse — clause A.

The grade statistic the lattice rewards

The collapsed lattice sum of R324CollapseEntity is ∑_q ∏ᵢ‖ρ̂(εqᵢ)‖²·∏ⱼ⟨Sⱼ⟩⁻²⟨Sⱼ^τ⟩⁻² over the zero-sum sector, where Sⱼ = q₁+…+qⱼ and Sⱼ^τ = q_{τ(1)}+…+q_{τ(j)}. Both propagator families are prefix sums. A free ε⁻¹-window summation is produced exactly when a proper prefix of the identity order and a prefix of the τ order agree as sets: then Sⱼ^τ = Sⱼ, the two brackets collide into ⟨Sⱼ⟩⁻⁴, and the single Z4 variable Sⱼ may be summed freely against a log-critical kernel (r324SW_translated_window_le_log, r324SW_shifted_window_le_log, both ≤ C·|log ε|). A key that is not freed this way is pinned by the zero-sum constraint and is not a summation variable at all: that is the only reason it costs O(1). Summing a pinned key freely is never affordable — the bare symbol mass costs ε⁻⁴ (r324SW_symbol_mass_le) and a marked key costs ε⁻⁸ (r324RoutedWindow_marked_window_le), which is exactly the endpoint sacrifice the routed budget C^m·L^{m-1}·ε⁻⁸ pays once.

So the statistic is the number of prefix coincidences #{j : 1 ≤ j < m, τ({0,…,j-1}) = {0,…,j-1}} — the classical count of decomposition points of τ — plus one for the trivial (whole-set) member of the chain, capped at m-1. The two proved data points are matched exactly: the identity has all m-1 decomposition points, hence grade m-1 (r324LayerSplitGrade_one), and the simple permutation (2,4,1,3) of R324CappedCrossGrading has none, hence grade 1 (r324LayerSplitGrade_simple_four).

Note that this is not dominated by the adjacency coincidences of r324GradeCoincidence: the direct sum of two copies of (2,4,1,3) at m = 8 has one decomposition point and no adjacency coincidence at all (r324Layer_split_not_dominated_by_coincidence), so the split grade needs — and here gets — its own layer count.

def Anderson4D.r324LayerSplit {m : ℕ} (τ : Equiv.Perm (Fin m)) : Finset (Fin m)

The decomposition points of τ: the proper prefixes of the identity order that τ preserves setwise.

Equations

• Anderson4D.r324LayerSplit τ = {j : Fin m | 1 ≤ ↑j ∧ ∀ i < ↑j, Anderson4D.r324LayerPos τ i < ↑j}

def Anderson4D.r324LayerSplitGrade {m : ℕ} (τ : Equiv.Perm (Fin m)) : ℕ

The σ-grade of a bijection: one free window per decomposition point, plus the trivial member of the chain, capped by the identity's full power m-1.

Equations

• Anderson4D.r324LayerSplitGrade τ = min ((Anderson4D.r324LayerSplit τ).card + 1) (m - 1)

theorem Anderson4D.r324LayerSplitGrade_le {m : ℕ} (τ : Equiv.Perm (Fin m)) : r324LayerSplitGrade τ ≤ m - 1

theorem Anderson4D.r324LayerSplitGrade_le_card {m : ℕ} (τ : Equiv.Perm (Fin m)) : r324LayerSplitGrade τ ≤ (r324LayerSplit τ).card + 1

theorem Anderson4D.r324LayerSplit_one (m : ℕ) : r324LayerSplit 1 = {j : Fin m | 1 ≤ ↑j}

The identity has every decomposition point.

theorem Anderson4D.r324LayerSplitGrade_one {m : ℕ} (hm : 2 ≤ m) : r324LayerSplitGrade 1 = m - 1

The identity carries the full window power m-1.

theorem Anderson4D.r324LayerSplitGrade_of_split_empty {m : ℕ} {τ : Equiv.Perm (Fin m)} (hm : 2 ≤ m) (h : r324LayerSplit τ = ∅) : r324LayerSplitGrade τ = 1

A bijection with no decomposition point has grade 1.

theorem Anderson4D.r324LayerSplit_simple_four : r324LayerSplit ((↑[0, 1, 3, 2]).formPerm ⋯) = ∅

The simple permutation (2,4,1,3) of R324CappedCrossGrading has no decomposition point.

theorem Anderson4D.r324LayerSplitGrade_simple_four : r324LayerSplitGrade ((↑[0, 1, 3, 2]).formPerm ⋯) = 1

The deranged m = 4 bijection has grade 1, matching the proved table of R324CappedCrossGrading.

theorem Anderson4D.r324Layer_split_not_dominated_by_coincidence : (r324GradeCoincidence ((↑[0, 1, 3, 2]).formPerm ⋯ * (↑[4, 5, 7, 6]).formPerm ⋯)).card + 1 < r324LayerSplitGrade ((↑[0, 1, 3, 2]).formPerm ⋯ * (↑[4, 5, 7, 6]).formPerm ⋯)

The split grade is not dominated by the adjacency coincidences. The direct sum of two copies of the simple permutation (2,4,1,3) has a decomposition point at 4 and no adjacency coincidence at all, so the hypothesis gradeP τ ≤ #coincidences + 1 of r324Grade_permLayerCount_of_coincidence fails for the split grade. That is why r324Layer_permLayerCount_split below proves the layer count for the split grade directly, from its own subset count.

The layer count of the split grade

theorem Anderson4D.r324LayerFactorial_mul_le {a : ℕ} (ha : 1 ≤ a) (n : ℕ) : a.factorial * (n + 1).factorial ≤ (a + n).factorial

def Anderson4D.r324LayerSplitAt (m : ℕ) (T : Finset ℕ) : Finset (Equiv.Perm (Fin m))

Bijections with prescribed decomposition points (indexed by ℕ).

Equations

• Anderson4D.r324LayerSplitAt m T = {τ : Equiv.Perm (Fin m) | ∀ j ∈ T, 1 ≤ j ∧ j < m ∧ ∀ i < j, Anderson4D.r324LayerPos τ i < j}

theorem Anderson4D.r324LayerSplitAt_mem {m : ℕ} {T : Finset ℕ} {τ : Equiv.Perm (Fin m)} : τ ∈ r324LayerSplitAt m T ↔ ∀ j ∈ T, 1 ≤ j ∧ j < m ∧ ∀ i < j, r324LayerPos τ i < j

def Anderson4D.r324LayerHead {m : ℕ} (τ : Equiv.Perm (Fin m)) (j : ℕ) (a : Fin j) : Fin j

The head block of a decomposed bijection.

Equations

• Anderson4D.r324LayerHead τ j a = ⟨min (Anderson4D.r324LayerPos τ ↑a) (j - 1), ⋯⟩

def Anderson4D.r324LayerTail {m : ℕ} (τ : Equiv.Perm (Fin m)) (j : ℕ) (a : Fin (m - j)) : Fin (m - j)

The tail block of a decomposed bijection.

Equations

• Anderson4D.r324LayerTail τ j a = ⟨min (Anderson4D.r324LayerPos τ (j + ↑a) - j) (m - j - 1), ⋯⟩

theorem Anderson4D.r324LayerHead_val {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hsplit : ∀ i < j, r324LayerPos τ i < j) (a : Fin j) : ↑(r324LayerHead τ j a) = r324LayerPos τ ↑a

theorem Anderson4D.r324LayerHead_injective {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (hsplit : ∀ i < j, r324LayerPos τ i < j) : Function.Injective (r324LayerHead τ j)

theorem Anderson4D.r324LayerPos_ge_of_split {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (hsplit : ∀ i < j, r324LayerPos τ i < j) {a : ℕ} (haj : j ≤ a) (ham : a < m) : j ≤ r324LayerPos τ a

Labels above a decomposition point occupy slots above it.

theorem Anderson4D.r324LayerTail_val {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (_hsplit : ∀ i < j, r324LayerPos τ i < j) (a : Fin (m - j)) : ↑(r324LayerTail τ j a) = r324LayerPos τ (j + ↑a) - j

theorem Anderson4D.r324LayerTail_injective {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (hsplit : ∀ i < j, r324LayerPos τ i < j) : Function.Injective (r324LayerTail τ j)

noncomputable def Anderson4D.r324LayerHeadPerm {m : ℕ} (τ : Equiv.Perm (Fin m)) (j : ℕ) : Equiv.Perm (Fin j)

The head block as a bijection of Fin j.

Equations

• Anderson4D.r324LayerHeadPerm τ j = if h : Function.Injective (Anderson4D.r324LayerHead τ j) then Equiv.ofBijective (Anderson4D.r324LayerHead τ j) ⋯ else 1

noncomputable def Anderson4D.r324LayerTailPerm {m : ℕ} (τ : Equiv.Perm (Fin m)) (j : ℕ) : Equiv.Perm (Fin (m - j))

The tail block as a bijection of Fin (m-j).

Equations

• Anderson4D.r324LayerTailPerm τ j = if h : Function.Injective (Anderson4D.r324LayerTail τ j) then Equiv.ofBijective (Anderson4D.r324LayerTail τ j) ⋯ else 1

theorem Anderson4D.r324LayerHeadPerm_pos {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (hsplit : ∀ i < j, r324LayerPos τ i < j) {i : ℕ} (hi : i < j) : r324LayerPos (r324LayerHeadPerm τ j) i = r324LayerPos τ i

theorem Anderson4D.r324LayerTailPerm_pos {m : ℕ} {τ : Equiv.Perm (Fin m)} {j : ℕ} (hjm : j < m) (hsplit : ∀ i < j, r324LayerPos τ i < j) {i : ℕ} (hi : i < m - j) : r324LayerPos (r324LayerTailPerm τ j) i = r324LayerPos τ (j + i) - j

theorem Anderson4D.r324LayerSplitAt_card_le (m : ℕ) (T : Finset ℕ) : (r324LayerSplitAt m T).card ≤ (m - T.card).factorial

The split count. At most (m-|T|)! bijections have all the prescribed decomposition points in T: the blocks between consecutive points are permuted independently, and ∏ bₜ! ≤ (m-|T|)!.

The σ-grading layer count for the split grade

theorem Anderson4D.r324LayerSplit_subsetCount {m : ℕ} (S : Finset (Fin m)) : ↑{τ : Equiv.Perm (Fin m) | S ⊆ r324LayerSplit τ}.card ≤ 1 ^ m * ↑(m - S.card).factorial

theorem Anderson4D.r324Layer_permLayerCount_split {m : ℕ} (hm : 1 ≤ m) : R324GradePermLayerCount 4 m r324LayerSplitGrade

The σ-grading layer count for the split grade, unconditionally. Grade j is carried by at most 4^m·(m-j)! bijections. Combined with r324Grade_layeredAt_of_collapse this is the entire counting half of clause A for the grade the lattice actually produces; only the per-τ graded lattice budget R324ColGradedBudgetAt remains.

theorem Anderson4D.r324Layer_permLayerCount_split_three : R324GradePermLayerCount 4 3 r324LayerSplitGrade

The order-three slice. At m = 3 the split grade obeys the layer count, and the identity still carries the full power m-1 = 2 (r324LayerSplitGrade_one) — the proved flat calibration r324Grade_permLayerCount_flat_three is the same slice with the grade rounded up to 2 for all six bijections.

theorem Anderson4D.r324LayerSplitGrade_one_three : r324LayerSplitGrade 1 = 2

Analytic input for clause A

Together with the adjacency statistic r324Layer_gradeCoincidenceCount, r324Layer_permLayerCount_split supplies the counting half of the σ-grading. The analytic input of r324Grade_cappedCrossLedger_of_gradedLattice is

R324ColGradedBudgetAt ρ D m r324LayerSplitGrade,

i.e. ∑_q ∏ᵢ‖ρ̂(εqᵢ)‖²·∏ⱼ⟨Sⱼ⟩⁻²⟨Sⱼ^τ⟩⁻² ≤ D^m·|log ε|^{grade τ} over the zero-sum sector. Its inductive step is: if j is the least decomposition point of τ, the zero-sum lattice sum factorises over the head block {0,…,j-1} and the tail block {j,…,m-1} (the head keys sum to Sⱼ, which is the only variable shared with the tail), *the head factor is the j-key sum at the reduced grade of τ|head and the tail factor is the (m-j)-key sum at the reduced grade of τ|tail, and the shared variable Sⱼ is summed once against ⟨Sⱼ⟩⁻⁴, contributing one factor |log ε|* (r324SW_translated_window_le_log)*, giving grade τ = grade(head) + grade(tail) + 1, which is exactly the recursion satisfied by r324LayerSplitGrade* (the two extremes being τ = id, where the recursion iterates m-1times, and aτwith no decomposition point, where it stops immediately atgrade = 1, the single free window of the whole zero-sum cube). The base case with no decomposition point is the proved R324ColDoubledBudgetAtroute: `r324Col_tsum_latWeight_lealready bounds *every*τby the identity pattern, which is|log ε|^{m-1}; the content of the general step is that a τwithout decomposition points is bounded by a *single* log, for which the pinned keys must be eliminated by the zero-sum constraint rather than summed (a freely summed key costsε⁻⁴, r324SW_symbol_mass_le, and a marked one ε⁻⁸, r324RoutedWindow_marked_window_le`).