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

CERTLIB: Machine-Verifiable Certificates for Quantum and Chemical Systems

Tennant, William

Published Jan 1, 2025• 0 citations
Publisher

Abstract

This record contains the preprint and complete machine-verifiable artifacts for CERTLIB, a solver-agnostic trust layer for quantum many-body and quantum chemistry computations. CERTLIB provides:a JSON-based schema for representing operator problems and exact rational certificates;a deterministic Python verifier that checks ncSOS and 2-RDM/PQG identities exactly over \mathbb{Q};a symbolic–numeric extraction pipeline for converting approximate floating-point solutions into exact rational algebraic identities.CERTLIB targets two widely used classes of operator statements:Noncommutative sum-of-squares (ncSOS) identitiesof the form H^{2} - \alpha H = \sum_{r} W_{r}^{\dagger} W_{r}, used in positivity and spectral-gap analysis.2-RDM dual certificates aligned with the PQG conerepresented via exact rational LDL^{\mathrm T} factorizations of dual matricesS = A - tI with D \succeq 0.All numeric entries in the JSON artifacts are encoded as{ "num": p, "den": q } with exact integer pairs, ensuring that verification requires no floating-point arithmetic.The reference verifier reconstructs each operator from JSON and checks the identities symbolically using Python’s fractions.Fraction.This package includes three case studies:L=20 ncSOS spin chain:An exact certificate for H^2 - H in a Pauli-bitset basis, sufficient to apply the Gosset–Mozgunov finite-size criterion for a bulk spectral gap under standard assumptions.O_3 active-space PQG examples (n = 66 and n = 153):2-RDM dual matrices derived from rationalized FCIDUMP data, each with an exact rational LDL^{\mathrm T} certificateS = A - tI = L D L^{\mathrm T}.Minimal PQG example with nonzero multipliers Y \neq 0:A hand-auditable 3×3 wedge-space problem demonstrating full CERTLIB support for adjoint mapsA = H - \mathcal{L}^*(Y) and nontrivial PQG multipliers.Contents of this Figshare record include:The PDF of the manuscript;JSON files for all ncSOS and PQG problems and certificates(spin chain, O_3 active spaces, and minimal PQG example with Y\neq 0);A Python reference verifier (verify_certificates.py) that re-checks every certificate exactly over \mathbb{Q};CERTLIB is intended as a lightweight reproducibility standard that journals, researchers, and software stacks can adopt to make numerical claims in quantum science auditable, portable, and verifiable by construction.

DOI
10.6084/m9.figshare.30614792

Related papers

Exact and certified bounds for the Bell inequality J62 of Pál and Vértesi

Artus Krohn-Grimberghe

This record contains the manuscript and complete verification artifact for the Bell inequality J62_4422 of Pál and Vértesi.It certifies the exact rational bracket750075557472719639 / 10^18 ≤ β_Q ≤ 750091086083765047288227625 / 10^27,and exact attainment of 3/4 by the stated two-qubit strategy. The lower endpoint is an exact rational strategy. The upper endpoint is certified by a sum-of-squares chain for the retained 365-word relaxation level.The Krawczyk certificate localizes the underlying KKT zero and establishes a strict local maximum, including negativity of the border form in all 256 boundary strata; it does not establish global optimality of that localized point. Accordingly, this work does not claim the exact quantum value, qubit-restricted optimality, minimum optimizer dimension, or global optimality of the localized KKT point.The archive includes SHA-256 manifests, standard-library replay programs, independently written certificate checks, mutation controls, and pinned full Krawczyk replays. The acceptance programs are fail-closed under optimized Python. The manuscript and certificates are licensed CC BY 4.0; verification code is licensed MIT.Version 1.1 is a hygiene-only update: it replaces one machine-local default path in a helper with the portable repository root ".", updates the corresponding checker and certificate source bindings, and leaves the mathematical calculation, inputs, claims, and replay outputs unchanged.

•Aug 28, 2026•0 citations

FEYNMAN-2 - Update

ALEXANDAR BALEVSKY

This update consolidates the formal, numerical, and publication-level corrections identified after Revision 3.0 of the FEINMAN 2 project and after direct execution of its reproducibility package. The underlying proposal remains a typed directed operator-graph calculus organized through the locked 4S-11S operator-space chain. The update does not introduce a new interaction or a confirmed deviation from standard quantum mechanics or quantum electrodynamics. Its main contribution is instead evidential and methodological: the complete package was checked by exact SHA-256 verification and rerun in the frozen environment (Python 3.13.5, NumPy 2.3.5, Linux x86_64/glibc 2.41), producing STATE=DONE and TESTS=PASS. The run reproduces the Cl(0,8) eight-generator certificate, the 32x32 extended Pauli certificate, the standard-QED anomalous-frequency checksum, the TERRA/ZERRA finite-grid count, and the frozen H2/H3+ finite-basis molecular outputs. The update corrects the benchmark-contract hash to c006873e...db777, distinguishes a recovery checksum from an independent one-loop integration, replaces the ambiguous bridge limit B->I by an explicitly declared identification or isometry between Hilbert spaces, and separates verified implementation claims from open physical claims. It also records incomplete executable coverage for graph-schema rejection tests, numerical no-signalling regression, and the TERRA/ZERRA norm-residual certificate. FEYNMAN-2 is therefore supported as a reproducible formal and computational research platform, while promotion to a physical theory still requires a nonidentity operator assignment frozen before a sealed holdout and independently replicated.

•Aug 4, 2026•0 citations

Verification scripts and deterministic outputs for "Entanglement-invariant topological fingerprint transitions in high-dimensional OAM biphoton states"

Cynthia Wright

This archive contains the reproducibility package for the manuscript “Entanglement-invariant topological fingerprint transitions in high-dimensional OAM biphoton states”. The files provide deterministic Python verification scripts and output logs for the analytic and numerical claims in the paper. The package includes verify_fast.py, which reproduces the F5,3 phase table, the universal count and chirality laws, the G5,3 fixed-entropy phase structure, the mixed-block sign structure, the robustness checks, and the worked D3 discriminant calculation. It includes verify_brouwer_slow.py, which performs a direct Brouwer-degree cross-check of the affine sector-degree criterion. It also includes analyze_fingerprint.py, which reports the active-sector counts, sign-resolved counts, chirality, and entropy values for the benchmark F5,3 and G5,3 examples. The output logs verify_results.out, verify_brouwer_slow.out, and analyze_fingerprint.out record the deterministic results used to support the manuscript. No experimental datasets are included; the associated article is a theoretical and computational study.

•Jul 7, 2026•0 citations

Towards near-term quantum simulation of materials

Laura Clinton, Toby S. Cubitt, Brian Flynn +6 more

Overview of data provided in support of Towards near-term quantum simulation of materials Contents of this folder: `analyse_materials_results.py`: script used to generate the summary tables and figures presented in the manuscript. `towards_quantum_simulation_data`: raw data used and produced when studying various 3D materials. `towards_quantum_simulation_analysis`: tables (in `.tex` format) and figures (as PDFs) presented in the manuscript. The contents of `towards_quantum_simulation_analysis` were generated by `analyse_materials_results.py`, i.e. the user need not run the script to produce the output files. Users can generate these analyses directly by running ```python analyse_materials_results.py```, though note the following packages will first need to be installed: `pandas >= 1.2.3` `numpy >= 1.23` `seaborn >= 0.11.1` `lfig >= 0.1.3` `matplotlib > 3.7.0` Included data Within `towards_quantum_simulation_data`, there are subfolders for each of the materials described in the manuscript, i.e. `SrVO3`, `GaAs`, `H3S`, `Si`, `Li2CuO2`. Within each material's folder are further subfolders for the `hamiltonian` and `encoding` used to represent the material, as well as subfolders for each of the `algorithms` studied. `hamiltonian`: files which specify the Hamiltonian for the material under study. There are a number of files `interactions.json` Hamiltonian terms in terms of Majorana monomials. `map_majorana_to_mode.json` keys are Majorana indices; values are the mode index to which they are associated. `map_mode_to_group.json` keys are mode indices; values are the group (or site) index to which they are associated. `map_group_to_position.json` keys are group indices; values are the corresponding 3D Cartesian coordinates of the lattice used to represent the material. `stage_data.json` contains key/value pairs of any other fields of interest. `encoding` files which specify the fermionic encoding which is customised for the material under study. `encoding.json` which details the edges of the hybrid compact encoding described in Section VI of the supplementary material. `precompiler.json` contains all the information which permits the encoding construction, including the Hamiltonian terms (`_interactions`) which match those in `hamiltonian/interactions.json`. The same mappings as present in the Hamiltonian data(a.g. `map_group_to_position`). `stage_data.json` contains key/value pairs of any other fields of interest. `algorithms` contains subfolders for each of the algorithms desribed in the manuscript Those explored for circuits depths: `TDSSplitTermsPriorityCircuitDepth` (TDS in the manuscript) `TDSSplitTermsPriorityCircuitDepthNoSwapNetwork` (TDS\*) `VQESplitTerms` (VQE) `VQESplitTermsNoSwapNetwork` (VQE*) each of which contain the files, inside the `circuitry` folder: `circuit_terms.csv`, which lists each individual term, together with their Pauli string and rotation angle, required to construct the corresponding quantum circuit `circuit_layers_to_implement.csv` groups the same terms into layers to achieve parallelism in the circuit. `stage_data.json` contains key/value pairs of any other fields of interest. and those used to compose measurement layers, as outlined in Section VII D of the supplementary material: `MeasurementCommutativity` `MeasurementNaiveQubitwise` `MeasurementNonCrossing` each of which contain the files, inside the `compilation` folder: `layers.csv` lists the terms which may be measured simultaneously to achieve the measurement strategies shown in Table S14. `stage_data.json` contains key/value pairs of any other fields of interest. CSV files In `towards_quantum_simulation_data`, there are unified CSV files containing the results of applying the procedures described in the manuscript to the target materials. `circuit_costs.csv`: results of running the circuit compiler described in the manuscript. `measurements.csv`: results of running the measurement compiler described in the manuscript. These CSVs are used in the analysis script `analyse_materials_results.py` to produce the figures and tables presented in the manuscript.

arXiv:2205.15256•May 30, 2022•8 citations

A Machine-Verified Separation of the Quantum and Almost-Quantum Sets in the 3322 Bell Scenario

Caleb Weiner

We give exact rational certificates for two results in the bipartite Bell scenario with three two-outcome measurements per party. First, the maximum of the $I_{3322}$ (Froissart) functional over the almost-quantum set -- the $1{+}AB$ level of the Navascues-Pironio-Acin (NPA) hierarchy -- is certified to lie between $0.2514708838$ and $0.2514709016$ (width $<2\times10^{-8}$), in the normalization with classical bound $0$ and quantum maximum $\approx0.2508754$; to our knowledge no value for this landmark had been published. Second, we exhibit a single exact rational behavior $T^{*}$ carrying certificates in both directions: a rational moment matrix proving $T^{*}$ almost-quantum, and a rational dual object proving that every NPA level-2 completion of $T^{*}$ requires slack at least $q=4.5934\times10^{-4}$, so that $T^{*}$ is not quantum. The strict inclusion $Q\subsetneq\tilde{Q}$ in the minimal three-setting scenario is thereby established end-to-end with no reliance on floating-point computation. Anatomically, the witness is locally quantum: all nine of its $2\times2$ correlator subtables pass the Tsirelson-Landau-Masanes criterion, so its non-quantumness is irreducibly a three-setting phenomenon, concentrated in ordering-dependent pseudo-moments coupling each party's third setting to the other's first two; the level-2 certificate is equivalently an exact sum-of-squares identity that any quantum state values nonnegatively and the witness is forced to value at $-q$. The certificates follow the rational rounding-projection-lifting programme recently developed for noncommutative optimization; for NPA moment matrices in canonical form the required projection reduces to a per-moment uniform shift, making certification essentially free at these sizes, and we work the programme in both the feasibility and infeasibility directions on one witness. Machine-checkable certificates and verifiers requiring only the Python standard library accompany the paper. Files in this record: the paper (PDF); exact rational certificates for both theorems (i3322_1AB_certificate.json, i3322_level2_infeasibility_certificate.json); standalone verifiers requiring only the Python 3 standard library (verify_i3322_certificate.py, verify_level2_certificate.py); and the generating scripts (certify_landmark.py, certify_level2.py). See README_ancillary.txt for which artifact proves which theorem and how to run the verifiers. v2: corrects the mechanism attribution in Sec. 5 (anatomy) and adds the archive reference to Data Availability; theorems, certificates, and verifiers unchanged.

•Jul 24, 2026•3 citations

The exact fourth-vector feasibility wall of the canonical MUB triple in dimension six

Noah Erlwein

For the canonical product MUB triple {Z₂ ⊗ Z₃, X₂ ⊗ Q₀, Y₂ ⊗ Q₁} in dimension six, known to admit no vector unbiased to all three bases, we prove an exact two-sided theorem for the projector-space feasibility functional f, where f(v) = 1 would characterize a candidate fourth unbiased vector. We show that the global maximum of f is W = (88 + 3√6) / 100 ≈ 0.9534846923. The bound is attained by an explicit algebraic unit vector, verified entirely in exact arithmetic over the field Q(ζ₂₄, √5). Its symmetry orbit contains 72 distinct maximizing rays. The matching global upper bound f ≤ W is established via an exact positive-semidefinite certificate at the level-2 Veronese lift. The certificate consists of a symmetric matrix over Q(√2, √3), whose polynomial identity and positivity are machine-verified in exact arithmetic and closed deterministically under the triple's 432-element symmetry group. No randomized computation or floating-point arithmetic appears anywhere in the proof chain. We further prove, via exact separating functionals, that degree-4 and degree-6 sum-of-squares certificates do not exist. In this precise sense, the lift level employed is minimal and necessary. Companion results include: • an exact product-vector ceiling for aligned product triples; • the exact wall value for the second known triple; • a complete Weyl-board census in dimension six, together with a Lean 4 kernel-verified combinatorial layer. These results completely characterize the pinned canonical triple. They do not resolve the MUB(6) problem, which remains open. The deposit contains two files: (1) the manuscript (PDF); (2) a complete verification bundle (ZIP; 91 files) containing all computational modules, tests, evidence receipts, execution logs, a SHA-256 manifest, and a minimal independent verifier (verify_global_certificate.py). The verifier is implemented in standard-library-only Python, shares no code with the certificate-construction pipeline, loads the stored exact certificate matrix, and independently re-establishes both directions of the global bound in approximately 150 seconds. Reproduction is available via: make verify-global Code is released under the Apache License 2.0 (with SPDX headers throughout the bundle). The manuscript text is released under CC BY 4.0. This research made extensive use of AI systems for conjecture generation, computation, proof drafting, and adversarial review. However, no mathematical claim depends on the correctness of any AI system. Every reported result is verified by exact rational arithmetic, exact interval arithmetic, or the Lean 4 kernel, and all verification artifacts are included in the deposit.

•Jun 12, 2026•0 citations
This record contains the preprint and complete machine-verifiable artifacts for CERTLIB, a solver-agnostic trust layer for quantum many-body and quantum chemistry computations. CERTLIB provides:a JSON-based schema for representing operator problems and exact rational certificates;a deterministic Python verifier that checks ncSOS and 2-RDM/PQG identities exactly over \mathbb{Q};a symbolic–numeric extraction pipeline for converting approximate floating-point solutions into exact rational algebraic identities.CERTLIB targets two widely used classes of operator statements:Noncommutative sum-of-squares (ncSOS) identitiesof the form H^{2} - \alpha H = \sum_{r} W_{r}^{\dagger} W_{r}, used in positivity and spectral-gap analysis.2-RDM dual certificates aligned with the PQG conerepresented via exact rational LDL^{\mathrm T} factorizations of dual matricesS = A - tI with D \succeq 0.All numeric entries in the JSON artifacts are encoded as{ "num": p, "den": q } with exact integer pairs, ensuring that verification requires no floating-point arithmetic.The reference verifier reconstructs each operator from JSON and checks the identities symbolically using Python’s fractions.Fraction.This package includes three case studies:L=20 ncSOS spin chain:An exact certificate for H^2 - H in a Pauli-bitset basis, sufficient to apply the Gosset–Mozgunov finite-size criterion for a bulk spectral gap under standard assumptions.O_3 active-space PQG examples (n = 66 and n = 153):2-RDM dual matrices derived from rationalized FCIDUMP data, each with an exact rational LDL^{\mathrm T} certificateS = A - tI = L D L^{\mathrm T}.Minimal PQG example with nonzero multipliers Y \neq 0:A hand-auditable 3×3 wedge-space problem demonstrating full CERTLIB support for adjoint mapsA = H - \mathcal{L}^*(Y) and nontrivial PQG multipliers.Contents of this Figshare record include:The PDF of the manuscript;JSON files for all ncSOS and PQG problems and certificates(spin chain, O_3 active spaces, and minimal PQG example with Y\neq 0);A Python reference verifier (verify_certificates.py) that re-checks every certificate exactly over \mathbb{Q};CERTLIB is intended as a lightweight reproducibility standard that journals, researchers, and software stacks can adopt to make numerical claims in quantum science auditable, portable, and verifiable by construction.
This record contains the manuscript and complete verification artifact for the Bell inequality J62_4422 of Pál and Vértesi.It certifies the exact rational bracket750075557472719639 / 10^18 ≤ β_Q ≤ 750091086083765047288227625 / 10^27,and exact attainment of 3/4 by the stated two-qubit strategy. The lower endpoint is an exact rational strategy. The upper endpoint is certified by a sum-of-squares chain for the retained 365-word relaxation level.The Krawczyk certificate localizes the underlying KKT zero and establishes a strict local maximum, including negativity of the border form in all 256 boundary strata; it does not establish global optimality of that localized point. Accordingly, this work does not claim the exact quantum value, qubit-restricted optimality, minimum optimizer dimension, or global optimality of the localized KKT point.The archive includes SHA-256 manifests, standard-library replay programs, independently written certificate checks, mutation controls, and pinned full Krawczyk replays. The acceptance programs are fail-closed under optimized Python. The manuscript and certificates are licensed CC BY 4.0; verification code is licensed MIT.Version 1.1 is a hygiene-only update: it replaces one machine-local default path in a helper with the portable repository root ".", updates the corresponding checker and certificate source bindings, and leaves the mathematical calculation, inputs, claims, and replay outputs unchanged.
This update consolidates the formal, numerical, and publication-level corrections identified after Revision 3.0 of the FEINMAN 2 project and after direct execution of its reproducibility package. The underlying proposal remains a typed directed operator-graph calculus organized through the locked 4S-11S operator-space chain. The update does not introduce a new interaction or a confirmed deviation from standard quantum mechanics or quantum electrodynamics. Its main contribution is instead evidential and methodological: the complete package was checked by exact SHA-256 verification and rerun in the frozen environment (Python 3.13.5, NumPy 2.3.5, Linux x86_64/glibc 2.41), producing STATE=DONE and TESTS=PASS. The run reproduces the Cl(0,8) eight-generator certificate, the 32x32 extended Pauli certificate, the standard-QED anomalous-frequency checksum, the TERRA/ZERRA finite-grid count, and the frozen H2/H3+ finite-basis molecular outputs. The update corrects the benchmark-contract hash to c006873e...db777, distinguishes a recovery checksum from an independent one-loop integration, replaces the ambiguous bridge limit B->I by an explicitly declared identification or isometry between Hilbert spaces, and separates verified implementation claims from open physical claims. It also records incomplete executable coverage for graph-schema rejection tests, numerical no-signalling regression, and the TERRA/ZERRA norm-residual certificate. FEYNMAN-2 is therefore supported as a reproducible formal and computational research platform, while promotion to a physical theory still requires a nonidentity operator assignment frozen before a sealed holdout and independently replicated.
This archive contains the reproducibility package for the manuscript “Entanglement-invariant topological fingerprint transitions in high-dimensional OAM biphoton states”. The files provide deterministic Python verification scripts and output logs for the analytic and numerical claims in the paper. The package includes verify_fast.py, which reproduces the F5,3 phase table, the universal count and chirality laws, the G5,3 fixed-entropy phase structure, the mixed-block sign structure, the robustness checks, and the worked D3 discriminant calculation. It includes verify_brouwer_slow.py, which performs a direct Brouwer-degree cross-check of the affine sector-degree criterion. It also includes analyze_fingerprint.py, which reports the active-sector counts, sign-resolved counts, chirality, and entropy values for the benchmark F5,3 and G5,3 examples. The output logs verify_results.out, verify_brouwer_slow.out, and analyze_fingerprint.out record the deterministic results used to support the manuscript. No experimental datasets are included; the associated article is a theoretical and computational study.
Overview of data provided in support of Towards near-term quantum simulation of materials Contents of this folder: `analyse_materials_results.py`: script used to generate the summary tables and figures presented in the manuscript. `towards_quantum_simulation_data`: raw data used and produced when studying various 3D materials. `towards_quantum_simulation_analysis`: tables (in `.tex` format) and figures (as PDFs) presented in the manuscript. The contents of `towards_quantum_simulation_analysis` were generated by `analyse_materials_results.py`, i.e. the user need not run the script to produce the output files. Users can generate these analyses directly by running ```python analyse_materials_results.py```, though note the following packages will first need to be installed: `pandas >= 1.2.3` `numpy >= 1.23` `seaborn >= 0.11.1` `lfig >= 0.1.3` `matplotlib > 3.7.0` Included data Within `towards_quantum_simulation_data`, there are subfolders for each of the materials described in the manuscript, i.e. `SrVO3`, `GaAs`, `H3S`, `Si`, `Li2CuO2`. Within each material's folder are further subfolders for the `hamiltonian` and `encoding` used to represent the material, as well as subfolders for each of the `algorithms` studied. `hamiltonian`: files which specify the Hamiltonian for the material under study. There are a number of files `interactions.json` Hamiltonian terms in terms of Majorana monomials. `map_majorana_to_mode.json` keys are Majorana indices; values are the mode index to which they are associated. `map_mode_to_group.json` keys are mode indices; values are the group (or site) index to which they are associated. `map_group_to_position.json` keys are group indices; values are the corresponding 3D Cartesian coordinates of the lattice used to represent the material. `stage_data.json` contains key/value pairs of any other fields of interest. `encoding` files which specify the fermionic encoding which is customised for the material under study. `encoding.json` which details the edges of the hybrid compact encoding described in Section VI of the supplementary material. `precompiler.json` contains all the information which permits the encoding construction, including the Hamiltonian terms (`_interactions`) which match those in `hamiltonian/interactions.json`. The same mappings as present in the Hamiltonian data(a.g. `map_group_to_position`). `stage_data.json` contains key/value pairs of any other fields of interest. `algorithms` contains subfolders for each of the algorithms desribed in the manuscript Those explored for circuits depths: `TDSSplitTermsPriorityCircuitDepth` (TDS in the manuscript) `TDSSplitTermsPriorityCircuitDepthNoSwapNetwork` (TDS\*) `VQESplitTerms` (VQE) `VQESplitTermsNoSwapNetwork` (VQE*) each of which contain the files, inside the `circuitry` folder: `circuit_terms.csv`, which lists each individual term, together with their Pauli string and rotation angle, required to construct the corresponding quantum circuit `circuit_layers_to_implement.csv` groups the same terms into layers to achieve parallelism in the circuit. `stage_data.json` contains key/value pairs of any other fields of interest. and those used to compose measurement layers, as outlined in Section VII D of the supplementary material: `MeasurementCommutativity` `MeasurementNaiveQubitwise` `MeasurementNonCrossing` each of which contain the files, inside the `compilation` folder: `layers.csv` lists the terms which may be measured simultaneously to achieve the measurement strategies shown in Table S14. `stage_data.json` contains key/value pairs of any other fields of interest. CSV files In `towards_quantum_simulation_data`, there are unified CSV files containing the results of applying the procedures described in the manuscript to the target materials. `circuit_costs.csv`: results of running the circuit compiler described in the manuscript. `measurements.csv`: results of running the measurement compiler described in the manuscript. These CSVs are used in the analysis script `analyse_materials_results.py` to produce the figures and tables presented in the manuscript.
We give exact rational certificates for two results in the bipartite Bell scenario with three two-outcome measurements per party. First, the maximum of the I3322I_{3322}I3322​ (Froissart) functional over the almost-quantum set -- the 1+AB1{+}AB1+AB level of the Navascues-Pironio-Acin (NPA) hierarchy -- is certified to lie between 0.25147088380.25147088380.2514708838 and 0.25147090160.25147090160.2514709016 (width <2×10−8<2\times10^{-8}<2×10−8), in the normalization with classical bound 000 and quantum maximum ≈0.2508754\approx0.2508754≈0.2508754; to our knowledge no value for this landmark had been published. Second, we exhibit a single exact rational behavior T∗T^{*}T∗ carrying certificates in both directions: a rational moment matrix proving T∗T^{*}T∗ almost-quantum, and a rational dual object proving that every NPA level-2 completion of T∗T^{*}T∗ requires slack at least q=4.5934×10−4q=4.5934\times10^{-4}q=4.5934×10−4, so that T∗T^{*}T∗ is not quantum. The strict inclusion Q⊊Q~Q\subsetneq\tilde{Q}Q⊊Q~​ in the minimal three-setting scenario is thereby established end-to-end with no reliance on floating-point computation. Anatomically, the witness is locally quantum: all nine of its 2×22\times22×2 correlator subtables pass the Tsirelson-Landau-Masanes criterion, so its non-quantumness is irreducibly a three-setting phenomenon, concentrated in ordering-dependent pseudo-moments coupling each party's third setting to the other's first two; the level-2 certificate is equivalently an exact sum-of-squares identity that any quantum state values nonnegatively and the witness is forced to value at −q-q−q. The certificates follow the rational rounding-projection-lifting programme recently developed for noncommutative optimization; for NPA moment matrices in canonical form the required projection reduces to a per-moment uniform shift, making certification essentially free at these sizes, and we work the programme in both the feasibility and infeasibility directions on one witness. Machine-checkable certificates and verifiers requiring only the Python standard library accompany the paper. Files in this record: the paper (PDF); exact rational certificates for both theorems (i3322_1AB_certificate.json, i3322_level2_infeasibility_certificate.json); standalone verifiers requiring only the Python 3 standard library (verify_i3322_certificate.py, verify_level2_certificate.py); and the generating scripts (certify_landmark.py, certify_level2.py). See README_ancillary.txt for which artifact proves which theorem and how to run the verifiers. v2: corrects the mechanism attribution in Sec. 5 (anatomy) and adds the archive reference to Data Availability; theorems, certificates, and verifiers unchanged.
For the canonical product MUB triple {Z₂ ⊗ Z₃, X₂ ⊗ Q₀, Y₂ ⊗ Q₁} in dimension six, known to admit no vector unbiased to all three bases, we prove an exact two-sided theorem for the projector-space feasibility functional f, where f(v) = 1 would characterize a candidate fourth unbiased vector. We show that the global maximum of f is W = (88 + 3√6) / 100 ≈ 0.9534846923. The bound is attained by an explicit algebraic unit vector, verified entirely in exact arithmetic over the field Q(ζ₂₄, √5). Its symmetry orbit contains 72 distinct maximizing rays. The matching global upper bound f ≤ W is established via an exact positive-semidefinite certificate at the level-2 Veronese lift. The certificate consists of a symmetric matrix over Q(√2, √3), whose polynomial identity and positivity are machine-verified in exact arithmetic and closed deterministically under the triple's 432-element symmetry group. No randomized computation or floating-point arithmetic appears anywhere in the proof chain. We further prove, via exact separating functionals, that degree-4 and degree-6 sum-of-squares certificates do not exist. In this precise sense, the lift level employed is minimal and necessary. Companion results include: • an exact product-vector ceiling for aligned product triples; • the exact wall value for the second known triple; • a complete Weyl-board census in dimension six, together with a Lean 4 kernel-verified combinatorial layer. These results completely characterize the pinned canonical triple. They do not resolve the MUB(6) problem, which remains open. The deposit contains two files: (1) the manuscript (PDF); (2) a complete verification bundle (ZIP; 91 files) containing all computational modules, tests, evidence receipts, execution logs, a SHA-256 manifest, and a minimal independent verifier (verify_global_certificate.py). The verifier is implemented in standard-library-only Python, shares no code with the certificate-construction pipeline, loads the stored exact certificate matrix, and independently re-establishes both directions of the global bound in approximately 150 seconds. Reproduction is available via: make verify-global Code is released under the Apache License 2.0 (with SPDX headers throughout the bundle). The manuscript text is released under CC BY 4.0. This research made extensive use of AI systems for conjecture generation, computation, proof drafting, and adversarial review. However, no mathematical claim depends on the correctness of any AI system. Every reported result is verified by exact rational arithmetic, exact interval arithmetic, or the Lean 4 kernel, and all verification artifacts are included in the deposit.