Twenty-Three Certified Decimals: Rigorous Ground-State Energies, Correlations and a Coupling Curve for the Half-Filled 4×4 Hubbard Model: certificate bundle v1.0.0
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).
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).
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 explicitly carry through to the Hubbard endpoint the product-state (Hartree-Fock-type) case that Waite et al. state is available within their framework. The closest route is their Theorem 7 with a subset of cardinality one. We give explicit constants, track each guiding spinor through the reduction, and provide a finite description of the resulting site-local Slater determinant. The target is a repulsive Fermi-Hubbard Hamiltonian on a full open rectangular square grid, with spatially uniform positive hopping and repulsion, local vector fields, and the entire fixed-number sector Nf = M. With inverse-polynomial squared overlap and normalized decision precision, the resulting promise problem is PromiseBQP-complete; hardness holds on the subclass with a unique sector ground state and an inverse-polynomial spectral gap. The guiding spinors are retained from their creation-time penalty ground states and rounded to normalized dyadic-pair descriptions. The proof includes explicit global perturbation bounds and preparation and energy-estimation costs. MSC2020: Primary 68Q12; Secondary 81P68, 81V70. The archive contains the complete LaTeX source, vector figures, numerical test data, build instructions, a manifest, and SHA-256 digests. AI-use disclosure: The natural-language proofs, diagnostic code, partial formal proofs, and manuscript were generated using GPT-6 Astra and Claude Fable 5.1 under the author's direction on the research question and acceptance criteria. AI review comprised four independent audits and one heterogeneous adversarial audit across the two model families; completed human mathematical proof reviews number zero. Formal checking is peripheral: five source-side and five finite-endpoint declarations have Lean kernel proofs, Schrieffer-Wolff composition is zero of eight original targets, and one overgeneral transfer signature has a singleton counterexample. The full uniform completeness theorem is not formally proved. The author supplied the presentation revisions and remains responsible for final acceptance of the work. Appendix C distinguishes the earlier high-precision numerical example from the new certified Arb interval calculation.
Implementing an improved method for analytic continuation and working with imaginary-time correlation functions computed using quantum Monte Carlo simulations, we resolve the single-particle dispersion relation and the density of states (DOS) of the two-dimensional Hubbard model at half filling. At intermediate interactions of U/t=4,6, we find quadratic dispersion around the gap minimum at wave vectors $\mathbf{k}=(\ifmmode\pm\else\textpm\fi{}\ensuremath{\pi}/2,\ifmmode\pm\else\textpm\fi{}\ensuremath{\pi}/2)$ (the $\mathrm{\ensuremath{\Sigma}}$ points). We find saddle points at $\mathbf{k}=(\ifmmode\pm\else\textpm\fi{}\ensuremath{\pi},0),(0,\ifmmode\pm\else\textpm\fi{}\ensuremath{\pi})$ (the X points), where the dispersion is approximately quartic, leading to a sharp DOS maximum above the almost flat ledge arising from the states close to $\mathrm{\ensuremath{\Sigma}}$. The fraction of quasiparticle states within the ledge is ${n}_{\mathrm{ledge}}\ensuremath{\approx}0.15$. Upon doping away from half filling, within the rigid-band approximation, these results support Fermi pockets around the $\mathrm{\ensuremath{\Sigma}}$ points, with states around the X points becoming filled only at doping fractions $x\ensuremath{\ge}{n}_{\mathrm{ledge}}$. The high density of states away from the $\mathrm{\ensuremath{\Sigma}}$ gap edge may be an important clue for a finite minimum doping level for superconductivity and other instabilities of doped Mott insulators.
We construct three new weight-6 bivariate-bicycle (BB) codes—two [[336,20,12]] codes, inequivalent under the BB presentation symmetries, over Z₂ × Z₈₄ and a [[360,24,12]] code over Z₆ × Z₃₀—and certify exact distance 12 in both the X and Z sectors. They encode 25% and 50% more logical qubits than the best distance-12, weight-6 code reported by IBM's evolutionary search (k = 16) [Cruz-Benito et al., arXiv:2606.02418]. They are also the only ones: a symmetry-reduced enumeration of every connected weight-6 BB code with three-term polynomials, n ≤ 360 and k ≥ 20 eliminates 1,448 of the 1,584 candidates with checked logical operators of weight at most 11, and the remaining 136 presentations fall into three classes under group automorphisms, renormalisation and A ↔ B, represented by the new codes; within the polynomial ansatz of [Bravyi et al., Nature 627, 778 (2024)], every one of the 432 such candidates has distance at most 10. The same certificates settle the distances of the IBM ladder [Bravyi et al., Nature 627, 778 (2024)]—[[72,12,6]], [[90,8,10]], [[108,8,10]], the gross code [[144,12,12]] and the two-gross code [[288,12,18]], both sectors—and certify 19 ≤ d ≤ 24 for [[360,12]], whose distance we establish to be exactly 24 by exhaustive enumeration, resolving the upper bound reported in [Bravyi et al., Nature 627, 778 (2024)]. For the depth-8 syndrome-extraction circuit they certify circuit-level distance exactly 6 for [[72,12,6]] in both memory bases and at least 6 for every other code tested. Certified lower bounds are DRAT refutations for n ≤ 144 and replayable search trees above, whose single pruning lemma is proved in Lean 4; a reader replays any certificate with a standard-library Python verifier plus drat-trim or a 200-line C replayer, without the software that produced it. In a 1.1-million-shot circuit-level benchmark under one frozen BP-OSD decoder, the new codes' block failure probabilities at p = 0.004 are 3.6–6.2 times lower than the gross code's and 3.4–5.6 times higher than the two-gross code's, in both memory bases. Every computation—search, certification, replay and benchmark—ran on one laptop (Apple M3 Pro, 18 GB) with no GPU and no cluster. Contents of the release paper/ — the manuscript (LaTeX source, bibliography and PDF). certificates/ — one manifest per code and sector (<code_id>_<sector>.json), its standard-library Python verifier (verify_qec_<code_id>_<sector>.py), the proofs in proofs/ (DRAT proofs and gzipped proof trees), the problem files and C source of the tree replayer, the Lean 4 minimality lemma (qec_minimality.lean), the weight-6 envelope witnesses with their checkers, the distance table, FORMAT.md (the certificate format) and REPLAY.md (a clean replay of every certificate: 44 of 44 pass). simulation/ — the projected detector error models, the BP-OSD and BP-LSD evaluation scripts, every 2,000-shot chunk record with its seed, the decoder-tuning grid and the joint-model controls. SHA256SUMS — the SHA-256 of every file. Verification In certificates/: python3 verify_qec_<code_id>_<sector>.py rebuilds the code from its polynomials, checks the logical basis by rank, regenerates every CNF or problem file byte for byte and replays the proof; its last line is the verdict. DRAT rows need drat-trim (set DRAT_TRIM); tree rows need a C compiler. The Lean lemma checks with lake env lean qec_minimality.lean in a project with the pinned Lean 4 v4.33.1 and Mathlib 0df444a3 (exit status 0). Integrity: shasum -a 256 -c SHA256SUMS. Hardware Every computation — search, certificate production, replay and the benchmark — ran on one MacBook Pro (Apple M3 Pro, 11 CPU cores, 18 GB memory, macOS 15.5), with no GPU and no cluster. License: Licensed by SmartLedger Solutions under CC BY-NC 4.0 (LICENSE.md). Commercial use requires a written license from SmartLedger Solutions (labs@smartledger.solutions). The certificate producer is proprietary and not distributed; verification does not need it.
The ground-state energy of the Hubbard model on a Bethe lattice with infinite connectivity at half filling is calculated for the insulating phase. Using Kohn's transformation to derive an effective Hamiltonian for the strong-coupling limit, the resulting class of diagrams is determined. We develop an algorithm for an algebraic evaluation of the contributions of high-order terms and check it by applying it to the Falicov-Kimball model that is exactly solvable. For the Hubbard model, the ground-state energy is exactly calculated up to order t12/U11. The results of the strong-coupling expansion deviate from numerical calculations as quantum Monte Carlo (or density-matrix renormalization group) by less than 0.13 (0.32 respectively) for U>4.76.
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.