Certified computation reproducibility workbench

Family 266: Exactly three mutually unbiased bases in dimension six. First application triage, 9 October 2026 Australia/Brisbane.

Problem and potential new use

Quantum measurement researchers can review six-dimensional MUB exclusions and reproduce the stated arithmetic/compiler verification conditions.

Applicability and commercial boundary

The strongest upper bound of three is computer-assisted under specified binary64 conditions. The selected Lean scope proves a weaker five-basis bound and supporting Fourier/cancellation statements; it does not certify exclusion of four arbitrary bases.

Initial business decision

Prototype evidence workflow. Buyer budget, commercial novelty and profitability are unvalidated.

Next verification action

Map every computation artifact and arithmetic condition to the exact conclusion before attempting trusted reproducibility.

Evidence scope

The catalog statement was individually reviewed. Main-paper abstract passages and available family scope notes were also inspected; paper-level theorem and algorithm details still require deeper review. No independent Lean check was run. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. See source metadata.

Main source

The maximum number of mutually unbiased bases in dimension six.