On this page
Quantum certificate evidence: available bytes, exact checks and missing obligations
9 October 2026. Family 266 has two different proof pipelines. This review adds selected manuscript reading, a pinned file inventory and 35 passing finite/source-data controls. It runs only our independent arithmetic study; it neither imports nor executes the upstream verifier, native programs or Lean kernel.
The conclusions must remain separate
| Evidence | Intended conclusion | What was established here |
|---|---|---|
| Native binary64 covering/exclusion pipeline | Exclude four arbitrary bases; with a lower construction, exactly three | Execution/arithmetic contract read; eleven named package paths absent in pinned checkout; pipeline not reproduced |
| Exact Fourier verifier | Pair and mixed moment certificates supporting Fourier vanishing and no seven-basis family | Verifier SHA matches the paper/wrapper; literal six Gram matrices independently checked; full moment identities not recomputed |
| MUBSix Comparator/solution entry | Fourier vanishing outside Tao equivalence and every attainable family has at most five members | Selected statement and entry read; imported closure/kernel acceptance not run |
| HadamardCubeFiber Comparator | A row-ratio fiber cancellation under two Hadamard premises and a two-cube-value condition | Statement/configuration read; supporting lemma is not the exactly-three theorem |
Detailed dossier. A compatible statement, a matching checksum and a successful partial calculation are different evidence levels.
The native execution contract
Eleven named paths are absent both from the tracked tree and the local paper directory: seven C++ files, extraction manifest, runner, computation-package README and reproduction instructions. Tracked file inventory records what this pinned paper directory contains. This establishes a local reproduction gap; external distributions were not exhaustively searched and the theorem is not thereby disproved.
Machine-readable obligations preserve the arithmetic, binary format, stages and terminal conditions. The paper requires separate binary64 operations, nearest rounding, no contraction/reassociation, masked exceptions and gradual underflow. The cover also needs two specific power-to-multiply lowerings checked in each rebuilt binary. Compiler flags, limited probes or absence of a dynamic pow symbol do not alone prove those semantics.
The reported execution contains 100 native invocations. Initial C has 15 exits of one and 163 unresolved graph-cap records; all must enter fallback. Four final shards then cover 1,127 fallback records with no saved failures. Treating every nonzero intermediate exit as terminal failure, or ignoring capped records because the supervisor later exits zero, would both misread the contract. Counts and byte identity establish coverage lineage only under the separate geometric and arithmetic arguments. Reported elapsed time 4,470.33 seconds is from the paper's platform, not a runtime we reproduced.
Independent exact matrix checks
The verifier's literal data were obtained through Python AST parsing and literal evaluation, without importing its code. Preserved literal data specifies block dimensions 5, 21, 11, 27, 22 and 12. Our exact rational LDL factorization reconstructs each matrix entry as L D L-transpose and verifies all 98 positive pivots. Reversing the coordinate order checks the paper's trailing-pivot condition: all 98 exceed 40,000; the smallest is about 41,331.17. The approximation is for display; exact fractions are retained in review.json.
Negative-diagonal mutations, singular/indefinite examples, exact rational positive matrices and asymmetric input rejection exercise the checker. The saved 35 controls also check the source checksum and stated count/negative-bound arithmetic. The displayed coefficient sum equals -2007321335237/30, but those coefficients were not derived from the full moment expansion here. Matrix positivity alone proves neither certificate nor any MUB family bound.
The full exact verifier has separate pair/mixed moment construction and exact substitution checks. Modular computations propose substitutions; a rational identity establishes their validity for real moments. A modular rank need not be the full rational rank of all unused equations. Reproducing those expansions and checking their semantic correspondence are outstanding tasks.
Software and commercial implication
A review module could inventory the actual artifact package, distinguish recovered failures from unresolved coverage, bind arithmetic/disassembly evidence to a build and map every conclusion to its exact proof obligation. This is a specialist integration into the shared evidence platform. No new standalone market or revenue is inferred.
BenchExec already supplies Linux execution/resource measurement and result tooling. ReproZip already packages programs and dependencies for reproduction. Those official descriptions were reviewed 9 October 2026; neither product was installed or benchmarked. A generic runner or archive wrapper has weak differentiation. Test whether a domain review finds actionable omissions beyond existing tools before charging for it.
Reading extent
Main PDF: pages 1-4 and 49-56; pages 50, 53 and 55 visually inspected. Exact companion: pages 1-3 and 16-25; pages 20, 24 and 25 visually inspected. Complete scope, two Comparator interfaces/configurations, wrapper and two solution entry files read. Selected verifier functions (lines 1-442 and 572-576) inspected; the literal data assignment parsed as data, not a full line-by-line code/proof review. Eleven source-file hashes are retained. The remaining mathematical arguments and imported formal closure are unaccepted.