Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Finite Certificates for All-Temperature Monotonicity of Pairing-Source Curvature

Piyush Sao

Published Sep 16, 2026• 0 citations
Publisher

Abstract

Proving a quantum-response inequality at every temperature requires control beyond a finite temperature grid or a truncated series. We give a sufficient finite certificate for strict growth of the pairing-source curvature 𝜅2(𝛽)=𝜕2ℎ log Tr 𝑒−𝛽(𝐻−ℎ𝑀)|ℎ=0, which equals 𝛽 times the physical source susceptibility. For finite Hermitian systems with source reversal, a positive spectral shift produces nonnegative two-insertion temperature coefficients. Ordering their ratios to the partition coefficients implies 𝜅′2(𝛽)> 0 for every 𝛽 > 0. A simple ground state coupled to the source forces these ratios toward a line with positive slope; an explicit spectral error bound proves every increment beyond a computable cutoff. The complete certificate therefore requires a finite coefficient prefix and finitely many spectral bounds. For the half-filled uniform-attraction Hubbard dimer, two ordered temperature-series quotients and the atomic formula prove curvature growth over all couplings, with connected- cluster consequences near gapped dimer products. For a connected four-site attractive chain, integer and rational arithmetic verifies 3199 increments and closes the infinite tail. A uniform perturbation bound also gives an explicit rectangle in hopping and attraction parameters. A self-contained finite-field certificate shows that the same chain’s unscaled polarization can decrease while i

DOI
10.5281/zenodo.22801772

Related papers

Lee–Yang Structure Does Not Imply Thermal Monotonicity

Piyush Sao

Imaginary pairing-source zeros at every temperature do not force the scaled polarization β⟨M⟩ to increase as the inverse temperature β increases. We prove this with a fermionic atom coupled to a neutral auxiliary degree of freedom. Its zero-field ground state is simple, and all its source zeros are imaginary for every β > 0. At fixed field h = 1/100, exact rational inequalities certify Dβ(h) := ∂β[β⟨M⟩] < −9/1000 throughout |β − 20 log 2| ≤ 1/100. These properties persist in a neighborhood within the same parameter family. On this interval, the scaled polarization within the even-parity sector increases. Cooling nevertheless shifts enough probability to the odd sector, on which the pair operator vanishes, to make the total decrease. The sector derivative identity separates this probability shift from the change within each sector. The same sector analysis gives the exact boundary J ≤ 4U/3 for growth of the zero-field curvature at every temperature in a two-site onsite-attraction and exchange family. Further examples distinguish this curvature from inverse-zero moments and from the unscaled polarization, which can decrease while the scaled polarization increases. For auxiliary-field parity comparisons, we identify the corresponding configuration and redistribution terms and show why a proof must control their sum.

•Sep 23, 2026•0 citations

A Pairing-Source Lee–Yang Theorem for Attractive Hubbard Systems

Piyush Sao

We prove a Lee–Yang theorem for onsite pairing sources in finite attractive Hubbard systems. For spin-conserving hopping with an arbitrary Hermitian up-spin matrix and its complex conjugate for down spin, real onsite chemical potentials, and nonnegative onsite attractions, the partition function is nonzero whenever the real parts of all local pairing fields have the same strict sign. In particular, its zeros in a uniform pairing field lie on the imaginary axis at every positive inverse temperature. This time-reversal-invariant class includes real spin-independent hopping and opposite orbital fluxes for the two spins. The proof has two steps. After a particle–hole transformation, the free Fock-space trace becomes a determinant. An indefinite-form argument shows that this determinant is nonzero throughout the source domain. We then represent the onsite attraction as a local operation on a quadratic source polynomial and prove that this operation preserves the same zero-free domain. The highest coefficient remains nonzero, so we can iterate the operation and take a locally uniform Trotter product limit to obtain the interacting theorem. For a nonzero uniform real pairing field, the same transfer argument gives a zero-free spin-fugacity annulus, positivity of the parity-twisted trace, and a lower bound on the induced parity gap. The uniform-source zero theorem also yields bounds on pair response and on the first zero. Finally, for uniformly local sequences at fixed temperature, we relate the first zero to uniform equal-time pair order.

•Sep 15, 2026•0 citations

A Lee–Yang Circle Theorem for Equal-Time Fermionic Pairing Measurements

Piyush Sao

We locate the complex zeros of an equal-time pairing measurement in a finite fermion system. Let P_i = c_{i↓}c_{i↑} annihilate an on-site pair and let M = Σ_i (P_i + P_i†) be its uniform pairing quadrature. For complex-conjugate hopping matrices in the two spin sectors, nonnegative onsite attraction, and nonnegative couplings between these quadratures, the polynomial z^n ⟨e^{(log z)M}⟩_β has all 2n zeros on |z| = 1 at every finite inverse temperature β > 0. We reach the measurement generating function by concentrating a time-dependent source into a shrinking imaginary-time interval with fixed integrated strength. If e^{±iθ₁} are the zeros nearest z = 1, then π²/(4θ₁²) ≤ ⟨M²⟩β ≤ 9n/(2√7 θ₁). For charge-conserving Gibbs states and P = Σ_i P_i, these bounds make lim inf_n ⟨P†P⟩{β_n}/n² > 0 equivalent to lim sup_n nθ₁^(n) < ∞. The criterion allows arbitrary finite positive β_n and unrestricted hopping geometry. Convergence of the scaled log generating functions on any positive-real set with an interior accumulation point determines a unique limiting angle measure and its origin density. Independent growing ordered blocks show why positive origin density and whole-system macroscopic fluctuations have different content. The folded zero product also gives positive inverse-root sums and finite cumulant recurrences. An exact free four-site calculation and an interacting rational certificate separate directional cumulant signs from individual-component signs. The pulse implication also yields a finite-temperature Ising application.

•Sep 21, 2026•0 citations

Width-uniform transfer-matrix gap certificates for the half-spin factor of a lattice gauge toy row: audited computer-assisted bounds at strong coupling and beyond the strong-coupling wall, with structural notes on Weil positivity

Ursachi Andrei

We study an explicit 2^w × 2^w transfer matrix Γ_w(β), the half-spin factor (all link spins ≤ 1/2) of the complete SU(2) transfer operator of an auxiliary open row of w plaquettes, and ask for a spectral gap that is uniform in the width w. (i) At β = 28/25 a Kotecký–Preiss polymer-current certificate gives |λ_k| ≤ e^{−2.90} λ_0 for all k ≥ 1 and all w ≥ 1 (computer-assisted, blind-audited). (ii) The bare current method stops at β ≈ 1.5 although the numerical gap stays between 3.4 and 4.5. (iii) After an exact “dressed” decomposition of Γ_w into connected interval operators, the connected parts obey an all-length geometric bound ‖K̂_L‖ ≤ (2009/50000)(381/2000)^{L−1} at β = 5/2 (exact rational certificate, not audited), with a closed-form decay rate. (iv) Beyond this wall, a time-ordered transfer certificate for the dressed gas with open time boundaries gives |λ_k| ≤ e^{−3.37} λ_0 for every w at β = 5/2, that is 98.8% of the numerical gap 3.4095, and |λ_k| ≤ e^{−5.38} λ_0 at β = 28/25 (computer-assisted, blind-audited except for its inputs from the tail certificate in (iii); one proof gap was found and repaired at no numerical cost). A second route (m ≥ 3.25) is still under audit. All certificates concern the half-spin factor only: with all spins the gap at β = 5/2 is 3.358, 3.312, 3.291 for w = 2, 3, 4, below 3.37 (5.433, 5.428, 5.426 at 28/25; certified by Astra at w = 2 and by our own, not yet audited, engine at w = 3, 4). These ratios follow a nearest-neighbour band law; a single triplet channel carries most of the higher-spin gain and, at β = 5/2, defeats a route-C certificate for the complete row. (v) We record exact structural facts: the both-open stretch of the row is a singlet/triplet mixer with a neutral singlet channel, and positivity of Γ_w forces λ_s ≥ 4p_2² − 3p_3, with physical margin Var(χ_{1/2}) ∼ 6/β². A final part collects observations on Weil positivity for the Riemann zeta function: in the theta-dressed jump formulation the dressed hop rate equals the critical constant 1/2 up to an explicit correction localised where the kernel Φ is not negligible (an exact consequence of W ∗ Φ = 0), so null-function dressings are critical and admit no dilute regime. This indicates why a current-type method does not transfer directly. The Sonin compression of Connes–Consani, the natural candidate ground state with a margin, stops bounding the Weil form on our test banks once the prime 2 enters. We also report finite-size comparator and lane data, experiments on the arithmetic side, and a dictionary between the two problems with explicit open target inequalities. Nothing here is a statement about continuum Yang–Mills theory or a proof of the Riemann hypothesis. Author: Andrei Ursachi (A. Ursachi; Ursachi, Andrei), independent researcher, ORCID 0009-0002-6114-5011. Version 2 (31 October 2026). Supersedes version 1; corrects an error in Definition 1 and extends the results.

•Oct 31, 2026•0 citations

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

Bryan W. Daugherty, Shawn Ryan, Gregory Ward

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).

•Oct 14, 2026•1 citation

A finite-width certificate for the entropy of the six-state square-lattice Potts antiferromagnet

Weiqi Jiang

We report an arithmetically certified enclosure of the zero-temperature entropy per site of the six-state square-lattice Potts antiferromagnet: ln W(6) lies in [1.435107300597, 1.435107684912]. Both endpoints follow from established free-strip ratio and even-cylinder inequalities evaluated with colour and spatial symmetry quotients. Complete integer matrices and positive integer vectors support the spectral certificates. All 4,790,948 entries of eight archived quotient matrices have been independently reconstructed from the colouring compatibility rule. Four matched width budgets separate finite-root certification uncertainty from the remaining thermodynamic gap. At the largest budget the finite-root contribution is below 1.168 x 10^-13, compared with an interval width of 3.84315 x 10^-7. The record contains the eight-page preprint, LaTeX source, complete computational materials and checksums. We acknowledge Gewu Intelligence Lab for providing the collaborative research environment in which this project was developed. W.J. acknowledges support from the Strategic Priority Research Program of the Chinese Academy of Sciences under Grant No. XDB1680102.

•Oct 29, 2026•0 citations
Proving a quantum-response inequality at every temperature requires control beyond a finite temperature grid or a truncated series. We give a sufficient finite certificate for strict growth of the pairing-source curvature 𝜅2(𝛽)=𝜕2ℎ log Tr 𝑒−𝛽(𝐻−ℎ𝑀)|ℎ=0, which equals 𝛽 times the physical source susceptibility. For finite Hermitian systems with source reversal, a positive spectral shift produces nonnegative two-insertion temperature coefficients. Ordering their ratios to the partition coefficients implies 𝜅′2(𝛽)> 0 for every 𝛽 > 0. A simple ground state coupled to the source forces these ratios toward a line with positive slope; an explicit spectral error bound proves every increment beyond a computable cutoff. The complete certificate therefore requires a finite coefficient prefix and finitely many spectral bounds. For the half-filled uniform-attraction Hubbard dimer, two ordered temperature-series quotients and the atomic formula prove curvature growth over all couplings, with connected- cluster consequences near gapped dimer products. For a connected four-site attractive chain, integer and rational arithmetic verifies 3199 increments and closes the infinite tail. A uniform perturbation bound also gives an explicit rectangle in hopping and attraction parameters. A self-contained finite-field certificate shows that the same chain’s unscaled polarization can decrease while i
Imaginary pairing-source zeros at every temperature do not force the scaled polarization β⟨M⟩ to increase as the inverse temperature β increases. We prove this with a fermionic atom coupled to a neutral auxiliary degree of freedom. Its zero-field ground state is simple, and all its source zeros are imaginary for every β > 0. At fixed field h = 1/100, exact rational inequalities certify Dβ(h) := ∂β[β⟨M⟩] < −9/1000 throughout |β − 20 log 2| ≤ 1/100. These properties persist in a neighborhood within the same parameter family. On this interval, the scaled polarization within the even-parity sector increases. Cooling nevertheless shifts enough probability to the odd sector, on which the pair operator vanishes, to make the total decrease. The sector derivative identity separates this probability shift from the change within each sector. The same sector analysis gives the exact boundary J ≤ 4U/3 for growth of the zero-field curvature at every temperature in a two-site onsite-attraction and exchange family. Further examples distinguish this curvature from inverse-zero moments and from the unscaled polarization, which can decrease while the scaled polarization increases. For auxiliary-field parity comparisons, we identify the corresponding configuration and redistribution terms and show why a proof must control their sum.
We prove a Lee–Yang theorem for onsite pairing sources in finite attractive Hubbard systems. For spin-conserving hopping with an arbitrary Hermitian up-spin matrix and its complex conjugate for down spin, real onsite chemical potentials, and nonnegative onsite attractions, the partition function is nonzero whenever the real parts of all local pairing fields have the same strict sign. In particular, its zeros in a uniform pairing field lie on the imaginary axis at every positive inverse temperature. This time-reversal-invariant class includes real spin-independent hopping and opposite orbital fluxes for the two spins. The proof has two steps. After a particle–hole transformation, the free Fock-space trace becomes a determinant. An indefinite-form argument shows that this determinant is nonzero throughout the source domain. We then represent the onsite attraction as a local operation on a quadratic source polynomial and prove that this operation preserves the same zero-free domain. The highest coefficient remains nonzero, so we can iterate the operation and take a locally uniform Trotter product limit to obtain the interacting theorem. For a nonzero uniform real pairing field, the same transfer argument gives a zero-free spin-fugacity annulus, positivity of the parity-twisted trace, and a lower bound on the induced parity gap. The uniform-source zero theorem also yields bounds on pair response and on the first zero. Finally, for uniformly local sequences at fixed temperature, we relate the first zero to uniform equal-time pair order.
We locate the complex zeros of an equal-time pairing measurement in a finite fermion system. Let P_i = c_{i↓}c_{i↑} annihilate an on-site pair and let M = Σ_i (P_i + P_i†) be its uniform pairing quadrature. For complex-conjugate hopping matrices in the two spin sectors, nonnegative onsite attraction, and nonnegative couplings between these quadratures, the polynomial z^n ⟨e^{(log z)M}⟩_β has all 2n zeros on |z| = 1 at every finite inverse temperature β > 0. We reach the measurement generating function by concentrating a time-dependent source into a shrinking imaginary-time interval with fixed integrated strength. If e^{±iθ₁} are the zeros nearest z = 1, then π²/(4θ₁²) ≤ ⟨M²⟩β ≤ 9n/(2√7 θ₁). For charge-conserving Gibbs states and P = Σ_i P_i, these bounds make lim inf_n ⟨P†P⟩{β_n}/n² > 0 equivalent to lim sup_n nθ₁^(n) < ∞. The criterion allows arbitrary finite positive β_n and unrestricted hopping geometry. Convergence of the scaled log generating functions on any positive-real set with an interior accumulation point determines a unique limiting angle measure and its origin density. Independent growing ordered blocks show why positive origin density and whole-system macroscopic fluctuations have different content. The folded zero product also gives positive inverse-root sums and finite cumulant recurrences. An exact free four-site calculation and an interacting rational certificate separate directional cumulant signs from individual-component signs. The pulse implication also yields a finite-temperature Ising application.
We study an explicit 2^w × 2^w transfer matrix Γ_w(β), the half-spin factor (all link spins ≤ 1/2) of the complete SU(2) transfer operator of an auxiliary open row of w plaquettes, and ask for a spectral gap that is uniform in the width w. (i) At β = 28/25 a Kotecký–Preiss polymer-current certificate gives |λ_k| ≤ e^{−2.90} λ_0 for all k ≥ 1 and all w ≥ 1 (computer-assisted, blind-audited). (ii) The bare current method stops at β ≈ 1.5 although the numerical gap stays between 3.4 and 4.5. (iii) After an exact “dressed” decomposition of Γ_w into connected interval operators, the connected parts obey an all-length geometric bound ‖K̂_L‖ ≤ (2009/50000)(381/2000)^{L−1} at β = 5/2 (exact rational certificate, not audited), with a closed-form decay rate. (iv) Beyond this wall, a time-ordered transfer certificate for the dressed gas with open time boundaries gives |λ_k| ≤ e^{−3.37} λ_0 for every w at β = 5/2, that is 98.8% of the numerical gap 3.4095, and |λ_k| ≤ e^{−5.38} λ_0 at β = 28/25 (computer-assisted, blind-audited except for its inputs from the tail certificate in (iii); one proof gap was found and repaired at no numerical cost). A second route (m ≥ 3.25) is still under audit. All certificates concern the half-spin factor only: with all spins the gap at β = 5/2 is 3.358, 3.312, 3.291 for w = 2, 3, 4, below 3.37 (5.433, 5.428, 5.426 at 28/25; certified by Astra at w = 2 and by our own, not yet audited, engine at w = 3, 4). These ratios follow a nearest-neighbour band law; a single triplet channel carries most of the higher-spin gain and, at β = 5/2, defeats a route-C certificate for the complete row. (v) We record exact structural facts: the both-open stretch of the row is a singlet/triplet mixer with a neutral singlet channel, and positivity of Γ_w forces λ_s ≥ 4p_2² − 3p_3, with physical margin Var(χ_{1/2}) ∼ 6/β². A final part collects observations on Weil positivity for the Riemann zeta function: in the theta-dressed jump formulation the dressed hop rate equals the critical constant 1/2 up to an explicit correction localised where the kernel Φ is not negligible (an exact consequence of W ∗ Φ = 0), so null-function dressings are critical and admit no dilute regime. This indicates why a current-type method does not transfer directly. The Sonin compression of Connes–Consani, the natural candidate ground state with a margin, stops bounding the Weil form on our test banks once the prime 2 enters. We also report finite-size comparator and lane data, experiments on the arithmetic side, and a dictionary between the two problems with explicit open target inequalities. Nothing here is a statement about continuum Yang–Mills theory or a proof of the Riemann hypothesis. Author: Andrei Ursachi (A. Ursachi; Ursachi, Andrei), independent researcher, ORCID 0009-0002-6114-5011. Version 2 (31 October 2026). Supersedes version 1; corrects an error in Definition 1 and extends the results.
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 report an arithmetically certified enclosure of the zero-temperature entropy per site of the six-state square-lattice Potts antiferromagnet: ln W(6) lies in [1.435107300597, 1.435107684912]. Both endpoints follow from established free-strip ratio and even-cylinder inequalities evaluated with colour and spatial symmetry quotients. Complete integer matrices and positive integer vectors support the spectral certificates. All 4,790,948 entries of eight archived quotient matrices have been independently reconstructed from the colouring compatibility rule. Four matched width budgets separate finite-root certification uncertainty from the remaining thermodynamic gap. At the largest budget the finite-root contribution is below 1.168 x 10^-13, compared with an interval width of 3.84315 x 10^-7. The record contains the eight-page preprint, LaTeX source, complete computational materials and checksums. We acknowledge Gewu Intelligence Lab for providing the collaborative research environment in which this project was developed. W.J. acknowledges support from the Strategic Priority Research Program of the Chinese Academy of Sciences under Grant No. XDB1680102.