What was already known
The 5/6 optimum and Bužek–Hillery channel are classical. The repository distinguishes its new stability estimates from the published optimality and asymmetric trade-off results; it gives no prior quantitative estimate of this form.
AI involvement
JD Jones directed the project. The disclosure says Claude produced the certificates, statements and Lean proofs; a later GPT consultation supplied extension statements and modules, checked before adoption.
JD Jones directed the project; Claude produced the selected stability statements, certificates and Lean proofs, and GPT supplied later extension statements and modules that were checked before adoption.
Importance
Quantifies how a nearly optimal six-state cloning channel must resemble the unique optimum, in both Kraus space and channel output.
Limitations
The claim uses six-state average fidelity and finite Kraus families. It does not assert a diamond-norm bound or equivalence with the Bloch-sphere average in Lean. The source reports a completed local Lean check, not independent human specialist review or external kernel replay.
Technical verification
The source reports completed lean proof checking of the kraus-space stability and channel-output stability theorems, with challenge/solution type matching and source-reported replays. This applies to the selected claim and is not an independent reproduction by AIProofWatch.
Formal checking
The source reports 44 completed Challenge statements, source and axiom audits, exact arithmetic replays and a Lean build; theorem 37 is Kraus-space stability and theorem 44 is channel stability.
- Checker
- Lean 4 kernel and documented local statement, axiom or certificate audits run by repository authors
- Scope
- For any finite-Kraus 1→2 qubit channel whose mean fidelity over the six Pauli eigenstates is at least 5/6−ε, the Kraus operators have total squared Frobenius distance at most 6ε from the span of the two Bužek–Hillery Kraus operators. For every input matrix ρ, the channel output is within 200√ε‖ρ‖F of the Bužek–Hillery channel in Frobenius norm.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
No independent human specialist review or human explanation of the stability mechanism is documented. Few is the evidence default.
Correction and publication history
Claim-level primary-source review of exact theorem, prior baseline, AI contribution and documented checking scope.
Read this published revision