We study the gauge-invariant Kogut–Susskind Hamiltonian on a periodic SU(2) ladder with link spins truncated at one half. For every circumference `N ≥ 3` and every coupling `x > 0`, we prove that the ground state is simple and lies in the trivial centre sector, with winding-sector separation at least `N(21x/200 + 37/(125x))`. The thermodynamic centre-flux energy density exists; rational product states, kernel-checked finite-block bounds and rational evaluation of an Ising integral give `σ(1) ∈ [0.58099, 0.66146]`. A local variational argument places the first excitation in the trivial sector for every `N ≥ 21`, uniformly in coupling. Lean-kernel-checked integer certificates enclose the full spectral gaps for `N = 3, …, 8`, establish their nonmonotonicity, and identify a change of first-excitation sector between five and six plaquettes. At three sizes, opposite certified endpoint orderings locate excitation-sector coincidences in disjoint coupling intervals, without asserting uniqueness. A spin-network proof identifies the explicit matrices with the truncated Hamiltonian; the winding block is a transverse-field Ising chain. This bundle contains the manuscript, the 733-module Lean 4 acceptance closure (acceptance command `lake build ChristMath.KSAccept`), the pinned toolchain and Mathlib revision, the generator and check scripts, the dependency and claim tables, and the fresh-process axiom audit. See README.md.
We study the gauge-invariant Kogut–Susskind Hamiltonian on a periodic SU(2) ladder with link spins truncated at one half. For every circumference N ≥ 3 and every coupling x > 0, we prove that the ground state is simple and lies in the trivial centre sector, with winding-sector separation at least N(21x/200 + 37/(125x)). The thermodynamic centre-flux energy density exists; rational product states, kernel-checked finite-block bounds and rational evaluation of an Ising integral give σ(1) ∈ [0.58099, 0.66146]. A local variational argument places the first excitation in the trivial sector for every N ≥ 21, uniformly in coupling. Lean-kernel-checked integer certificates enclose the full spectral gaps for N = 3, …, 8, establish their nonmonotonicity, and identify a change of first-excitation sector between five and six plaquettes. At three sizes, opposite certified endpoint orderings locate excitation-sector coincidences in disjoint coupling intervals, without asserting uniqueness. A spin-network proof identifies the explicit matrices with the truncated Hamiltonian; the winding block is a transverse-field Ising chain. This bundle contains the manuscript, the 733-module Lean 4 acceptance closure (acceptance command lake build ChristMath.KSAccept), the pinned toolchain and Mathlib revision, the generator and check scripts, the dependency and claim tables, and the fresh-process axiom audit. See README.md.
We construct Lean-kernel-checked spectral certificates for rational definite pencils representing the periodic SU(2) Kogut–Susskind ladder with link spins truncated at `j ≤ 1`. The construction uses an unnormalised spin-network basis with a positive diagonal Gram matrix. At unit coupling and circumferences `N = 3, 4`, the certificates enclose both centre-sector ground energies and give strict lower bounds for both sector first-excited energies. They identify a simple charge-0 ground level and a simple charge-1 first-excited level of the full pencil, with full spectral gaps in `[0.865089, 0.865122]` and `[1.183111, 1.183144]`, respectively. The gap therefore increases strictly between these two sizes. Compared with the independently certified `j ≤ ½` gaps at the same sizes and coupling, it decreases strictly at both sizes, while the first excitation remains in the nontrivial centre sector. The `N = 4` sector dimensions are 579 and 434. Their certificates use separately kernel-checked arithmetic segments composed by proved chain lemmas, with measured segment-process memory near 1.6 GiB; the final aggregation has a larger memory requirement. The final theorems use only `propext`, `Classical.choice` and `Quot.sound`. The spectral certificates are kernel-checked statements about the supplied pencils. Their interpretation as statements about the truncated Hamiltonian is established by a hybrid verification: kernel-checked finite identities, paper proofs of the spin-network identification, and independent exact-rational verification of the selection-eligible magnetic contractions, with vanishing elsewhere established by the selection-rule proof and stored-support certificates. The full identification chain is not kernel-checked. No cutoff-convergence or untruncated-gap conclusion is asserted. This bundle contains the manuscript draft, the 57445-module Lean 4 acceptance closure (acceptance command `lake build ChristMath.J1Accept`), the exact pencils and local tables, the emitters, the independent Rust implementation, and the fresh-process axiom audit.
We prove the ground-state energy of the periodic, half-filled 4×4 repulsive Hubbard model with t = 1 to at least 23 decimal places at U = 1, 2, 3, 4, 5, 6, 7, 8, 10, 12 and 16: every enclosure has width below 10⁻²⁴. The double occupancy, the spin correlations and the staggered structure factor have certified interval widths below 10⁻¹⁰, and the kinetic energy below 10⁻⁹. Hypercube, spin and pseudospin symmetries reduce the problem to a 19,186-dimensional block that contains the ground state by Lieb's theorem and a character argument. A binary64 Cholesky factorization, verified using a rigorous rounding-error bound evaluated in exact rational arithmetic, certifies spectral separation within this block; exact Rayleigh quotients and residuals then give Temple enclosures of the energy and bounds on the angle to the ground state, which certify the observables. Separation certificates at both ends and a perturbative trial family enclose E₀(U) for every U in [3.9, 4.1], with uniform width at most 1.6 × 10⁻⁹. Two independent implementations replay the certificates, the interlacing and Temple steps are proved in Lean 4, and all computations run on one laptop. At U = 4 and 8, exact-arithmetic brackets that use neither Lieb's theorem nor floating point are also given, and the enclosures bound their deficits. At U = 4 the certified energy rounds to −13.62185 and excludes the published value −13.62192 [Physical Review B 94, 085103]. Contents of the bundle paper/ — the manuscript (Markdown and PDF), its figures, and supplementary/ with five videos generated from the certificate files. rayleigh/symmetry/ — the enclosure pipeline (block dimensions, exact basis, certificates, observables, the interval certificate) and recheck/, the independent Rust reference checker; certificates/ holds every certificate, trial vector, run log, checker log and the clean-replay report. sos/, rayleigh/demo/, cluster/ — the exact-arithmetic bracket certificates and the expected outputs of their checkers (golden_ files); the bracket checkers belong to the authors' certification software and are not included. formal/ — the Lean 4 statements (rank-one interlacing, Temple's inequality, the sum-of-squares remainder bound). tests/ — the generators of every table, figure and video of the manuscript. replay.sh, REPLAY.md — the automated replay and the step-by-step commands. AUDIT_AXIOMS.txt — #print axioms of the formal statements. SHA256SUMS — checksums of every file. Verification PYTHON=<python with numpy and scipy> ./replay.sh rebuilds the symmetry block from the Hamiltonian, reproduces every certificate from the stored integer vectors, runs the Rust reference checker, recomputes the observables and checks the manuscript's tables, and writes REPLAY_REPORT.md. It needs about 12 GB of memory and 16 GB of free disk, and takes about half an hour on the hardware above; its work directory is removed at the end. REPLAY.md lists the commands step by step; rayleigh/symmetry/certificates/REPLAY_REPORT_2026-10-14.md is a clean replay of this material. Not included: the two 662,547,600-byte full-sector vectors of the upper bracket certificates (their SHA-256 digests are in rayleigh/demo/). Integrity: shasum -a 256 -c SHA256SUMS inside the bundle; the SHA-256 of the tarball is in the .sha256 file beside it. Environment Python: 3.13.7 with numpy 2.5.4, scipy 1.18.1, matplotlib 3.11.2 (producer-requirements.txt) Rust: 1.90.0 (reference checker; cargo build --release in rayleigh/symmetry/recheck) Lean: leanprover/lean4:v4.33.1 with Mathlib v4.33.1 (formal statements) Hardware: Apple M3 Pro, 18 GiB (all production and replay) License: CC BY-NC 4.0. Commercial use requires written permission from Origin Neural AI (labs@smartledger.solutions).
Volume-Uniform Finite-Volume Bounds with the Representation Cutoff Removed: a Reconstruction and Computer-Assisted Improvement of Creation-Operator Constants We study the Kogut–Susskind Hamiltonian of pure SU(2) and SU(3) lattice gauge theory on three-dimensional cubic boxes, H = aΣ_e L_e + bΣ_p (1 - F_p), with L_e the electric Casimir on link e and F_p = N⁻¹Re tr U_p, at strong coupling (small b/a). An unrefereed preprint by Gauvin adapts the creation-operator method of Bravyi, DiVincenzo and Loss to this setting and states, for SU(3), a physical gap uniform in the volume, with the representation cutoff removed, for b/a ≤ 1/648. We give a self-contained reconstruction of the finite-volume argument, identify its external analytic inputs, and reproduce its constants. We then prove a sequence of refinements of the commutator estimate: a selection rule of Wilson-loop multiplication that restricts admissible creation placements, fractional witness counting, orthogonality of output sectors, Haar-measure bounds for vacuum projections before and after the plaquette multiplication, a two-link sandwich identity, a joint vacuum-row bound, and a size-weighted norm. The finite tuple constants and final sufficient inequalities are checked in exact rational arithmetic by two author implementations and a separate verifier written from the stated definitions. The operator inequalities that justify these arithmetic definitions are proved analytically. On open boxes the physical gap is at least 3a/2 for SU(2) whenever b/a ≤ 2/95, and at least 8a/3 for SU(3) whenever b/a ≤ 2/35 (1/16 with a sharper representation-theoretic bound), uniformly in the box. These sufficient couplings are 3072/95 and 1296/35 times those obtained from the preprint's constants (for SU(2), our transfer of them). The corresponding open-box endpoints in Hamiltonian units are β_H=√(4/95) ≈ 0.205 for SU(2) and β_H=√(6/35) ≈ 0.414 for SU(3), or √(3/16) ≈ 0.433 with the strengthened SU(3) bound. The basic open-box certificates also bound the static fundamental potential below linearly: for static charges at graph distance L ≥ 6, E_{x,y} - E_vac ≥ σ L with σ = 5/16 a for SU(2) at b/a ≤ 2/95 and σ = 5/9 a for SU(3) at b/a ≤ 2/35, uniformly in the box. A variable exclusion fraction and an independent local-decoupling upper bound bracket the first physical excitation energy above the vacuum. On open boxes containing an elementary plaquette, at b/a = 1/5000 this energy lies in [2.990, 3.050] a (SU(2)) and [5.326, 5.390] a (SU(3)). These are strong-coupling statements at fixed lattice spacing, not continuum statements. Files ym_strong_coupling_gaps.pdf: the paper. zenodo_ymgap_v1.0.0_2026-10-23.zip: the certificate bundle: two independent implementations of the certified tuple constants, the verifier, the tamper-test driver, the Section 8 upper-bound program and its exact checker, the number generator, manifests and verifier outputs for all 34 certificate configurations, the complete tuple files, and the paper source with every number generated from these files. Its SHA-256 is in the adjacent .sha256 file; SHA256SUMS inside covers every file. README.md, LICENSE.md: copies of the bundle's front matter. Verification ./replay.sh (Python 3, standard library only; a few minutes) regenerates every tuple file, compares it entry by entry with the second implementation, verifies every manifest in exact rational arithmetic, runs the tamper tests and the exact check of the two-sided bracket upper bounds, and regenerates every number of the paper; it exits non-zero on any failure. Scope: strong-coupling statements for the Kogut–Susskind lattice Hamiltonian at fixed lattice spacing, uniform in the volume, with the representation cutoff removed. They are not continuum statements and do not address the continuum Yang–Mills mass gap problem. Licence: CC BY-NC 4.0 (LICENSE.md), licensed by SmartLedger Solutions. Commercial-use enquiries: labs@smartledger.solutions. No patent licence is granted by this release.
Preprint of the article "A fixed-level certification dichotomy for an infinite family of frustration-free spin chains" (22 pages, no figures). To every finite loopless directed graph T the paper attaches a rational, range-three, frustration-free spin-chain interaction: arcs of T carry hopping bands for domain walls, missing arcs act as hard local penalties. The main theorem is the exact three-term equivalence: T is acyclic <=> liminf_m gap_m(T) > 0 <=> delta_LTI(5) > 0, where gap_m is the spectral gap of the periodic chain on m sites and delta_LTI(5) is the value of the local translation-invariant (LTI) semidefinite certification hierarchy at level 5, its first sound level. The certification level is fixed while the size of the graph and the local Hilbert-space dimension are unbounded across the family. To the author's knowledge, this is the first fixed-level completeness result for a spectral-gap certification hierarchy over an infinite family of frustration-free chains: a single finite combinatorial invariant, acyclicity, decides both the thermodynamic spectral gap and the success of the certificate at one universal level. The acyclic direction is proved by an explicit rational certificate, a superpotential built from a topological height and three local corrections, giving delta_LTI(5) >= min{1/48, 1/sqrt(12H)} for a DAG of height H. The cyclic direction is made quantitative by a free-fermion analysis of the invariant winding sectors: directed cycles carry a diffusive lowest mode of energy of order 1/m^2, and the finite-volume gaps of the directed 2- and 3-cycles are computed exactly, 2(1-cos(pi/m)) and 2(1-cos(2pi/m)). The relationship with the PVBS chains of Bachmann and Nachtergaele and with earlier gapped-gapless classifications is discussed explicitly. All computer-assisted statements use exact symbolic arithmetic. The complete reproducibility package (symbolic pipeline, generated blocks with exact characteristic polynomials, Sturm data, LDL^T certificates, SHA-256 digests) is archived separately at https://doi.org/10.5281/zenodo.21790411. The manuscript has been submitted to Reports on Mathematical Physics.
We study Kogut--Susskind SU(2) lattice gauge theory on collapsed two-leg plaquette chains in a spin-network (electric) basis with canonical intertwiners fixed in closed form: the Wigner 3j tensor with an ε metric on each head slot, certified by vertex Casimir annihilation. Magnetic plaquette matrix elements factorize in magnitude into per-vertex Racah 6j factors (verified to 1.2×10−15 through electric truncation jmax=2), while their \emph{signs} obey a refined local class law. We report three results. (1) An exact \emph{factored transfer contraction} evaluates any matrix element in O(106) flops independent of link labels, giving measured Hamiltonians at any moderate length with no sign table; it reproduces independent DMRG bulk energies to 9×10−16. (2) A non-gauge \emph{underdetermination phenomenon}: the complete set of length-≤3 amplitudes leaves a GF(2) sign freedom that is not pure gauge --- two tables, each exact on all measured length-≤3 data, differ at length ≥4 by O(0.5) in ground energy. (3) A \emph{pinning result}: adjoining the (cheap) complete length-4 batteries collapses the freedom to true gauge; the pinned table reproduces independent length-5 and length-6 ground truth to 10−14--10−13. %% ANCHOR: ABSTRACT-R3L5 (one sentence on rung-3 L=5 certification) %% ANCHOR: ABSTRACT-R3L5-END Corrected physics follows: the flux gap rises monotonically in λ=4/g4 at every electric truncation, each rung softening the slope, with geometric rung convergence of both gap and bulk energy density. %% ANCHOR: ABSTRACT-EXTRAP (final extrapolation sentence) %% ANCHOR: ABSTRACT-EXTRAP-END All code, data, and machine-verifiable certificates accompany this deposit. The bundle contains the SHA-256 manifest of all 115 files, the seven stage deliverables, source code, and the datasets
We give a computer-assisted proof that the first twelve excitations of the neutral SU(3) lattice gauge Hamiltonian on a single cube form two isolated six-dimensional spectral subspaces. Their representations under spatial symmetry and charge conjugation are A+ ⊕ E+ ⊕ T + and A− ⊕ E− ⊕ T − . Complete electric- 1g g 1u 1u u 1g energy windows, rational Ritz bounds, and full Wilson-output Gram matrices yield certified eigenvalue counts for the untruncated operator. The main theorems use interior thresholds with larger comparison-form margins and give separations of at least 0.78482728 between the clusters and 0.72784037 above the second cluster. A separate refinement improves these values to 0.89782728 and 0.85184037. The neutral gap lies in [4.415605103, 4.978456040]. All multiplicities are retained, and selected matrix entries are audited with an independent Haar-integration algorithm. No ordering of the irreducible components within either cluster, volume-uniform gap, or continuum limit is asserted.