MathIdeasResearch in progressRepository ↗
← Research catalogOriginal Markdown ↓
On this page

Certified numerical computation reproducibility workbench

Initial decision: Prototype evidence workflow. First dossier, 9 October 2026 Australia/Brisbane. No buyer validation or profitability evidence has been established.

Research finding

The dimension-six mutually unbiased bases paper claims exactly three, with exclusion of four arbitrary bases through a documented computation under specified binary64 and compiler conditions. A companion uses exact integer/rational Fourier certificates. The selected Lean scope establishes a weaker five-basis bound and supporting Fourier/cancellation statements, not the headline upper bound of three.

Problem and buyer

A research lab publishing computer-assisted results needs to preserve the conditions under which a numerical certificate is valid and distinguish that evidence from a formal theorem covering a weaker result. Reviewers otherwise receive a successful log without enough context to reproduce its meaning.

What the finding could enable

A reproducibility system can assemble arithmetic model, compiler flags, source hashes, certificate inputs, verifier identity, environmental constraints and exact claim mapping. This specializes the proof artifact registry to certified numerical computation and can introduce a hybrid evidence packet containing exact arithmetic, floating-point certificates and selected Lean coverage without conflating them.

Technical and commercial limits

Binary64 execution assumptions can depend on compiler options, rounding, fused operations and platform details specified by the paper. Running an untrusted verifier directly is not a trusted proof check. The full pipeline has not been independently reproduced here, and a machine verdict alone does not establish the intended semantic theorem.

Minimal architecture

Shared artifact registry -> claim-to-certificate graph -> compiler/arithmetic contract -> immutable input hashes -> controlled verifier runner -> complete logs -> coverage-difference report. Begin with static manifest extraction and a reviewer-readable packet; add a trusted isolated environment before automated verified labels.

Existing alternatives and differentiation

Comparator already supports selected formal statement checks, while the companion research includes a complete exact verifier. The commercial contribution would be reproducible packaging, hybrid evidence lineage and review operations. A simple wrapper around an existing verifier is insufficient differentiation. Comparator.

Monetization hypothesis

Hypothesis: AUD 5,000–15,000 for a bounded reproducibility audit, then bundle recurring runs into opportunity 001 rather than sell a second registry subscription. At an illustrative AUD 8,000 audit with 30 expert hours costed at AUD 180/hour, AUD 2,600 remains before environment engineering, compute and overhead. Specialist demand may be too small for a standalone business.

Validation experiment

Extract the exact arithmetic and compiler obligations for the MUB exclusion and map which conclusion each certificate or formal module supports. Create an intentionally missing compiler flag and a weaker formal-scope record; the report must expose both instead of claiming exactly-three formal verification.

Conditions to reject or defer

Reject if publishing teams already produce equivalent reproducible packets through inexpensive CI, or if a trusted environment costs more to maintain than the audit revenue. Defer a verified exactly-three badge until the stated complete pipeline is independently reproduced and its trust assumptions reviewed.

Next concrete action

Read the computation pipeline’s arithmetic appendix and produce a static obligation manifest without executing bundled verifier code.

Pinned research sources