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 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 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.
The best known lower bound for the minimum Kochen-Specker vector system in R3 -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
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.
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 prove uniform QMA membership for the spectral-infimum decision problem for the full spinful antisymmetric Coulomb Hamiltonian with unit nuclei, distinct rational nuclear positions, unary electron number and inverse-polynomial promise gap. Nuclear repulsion is omitted. Positions and thresholds use binary rational encoding; the result assumes neither binding nor a spectral gap, geometric separation, bounded physical diameter, a selected finite basis, a fixed spin sector or an efficiently prepared low-energy state. The proof combines quantitative localization including escaped electrons, Hardy-controlled Coulomb caps, a finite kinetic cutoff, exact shifted sampling with L2 error control, and a polynomial-size verifier on arbitrary witness states. Together with the hardness theorem of the pinned source manuscript, this gives QMA completeness for the same problem. Classical sector localization, finite-basis electronic complexity, smooth-box discretization and earlier real-space simulation estimates are credited. The accompanying Lean support proves selected finite sampling, representation-average and scalar error interfaces; it does not formalize the full continuum or quantum-complexity theorem. No extension to exponentially large binary nuclear charges or worldwide priority claim is made. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review or worldwide-priority certification. Identified OpenAI source inputs at revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb are stipulated true. Lean verifies scoped supporting results only, not the full theorem. Original prose: CC BY 4.0; original code and Lean: MIT; third-party rights preserved. See the supporting archive for precise assumptions, coverage, provenance and corrections.