A Walsh normal form for the binary Burnside operator, the p⁺-expansion conjectured by Diaconis, Lin and Ram, and the support blocks of the k-ary chain

Conjecture 6.3 of arXiv:2512.23285v1 as a matrix identity for n = 1..7: the binary Burnside operator Kₙ on C₂ⁿ, built from the source's own two-step process (K(x,y) = |Gₓ|⁻¹ sum_(s in Gₓ cap G_y) 2^(-c(s))), equals sum_(x+y+z=n) c_(y,z) f(x,y,z) with f the sum over all 3ⁿ orderings of Kronecker products of p+, p-, p+h and c_(y,z) = (y!z!/((y/2)!(z/2)!((y+z)/2)!2ʸ⁺ᶻ))². Both sides coded literally; native_decide.

The weights the source prints in its K₄ and K₆ expansions (c_(0,0)=1, c_(2,0)=c_(0,2)=1/4, c_(4,0)=c_(0,4)=9/64, c_(2,2)=1/64, c_(6,0)=c_(0,6)=25/256, c_(2,4)=c_(4,2)=1/256) reproduced from the closed formula, and c_(y,z) = 0 exactly when y or z is odd, for y+z <= 8. Kernel-clean by cross-multiplication over N (decide, no axioms).

Negative controls for Conjecture 6.3: doubling c_(2,0) breaks it at n = 2 and n = 3; deleting the parity case distinction in c_(y,z) (which makes c_(1,1) = 1/16) breaks it at n = 2; deleting the p+h terms breaks it at n = 2; replacing 'sum over all orderings' by 'number of orderings times the sorted ordering' is correct at n = 2 and false at n = 3; Kₙ is not symmetric (the orientation is K, not K^T); Kₙ is stochastic for n <= 5.

The 2x2 algebra behind Conjecture 6.3, kernel-clean over Z after clearing the factor 2: the source's displays 2p+ = 1+e+f, 2p- = 1-e-f, 2p+h = (1+e+f)h; the sl₂ relations [e,f]=h, [h,e]=2e, [h,f]=-2f; p+ and p- complementary orthogonal idempotents with (p+h)² = 0; and the change of basis p+ H = H E₁1, p- H = H E₂2, p+h H = H E₁2 for H = [[1,1],[1,-1]], which turns a Kronecker product of x copies of p+, y of p-, z of p+h into the single matrix unit E_(S,T) with S subset T, |S| = y, |T S| = z.

Closed form of the binary Burnside kernel: sum_(sigma in Sₘ) 2^(-c(sigma)) = (2m)!/(4ᵐ m!) (checked by enumeration for m <= 7), hence K(x,y) = w(a0,a1) w(b0,b1) with w(s,t) = R(s)R(t)/(s+t)! and (a0,a1,b0,b1) the joint type of (x,y); verified against the literal process for n <= 6. In particular K(x,y) depends on (x,y) only through the joint type.

Cycle-parity lemma: for a uniform sigma in Sₘ and a fixed t-subset, the probability that every cycle of sigma meets the subset in an even number of points is binom(t,t/2)/2ᵗ for t even and 0 for t odd – independent of m. Kernel-bound by enumeration for all m <= 8 and all t <= m.

The core identity sum_(i<=y) sum_(j<=z) (-1)ⁱ binom(y,i) binom(z,j) gammaᵢ₊ⱼ gamma_(y+z-i-j) = 2ʸ⁺ᶻ c_(y,z) with gammaₜ = binom(t,t/2)/2ᵗ, kernel-bound for y+z <= 20; and its arithmetic core, von Szily's identity p!q!(p+q)! sumᵢ (-1)ⁱ binom(2p,i) binom(2q,p+q-i) = (-1)ᵖ (2p)!(2q)! (the super Catalan number S(p,q)), kernel-clean over Z (decide, no axioms) for p,q <= 10.

Correction to arXiv:2512.23285v1: its sentence after Conjecture 6.3, 'the constants c_(k,k) are exactly the eigenvalues betaₖ of our Markov chain', is false for the c it defines – c_(k,k) = 0 for odd k, c_(2,2) = 1/64 against beta₂ = 9/64, and among k <= 8 the only k with c_(k,k) = betaₖ is k = 0. The weights that are the eigenvalues are c_(2k,0) = c_(0,2k) = binom(2k,k)²/2⁴ᵏ = betaₖ, checked for k <= 8. Kernel-clean by cross-multiplication over N.

Walsh normal form of the binary Burnside operator: with H = [[1,1],[1,-1]] and K ₙ = 2⁻ⁿ H^(ot n) Kₙ H^(ot n), the entry K ₙ[S,T] is c_(|S|,|T S|) when S subset T and 0 otherwise – so Kₙ is triangular for the inclusion order in the Walsh basis, with an entry that does not depend on n. Kernel-bound for n <= 7 from the process itself and for n <= 10 through the closed form BP5; the conjecture's right-hand side has the same normal form for n <= 5. With BP4 the two statements 'Conjecture 6.3 at n' and 'K ₙ = triMat n' are equivalent.

The source's eigenvalue table recovered from the normal form: for n <= 8 the diagonal of the Walsh-transformed Burnside operator carries betaₖ = binom(2k,k)²/2⁴ᵏ exactly binom(n,2k) times and 0 exactly 2ⁿ⁻¹ times – the source's display (1.3) – because a matrix triangular for a partial order is triangular for any linear extension of it.

Conjecture 6.3 in n-free form, for every n <= 24: both sides depend on the pair of states only through the joint type (a0,a1,b0,b1), the left as w(a0,a1)w(b0,b1) and the right as 2⁻ⁿ sum_(y,z) c_(y,z) [uʸ vᶻ] (1+u+v)ᵃ⁰(1-u-v)ᵃ¹(1-u+v)ᵇ⁰(1+u-v)ᵇ¹; the two agree on every one of the binom(n+3,3) types for every n <= 24. The bridges to the literal matrices are checked for n <= 6 (left, BP5) and n <= 5 (right).

Conjecture 6.3 of arXiv:2512.23285v1 holds for every n. Proof (record section 3): (i) in the Hadamard basis p+, p-, p+h are the matrix units E₁1, E₂2, E₁2 and words correspond bijectively to pairs S subset T, so the conjecture is equivalent to the normal form BP9; (ii) the inner Fourier sum sum_y K(x,y)(-1)^(|T cap y|) is the probability that every cycle of a uniform sigma in Gₓ meets T evenly, which by the cycle-parity lemma BP6 equals gamma_(|T cap A|) gamma_(|T cap B|); (iii) the alternating outer sum vanishes unless S subset T and otherwise leaves an n-free quantity S(y,z); (iv) S(y,z) = 2ʸ⁺ᶻ c_(y,z) by a constant-term computation that reduces to von Szily's identity (BP7). Corollaries: the source's eigenvalue table, and the correction BP8.

Cost profile of this family: no import Mathlib anywhere (Rat, Array, List from core; factorial and binomial defined locally), so every module peaks at 1.6 GB RSS instead of the 3.3-6.6 GB Mathlib baseline, and the whole family re-checks in 27 minutes of wall clock (Defs 7 s, Weights 7 s, NormalForm 252 s, Instances 356 s, Structure 435 s, TypeForm 565 s). Rat arithmetic does not reduce in the Lean kernel (Rat.add normalises through Nat.gcd), so every rational-valued check is native_decide while the integral ones (2x2 algebra, von Szily, the correction) are decide and axiom-free. The literal 3ⁿ-ordering right-hand side costs 12x per step in n: n = 6 is 16 s, n = 7 is 257 s, n = 8 would be about 1 h – over the single-file stop rule, which is why n <= 7 is the literal range and the type form carries the rest.

What the weights of Conjecture 6.3 are, for ALL y,z (not a finite range): c_(y,z) = c_(z,y) (so exchanging p- and p+h leaves the conjecture's right-hand side unchanged), c_(y,z) = 0 as soon as y or z is odd, and c_(2p,2q) = (S(p,q)/4^(p+q))² where S(p,q) = (2p)!(2q)!/(p!q!(p+q)!) is the super Catalan number – i.e. the constants of the conjecture are squares of normalised super Catalan numbers, which is why the core identity BP7 is von Szily's identity. Kernel-clean (decide/rfl, no axioms at all).

Von Szily's identity for every p and q, kernel-clean: (sumᵢ (-1)ⁱ binom(2p,i) binom(2q,p+q-i)) * p! q! (p+q)! = (-1)ᵖ (2p)!(2q)!, proved from the differential equation (1-X²) A' = A((b-a) - (a+b)X) for A = (1-X)ᵃ (1+X)ᵇ and the resulting three-term coefficient recurrence. With it: integrality of the super Catalan number S(p,q) = (2p)!(2q)!/(p!q!(p+q)!) for all p,q; the palindrome reflect(a+b) A = (-1)ᵃ A; and the vanishing of the middle coefficient [Xʰ] (1-X)ᵃ (1+X)ᵇ = 0 for a odd and a+b = 2h (which is why c_(y,z) = 0 at odd arguments). A bridge lemma identifies the family's Mathlib-free szilySum / chs / fct with Finset.sum / Nat.choose / Nat.factorial, so vonₛzily of Structure.lean (p,q <= 10, decide, row BP7) is literally the finite instance.

The core identity of Conjecture 6.3 for every y and z, kernel-clean: sum_(i<=y) sum_(j<=z) (-1)ⁱ binom(y,i) binom(z,j) gammaᵢ₊ⱼ gamma_(y+z-i-j) = 2ʸ⁺ᶻ c_(y,z) with gammaₜ = binom(t,t/2)/2ᵗ, stated in the family's own coreSum and cYZ. Proof: the constant-term computation of the founding record's section 3.4 carried out in the ordinary polynomial ring Z[u][v] (after u = p², v = q²): [uʰ vʰ] (u+v)ᵃ (uv+1)ᵇ = mid(a) mid(b) when a+b = 2h, and (uv+1) -/+ (u+v) = (u-1)(v-1) / (u+1)(v+1), so the double sum is ([uʰ] (u-1)ʸ (u+1)ᶻ)², which von Szily (BP15) evaluates. The odd cases come from the middle-coefficient vanishing of BP15.

The cycle-parity constant for every block size, kernel-clean: sumᵢ₌₀ᵐ Xⁱᵗ (1+X)ᵐ⁻ᵗ) * w(m-i, i) = gammaₜ for all t <= m, where w(s,t) = R(s)R(t)/(s+t)! is the closed-form block weight of row BP5 – so the constant does not depend on the block size m. Proof, permutation-free: clearing R(i) = (2i-1)!!/2ⁱ turns it into LW(m,t) = 2ᵐ⁻ᵗ m! mid(t) for an integer sum, Pascal's rule plus (2i-1)!! recursion give LW(m+1,t) = 2(m+1) LW(m,t) in one line, the t = 0 case is the central-binomial convolution sumᵢ binom(2i,i) binom(2(m-i),m-i) = 4ᵐ, and the diagonal is sumᵢ (-1)ⁱ binom(2i,i) binom(2(t-i),t-i) = 2ᵗ binom(t,t/2), proved by square-root uniqueness in Z[[X]] (two integer sequences with the same convolution square and constant term 1 are equal).

Triangularity and n-freeness of the Walsh entry of the binary Burnside operator, for every n, kernel-clean. With s1, s2, s3, s4 the sizes of S cap T, S T, T S and [n] (S cup T), the four-fold region sum walshEntry s1 s2 s3 s4 – which is 2ⁿ times the Walsh entry K ₙ[S,T] by the region decomposition of section 3.3 of the founding record, a step that is NOT formalised here – equals 0 when s2 /= 0 (i.e. S not subset T) and 2ˢ¹⁺ˢ³⁺ˢ⁴ c_(s1,s3) when s2 = 0 – so for S subset T the entry is c_(|S|,|T S|) and n does not occur in it. Proved for all s1,s2,s3,s4 from sumᵢ₂ (-1)ⁱ² binom(s2,i2) = [s2 = 0], sumᵢ₄ binom(s4,i4) = 2ˢ⁴ and the core identity BP16.

The k-ary Burnside kernel in closed form equals the literal process. With Rₖ(m) = sum_(sigma in Sₘ) k^(-c(sigma)) = prod_(i<m) (1/k + i) (the classical sum_(sigma in Sₘ) u^(c(sigma)) = u(u+1)...(u+m-1) at u = 1/k) and N_cd = #i: xᵢ = c, yᵢ = d, K(x,y) = prod_(c in Z/k) (prod_(d in Z/k) Rₖ(N_cd)) / n_c! with n_c = sum_d N_cd. Checked entry by entry against the literal |Gₓ|⁻¹ sum_(sigma in Gₓ cap G_y) k^(-c(sigma)), computed by walking every one of the n! permutations, counting its cycles and distributing its mass over the pairs of states it fixes: k = 2 for n <= 4, k = 3 for n <= 4, k = 4 for n <= 3. The k = 2 case is BP5.

Cycle-residue lemma for the k-ary Burnside process: for a uniform sigma in Sₘ and a colouring of [m] by Z/k with tᵣ points of colour r (r = 1..k-1) and m₀ points of colour 0, the probability that every cycle of sigma has colour-sum = 0 mod k equals Gammaₖ(t₁,...,tₖ₋₁) and is INDEPENDENT of m₀. Three kernel-bound checks: (i) the counting recursion equals brute-force enumeration of Sₘ for k = 2, 3, 4 and every type of total weight <= 6; (ii) the m₀-independence for k = 2, 3 and every colouring of at most 7 points; (iii) the exponential generating function Gammaₖ(t) = (prodᵣ tᵣ! / (sumᵣ tᵣ)!) [wᵗ] det Circ(1, -w₁,..., -wₖ₋₁)^(-1/k) for k = 2, 3 to total degree 6 and k = 4 to total degree 4, with the circulant determinant computed from the definition of a determinant (sum over permutations with signs) so that no root of unity appears anywhere. det Circ = 1 - w² for k = 2 and 1 - w1³ - 3 w1 w2 - w2³ for k = 3. Gamma₂(t) = binom(t,t/2)/2ᵗ recovers BP6, the cycle-parity lemma of the k = 2 proof.

Support triangularity of the k-ary Burnside operator in an integer basis. On functions on Z/k take g₀ = 1 (constant) and gᵣ = deltaᵣ (r = 1..k-1); the change of basis G is unimodular over Z (G⁻¹ G = G G⁻¹ = 1 checked by decide for k = 2,3,4,5, kernel-clean), and a tensor g_(a₁) ox... ox g_(aₙ) is a function of x restricted to supp a = i: aᵢ /= 0. With Cₙ = (G⁻¹)^(ot n) Kₙ G^(ot n), the entry Cₙ[a',a] vanishes unless supp a' subset supp a. Checked at every one of the k²ⁿ index pairs for k = 2 with n <= 6, k = 3 with n <= 5, k = 4 with n <= 4: 0 violations. The same integer basis replaces the DFT of Z/k used in the design pull, which is what keeps the family Mathlib-free and every check exact over Q.

The block identity for the k-ary Burnside operator, bound as an explicit unimodular similarity. Cₙ = (G⁻¹)^(ot n) Kₙ G^(ot n) is support-triangular AND n-free: for supp a' subset supp a = T with |T| = t, Cₙ[a',a] equals Cₜ[a'|_T, a|_T], the corresponding entry of the smaller normal form, with n absent from the right-hand side. Checked at every index pair for k = 2 with n <= 6, k = 3 with n <= 5, k = 4 with n <= 4 (0 violations), together with the unimodularity of G and the agreement of the one-tensor-factor-at-a-time sweeps with the naive dense Kronecker products. Consequence (ordinary linear algebra): ordering the kⁿ words by |supp| puts Cₙ in block-triangular form whose level-t diagonal block is block-diagonal with binom(n,t) copies of the n-free (k-1)ᵗ x (k-1)ᵗ operator Dₜ, so charpoly(Kₙ)(z) = prodₜ₌₀ⁿ charpoly(Dₜ)(z)^(binom(n,t)) and mult_(Kₙ)(lambda) = sumₜ mult_(Dₜ)(lambda) binom(n,t) with coefficients independent of n. Since the functions n -> binom(n,t) are linearly independent, Conjecture 6.4 of arXiv:2512.23285v1 for a given k is EXACTLY the statement that the nonzero spectra of D₀, D₁, D₂,... are pairwise disjoint. Dₜ is also checked equal to the n-free type formula Dₜ[b] = sum_(0<=e<=b) (-1)^(|e|) (prod binom(bᵣd,eᵣd)) Kₜype(N(e)), which is what makes levels t = 8..16 computable at all. Dimensions check: sumₜ binom(n,t)(k-1)ᵗ = kⁿ.

The source's eigenvalue 1/18 pinned to a unique level, and two more with it. (i) 1/18 is an eigenvalue of D₄ (k = 3) of geometric multiplicity at least 2: two explicit INTEGRAL eigenvectors of the 16 x 16 block, v1 = (0,0,0,0,0,1,-1,0,0,-1,1,0,0,0,0,0) and v2 = (0,0,0,1,0,0,-1,0,0,-1,0,0,1,0,0,0) in the word ordering of nzWords 3 4, each satisfying D₄ v = v/18, with the 2x2 minor on rows 3 and 5 equal to -1 so they are independent. (ii) 1/18 is an eigenvalue of NO other level t <= 8: Rₜ(1/18) /= 0 for every t <= 8 with t /= 4 while R₄(1/18) = 0, where Rₜ is the annihilator of KB9. Hence b_(1/18) = 4 is unique and mult_(Kₙ)(1/18) = 2 binom(n,4) = 2, 10, 30, 70 at n = 4, 5, 6, 7 – the table printed in arXiv:2511.01245 section 6, now derived with a bₗambda that is proved rather than suggested. The same pin for 4/243 (level 8; Rₜ(4/243) /= 0 for every t <= 7, R₈(4/243) = 0, multiplicity 14 binom(n,8)) and for 6857/885735 (level 12; Rₜ /= 0 for every t <= 11, multiplicity 132 binom(n,12)).

The rectangular eigenvalue family of the k-ary Burnside process. For mu = (aᵏ⁻¹) at level t = a(k-1) the GLₖ₋₁-block is one-dimensional, so Dₜ acts on it as a SCALAR thetaₐ computable from the n-free type formula alone: thetaₐ = sum over compositions c of a indexed by Sₖ₋₁ of sgn(c) (a!/prodₚi cₚi!) D_(a(k-1))[sumₚi cₚi Pₚi]; for k = 3 this is thetaₐ = sumᵤ (-1)ᵘ binom(a,u) D₂ₐ[(a-u, u; u, a-u)]. Bound values: k = 3 gives theta₁ = 0, theta₂ = 1/18, theta₃ = 0, theta₄ = 4/243, theta₅ = 0, theta₆ = 6857/885735, theta₇ = 0, theta₈ = 357161/79716150; k = 4 gives theta₂ = 3/256; k = 5 gives theta₂ = 3/1250. Multiplicity in Kₙ is f^((aᵏ⁻¹)) binom(n, a(k-1)), the number of standard Young tableaux of the (k-1) x a rectangle (Catalan for k = 3): 2 binom(n,4), 14 binom(n,8), 132 binom(n,12), 1430 binom(n,16) for k = 3 and 5 binom(n,6) for k = 4. The a = 2, k = 3 member is exactly the source's 1/18 with its printed table. Control: thetaₐ is not a Gammaₖ product – Gamma₃(2,2) Gamma₃(4,4)² = 361/24300 /= 4/243 = theta₄, which is why the k = 2 von Szily / super-Catalan endgame has no k >= 3 analogue.

Conjecture 6.4 of arXiv:2512.23285v1 for k = 3 and every n <= 16, via exact cross-level coprimality. The Sₜ-isotypic refinement Dₜ = sum over mu of (id_(Sᵐu) ox Dₜᵐu) splits charpoly(Dₜ) into 62 irreducible nonzero factors over Q across t <= 16, each of degree at most 3; they are recorded in primitive integer form with their labels (t, mu₁, mu₂, fᵐu). For EVERY one of the 1891 pairs i < j – cross-level and within-level – there is a Bezout certificate u Pᵢ + v Pⱼ = c with u, v in Z[z] and c a nonzero integer, so a common root would force c = 0 and the 62 are pairwise coprime. The certificate list is checked to cover exactly allPairs 62 in lexicographic order and the 62 coefficient lists to be pairwise distinct. Everything is integer polynomial arithmetic, so all three theorems are decide: checked by the Lean kernel with NO native_decide axiom (#print axioms is empty for the shape and coverage theorems and [propext] for the coprimality theorem). With KB4 this gives: no two levels t /= t' <= 16 share a nonzero eigenvalue, hence every nonzero eigenvalue of Kₙ for n <= 16 occurs with multiplicity aₗambda binom(n, bₗambda), bₗambda the unique level and aₗambda = sumₘu fᵐu mult_(D_(b)ᵐu)(lambda). Certificate size: 70350 digits in total, largest integer 48 digits. What is kernel-checked: the 1891 Bezout identities. What is cited: that these 62 polynomials are the nonzero irreducible factors of charpoly(Dₜᵐu) (exact Q-factorisation of the isotypic blocks, Schur-Weyl for GL₂ x Sₜ, reproduced in the record; kernel-checked independently for t <= 8 by KB9), and – only for identifying algebraic with geometric multiplicity – the non-negative spectrum and diagonalisability of Feng, arXiv:2510.25202.

Negative controls for the k-ary rows. (i) A wrong block gives a different normal form: shifting the (w₀,w₀) diagonal entry of the level-t table by 1 breaks the block identity at every level t <= 3 for k = 3 and at t = 2 for k = 4 (entry 0 of a level-t block is never consulted for t >= 1, because a column index of full support has no zero digit – so the naive perturbation is the wrong control and is recorded as such). (ii) The triangularity is strictly triangular and one-sided: there are nonzero entries with supp a' a proper subset of supp a, and zero entries in the transposed pattern. (iii) D₁ = 0 while D₀ = (1) and Dₜ /= 0 for t = 2,3,4 (k = 3) and t = 2 (k = 4) – which is why bₗambda is never 1. (iv) Kₙ is stochastic and reversible for pi(x) proportional to |Gₓ| (|Gₓ| K(x,y) = |G_y| K(y,x), checked for k = 3, n <= 3) but is NOT a symmetric matrix: K((0,0),(0,1)) = 1/18 while K((0,1),(0,0)) = 1/9. (v) Gammaₖ(t) = 0 unless sumᵣ r tᵣ = 0 mod k, and is nonzero on the residue-0 types. (vi) The Bezout check is not vacuous: perturbing c or a coefficient of u makes it fail, a polynomial has no constant Bezout combination with itself, and for the genuinely non-coprime pair 18z - 1 and (18z-1)(27z-5) the Euclidean combination is 0, not a nonzero constant. (vii) The annihilators are needed in full: neither 27z - 5 nor 18z - 1 annihilates D₄ alone, R₄ does not annihilate D₅, R₇ does not annihilate D₈, and the same for k = 4 at t = 4, 5.

Annihilating polynomials for the support blocks: Conjecture 6.4 for k = 3 and n <= 8 without any representation theory. With Rₜ:= prodₘu Pₜᵐu (the product of the distinct nonzero irreducible factors of charpoly(Dₜ), from KB7's list), the single exact matrix identity Rₜ(Dₜ). Dₜ = 0 holds over Q on the full 2ᵗ x 2ᵗ block for every t <= 8. It gives spec(Dₜ) contained in 0 union roots(Rₜ) outright: if Dₜ v = lambda v with v /= 0 then Rₜ(lambda) lambda = 0. Combined with KB7's axiom-free pairwise coprimality, no two levels t /= t' <= 8 share a nonzero eigenvalue – kernel-checked end to end, with no Schur-Weyl decomposition, no cited factorisation and no linear-algebra routine whose correctness has to be assumed. With KB4 (kernel-bound for k = 3 at n <= 5, and Theorem A of the design journal for larger n) this is Conjecture 6.4 for k = 3 and every n <= 8. It also confirms, at every t <= 8 and independently of Feng arXiv:2510.25202, that the minimal polynomial of Dₜ is z Rₜ, i.e. squarefree, i.e. that Dₜ is diagonalisable.

k = 4 done exactly: Conjecture 6.4 for k = 4 and every n <= 5 kernel-bound, n <= 6 computed. For each t <= 6 the minimal polynomial of the block Dₜ (size 3ᵗ) was computed exactly over Q by a Krylov dependence on the exact rational matrix; its nonzero part factors into 11 primitive integer polynomials: z - 1 (t=0), none (t=1, D₁ = 0), 8z - 3 (t=2), 8z - 1 (t=3), 32z - 3 and 2048z² - 468z + 9 (t=4), 16z - 1, 64z - 1, 256z - 21 (t=5), 256z - 3, 196608z² - 12416z + 107 and 4194304z³ - 790528z² + 32316z - 315 (t=6). All 55 pairs carry Bezout certificates over Z (decide, kernel-checked, no native_decide axiom), so no two levels t /= t' <= 6 share a nonzero eigenvalue; and Rₜ(Dₜ). Dₜ = 0 is checked exactly over Q on the full 3ᵗ x 3ᵗ block for every t <= 5, which is what makes the coprimality a statement about the actual spectra. At t = 6 the block is 729 x 729 and Horner evaluation of R₆ (degree 6) costs about 2.7 x 10⁹ exact rational operations, over the budget; there the identity was verified modulo two primes (999983 and 999979) outside Lean in 120 s, which is what extends the computed range to n <= 6. Cross-check: 256z - 3 at t = 6 is the rectangular scalar theta₂ = 3/256 of KB6, predicted from the one-dimensional GL₃-block of the 2x2x2 rectangle and found independently in a 729 x 729 block built from the process. The k = 4 levels carry cubic irrationalities already at t = 6, one level earlier than k = 3 (t = 12).