Where the substitution method stops on the short product over 𝔽₂
Abstract
Let T_N be the structure tensor of the short (truncated) product 𝔽₂[x]/x^N, whose rank R(T_N) is the number of coefficient multiplications a bilinear algorithm for that product needs. The value R(T₅) sits at the boundary of what exhaustive search reaches: the bound R(T₅) ≥ 10 is classical, the matching R(T₅) ≥ 11 rests on a single covering-sets computation reported in a summary table, and no independent verification of it exists. We show that the substitution method, in the form of the explicit one-level ladder it yields for T_(N+1), provably cannot supply the missing unit. Restated on subspaces of matrices, the ladder reduces R(T₅) ≥ 3+m to the minimum m of a rank functional over a family of 4-dimensional subspaces of 𝔽₂^(4 × 4) indexed by 4096 parameter triples. We prove that this minimum is exactly 7: one member is contained in the span of seven rank-one matrices – and exactly seven rank-one matrices lie in that span, so the witness is complete – while no member at all is contained in the span of six, a statement certified by exhausting 103,643,136 candidate subspaces. Since the slice space of T₄ needs eight, the comparison is exact and the ladder yields R(T₅) ≥ 10, never 11. The same machinery produces certificates, checked by the Lean 4 kernel, for the exact values R(T₃)=5 and R(T₄)=8 in both directions, and for the exact symmetric ranks of 𝔽₂[x]/x^N for N ≤ 5 and of 𝔽₂[x]/(x^N-1) for N ∈ {3,5,6}, together with Rˢʸᵐ(T₆) ∈ {13,14}. Those values are published; the certificates are new.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
050e4d4755935a79bc71170c97c6752263e6092a08b44c7b696468e0e4354813
Claim ledger
Stated results
trunc-01routine2026-08-23
Bilinear schemes for F_q[x]/x^N, the defining identities, and soundness over every commutative semiring
trunc-02routine2026-08-23
Transfer along a ring hom, and padding: TruncRankLE.map,.ofᵢnt,.succ,.mono
trunc-03routine2026-08-23
The decidable layer: tables, identCheck, and the bridge identCheckᵢff
trunc-04known2026-08-23
R_(F₂)(F₂[x]/x²) <= 3, R_(F₂)(F₂[x]/x³) <= 5, R_(F₂)(F₂[x]/x⁴) <= 8: explicit schemes, every identity in the kernel
trunc-05known2026-08-23
R_(F₂)(T₅) <= 11 and R_(F₂)(T₆) <= 14: explicit bilinear algorithms for the short product mod x⁵ and mod x⁶, all 125 and 216 identities in the kernel
trunc-06known2026-08-23
R_(F₂)(F₂[x]/x²) = 3 exactly, both directions kernel-checked
trunc-07routine2026-08-23
Negative controls: non-vacuity, a dropped product, a swapped table, a wrong length, and characteristic 2
trunc-08known2026-08-23
OPENNESS CHECK, NOT A THEOREM: R_(F₂)(T₅) = 11 is already published, so arXiv:2603.07280's Table 6 gap is stale and the queue cell is closed
This ledger entry is reported in prose and is not bound to a Lean theorem.trunc-09routine2026-08-23
PRICED FRONTIER, NOT A THEOREM: the lower bound R >= 11, and the neighbouring open cells, are out of reach of both routes built here
This ledger entry is reported in prose and is not bound to a Lean theorem.trunc-10routine2026-08-30
The F₂ span engine: R_G(V) = mindim W: V subseteq W, W spanned by the atoms it contains, its echelon linear algebra, and the master theorem topSearchₒf_gens – a false search answer refutes every rank-r decomposition
trunc-11known2026-08-30
Explicit SYMMETRIC bilinear schemes (b = a) for the truncated product: Rₛym(T₃) <= 5, Rₛym(T₄) <= 8, Rₛym(T₅) <= 11, Rₛym(T₆) <= 14, every N³ identity by kernel decide
trunc-12known2026-08-30
The cyclic product F₂[x]/(x^N - 1) added to the family, with soundness over every commutative semiring, and symmetric schemes giving R(C₃) <= 4, R(C₅) <= 10, R(C₆) <= 12
trunc-13routine2026-08-30
Negative controls for the symmetric witnesses: a too-large claim, a too-small claim, a wrong-ring claim both ways, a swapped table, a characteristic control, and non-vacuity
trunc-14candidate2026-08-30
THE LADDER OBSTRUCTION: an explicit 4-dimensional subspace in the one-level substitution family at N = 4 that seven rank-one matrices already span, against R(T₄) = 8 – the substitution route to R_(F₂)(T₅) >= 11 is closed, with a witness instead of a timeout
trunc-15known2026-08-30
R_(F₂)(T₃) = 5 and R_(F₂)(T₄) = 8 exactly, BOTH directions kernel-bound
trunc-16known2026-08-30
Rₛym(T₂) = 3, Rₛym(T₃) = 5, Rₛym(T₄) = 8 exactly
trunc-17known2026-08-30
Rₛym(T₅) = 11 exactly: a machine-checked verification of the published value inside the symmetric subclass, which contains BDEZ's 112 optimal T₅ schemes
trunc-18known2026-08-30
Rₛym(C₃) = 4 and Rₛym(C₅) = 10 exactly
trunc-19known2026-08-30
Rₛym(C₆) = 12 exactly: any rank-11 scheme for the cyclic product of length 6 – the open end of arXiv:2603.07280's cell [11,12] – must be NON-symmetric
trunc-20routine2026-08-30
Engine controls: every search answers true at the true value and false at budget zero, and the truncated and cyclic searches disagree exactly where the two algebras do
trunc-21known2026-08-30
Rₛym(T₆) >= 13, exhausting 67,831,173 candidate subspaces, so Rₛym(T₆) is in 13, 14
trunc-22known2026-08-30
WITHDRAWAL, NOT A THEOREM: the strategy journal's six 'new' symmetric exact values are all printed in BDEZ 2012 Table 4
This ledger entry is reported in prose and is not bound to a Lean theorem.trunc-24candidate2026-08-30
The (★) family swept whole: no member at N = 4 has atom-rank <= 6, so the minimum over all 4096 parameter triples is EXACTLY 7 and one level of the substitution ladder yields exactly R(T₅) >= 10
trunc-23measurement2026-08-30
PRICED FRONTIER, NOT A THEOREM: what this engine cannot reach, measured, and the negative find-direction sweep on the three open cells
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- The truncated (or *short*) product of length N multiplies two polynomials of degree < N and keeps the coefficients of 1, x, …, x^(N-1). Its structure tensor is
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7