Certificates for the tensor rank of split-octonion multiplication

This repository contains the computational part of the proofs in the paper The tensor rank of split-octonion multiplication (H. Lemley, 2026). The repository contains commented Python using the standard library only, plus a SAT solver and an LRAT proof checker for one step. Every computational claim below can be re-checked with one command.

Let T be the multiplication tensor of the split octonions in Zorn's vector-matrix basis (code/verification/octonions.py). Its 32 nonzero structure constants are ±1, so T is defined over ℤ.

Result	Statement	Check	Estimated Time (one core unless noted)
F₂	R(T) = 19 over F₂	code/verification/check_upper.py, code/verification/check_f2_restriction.py, code/sat/check_f2_capacity.py	1 s, 1 min, about 5.5 CPU-hours (15 min on 24 cores)
Characteristic 2	18 ≤ R(T) ≤ 19 over every field of characteristic 2	code/verification/check_upper.py, code/verification/check_universal.py	1 s
F₃	18 ≤ R(T) ≤ 21 over F₃	code/verification/check_upper.py, code/verification/check_f3.py	1 s, 3 min
Every field	18 ≤ R(T) ≤ 21 over every field	code/verification/check_upper.py, code/verification/check_universal.py	1 s
C and Q(i)	18 ≤ R(T) ≤ 20; an explicit 20-term identity	code/verification/check_complex_upper.py, code/verification/check_universal.py	1 s
Fields containing i	R(T) ≤ 20 if char ≠ 2, i² = −1 and the field has more than five elements; in particular F_q with q ≡ 1 (mod 4), q > 5	code/verification/check_complex_upper.py	1 s

The last identity is a rational parameter family with u outside {0, ±1, ±i}. F₅ has no admissible parameter; the bounds there remain 18–21. A 20-term identity establishes an upper bound over C and fields containing i.

Repository layout

• code/verification/: certificate checkers and shared exact algebra.
• code/sat/: F₂ capacity encoding, symmetry splitting, and pinned SAT/LRAT tooling.
• code/tools/: certificate tamper tests.
• data/: the original certificate inputs.
• lean/: the Lean project, with 19 analytic reductions and Lean estimates.
• docs/proofs/: the written research proof and its dependencies.

Lean formalizations of the decomposition upper bounds, the parameter family, and foundational reductions are present in the lean/ directory, together with an explanation of their semantic correspondence; the complete lower-bound formalizations remain unfinished. The research semantic report identifies the exact checked scope and remaining geometric obligations.

See code/README.md for the implementation layout.

Running

./code/verify_all.sh --quick      # everything except the SAT leaves (a few minutes)
./code/verify_all.sh              # everything (17 minutes on 24 cores); builds CaDiCaL and lrat-check on first use
WORKERS=16 ./code/verify_all.sh   # parallelism of the F₂ capacity step (default: all CPUs)

Requirements: Python ≥ 3.10. For code/sat/check_f2_capacity.py also git, a C/C++ compiler, make, a POSIX system (named pipes), and about 3 GB of RAM per worker. Each leaf writes a 70 MB CNF to the temporary directory (--work, default $TMPDIR), which should preferably be a RAM file system. code/sat/build_solvers.sh fetches and builds the two external programs at pinned commits.

What each script checks

• code/verification/check_upper.py: a 19-term decomposition over F₂ (data/D19_F2.json) and a 21-term decomposition over Z[1/2] (data/D21_Zhalf.json, exact over Q, denominators 1, 2, 4) reproduce all 512 entries of T.
• code/verification/check_f2_restriction.py: the restriction-bound certificate over F₂ (data/F2_restriction_bounds.*, 32 orbit representatives). It builds the orbits of all 417,199 subspaces of first-input functionals under 16 verified autotopy generators, then re-checks every proof (flattening, forced product, degenerate reduction, substitution with backtracking) using its own orbit table only. Gives R ≥ 18.
• code/sat/check_f2_capacity.py: builds the capacity CNF from those bounds and proves it unsatisfiable by a symmetry-reduced case split; each leaf is solved by CaDiCaL and its LRAT proof is streamed through a pipe into lrat-check. Proofs are never stored on disk because they become enormous quickly. This gives R ≥ 19. The split is adaptive (a leaf that exceeds --timeout is split further); data/F2_case_tree_hint.json lists the nodes known to need splitting and only saves time. Soundness does not depend on the shape of the tree.
• code/verification/check_f3.py: replays the F₃ capacity certificate (data/F3_capacity_proof.tar.gz, 1.8 MB: the 27 table entries, 1,574 search traces and 2,191 orbit-transport witnesses used by the proof; 3,393 job files including trace metadata, symmetry contexts, and split files).
• code/verification/check_universal.py: the integral composition, polarization, adjoint and quaternion identities, plus all 1,024 signed-Gram patterns and 100 minor identities used in the written all-field lower-bound proof. The geometric and dimension deductions are proved in the paper.
• code/verification/check_complex_upper.py: all 512 entries of data/D20_Qi.json over Q(i), the exact symbolic family data/D20_Qi_family.json, and finite-field specializations including F₉ and F₂₅. All cleared polynomials vanish exactly; their coefficient ring is Z[1/2][i].
• code/verification/check_general.py: the finite identities used in the earlier field-independent lower bound 16 (Koszul-flattening minors with determinants 96, 144, 81, 6561; kernel vectors; wedge maps).
• code/tools/research_tamper_tests.py (not part of the proof): rejects corrupted Gaussian coefficients, family coefficients, characteristic-dependent denominators and signed-Gram witnesses.
• code/tools/tamper_tests.py (not part of the proof): corrupts each certificate in a small way and confirms that the corresponding checker rejects it.

Trust base

To trust the results you need to trust: the Python interpreter; the scripts under code/ (code/verification/octonions.py, code/verification/linalg.py, code/verification/check_*.py, code/sat/check_f2_capacity.py); and lrat-check from drat-trim (509 lines of C). CaDiCaL does not need to be trusted, as they are verified by lrat-check after generation. The mathematical arguments that turn these checks into the theorems are proved in the paper. Each script's docstring says which statement it checks.

The certificates were produced by other programs that are not needed here. The restriction bounds over F₂ by an F₂ port of X. Wang's tensor-rank-lower-bound toolkit, the F₃ certificate by a capacity-search program (its own verifier agrees with code/verification/check_f3.py), the decompositions by flip-graph and SAT searches and, for D21, by 3-adic Hensel lifting of an F₃ decomposition. The rank-20 family is obtained from complex searches and an order-four symmetry reduction, followed by exact reconstruction and symbolic verification.

Data files (sha256)

bc5911afa4b35c59c62e456562af37b3ee5f231f900551a44a63125593d68cbc  data/D19_F2.json
4e9a71551519f40c67e2c56b5c1c2fff1806ba3d6726ce0e1c7150ee6f15368d  data/D21_Zhalf.json
b73d6b17f0d04dbefe2582c3b934194f50d3fcfa219068442b7f2b44921f6d47  data/F2_restriction_bounds.pb.txt
7a38eb748052e086c97844007e9245cb88c21fea06dd93900985b09a3316b9c6  data/F2_restriction_bounds.btp
3c28091e42004656f7026618608193446d107fa70ae004a2e04ba1d4a84017d6  data/F3_capacity_proof.tar.gz
597d81bc28613d97909581af7ce17e1445151ec08c555c9f28d92536358a10ff  data/general_koszul_minors.json
e1ae9ad98a0684d7135fdbc41d84958e6a13012c24adc362276b349831eef56a  data/general_rank4_kernel.json
f1b9d6951ac5b076bd32c9f441de1ccf93544590c51e7eb0c3b2d2317169b270  data/D20_Qi.json
6879556d57ae0afeb3ceae2562adc4f5c69c8525ea192123d9eb15ac6d6a3d6b  data/D20_Qi_family.json
44a7daa1bd6660dff0e1f29fbdc7c2c5a2268e98c231e926e71814160331db2d  data/quaternion_rank14_upper.json
0d7d2b3bd3eca5ee8bd2545034e021995f3fffaa2d72e47dc151a725c59f835b  data/universal_gram_certificate.json

License

All code is released under the MIT License and is presented with no warranty or guarantees. You may use it in any way for any purpose and are not restricted by the original author of the code.