What exactly is machine-checked in CSD?

The short answer

"Machine-checked" gets used loosely, so here's the strict sense this programme means. A proof assistant is a computer program that accepts a proof only when every step follows from earlier steps by fixed logical rules, and the one used here is called Lean. Every theorem in the CSD corpus, tens of thousands of lines of it, has passed that check all the way down to Lean's logical core, so no step in any proof is taken on trust.

Two facts sharpen the claim. First, every mathematical proof rests on some basic assumptions, and Lean has a small fixed set of them built in. The corpus adds none of its own, as an early dependence on an unproved representation theorem was removed by proving that theorem. Second, the physical postulates of CSD aren't assumptions slipped in at the foundations, as they appear as explicit hypotheses in the statements of the theorems that use them, so a reader can see exactly what each result costs and where it pays.

Equally strict is what checking can't do. A proof assistant can't certify that a formal statement means what the accompanying prose says it means, so the real failure mode is a fluent but false description of a true theorem, and the repository runs automatic checks against prose drifting away from the mathematics, and says plainly that reading the mathematics as physics is a human responsibility.

The longer answer

The verification is layered. The library and its regression suite build with every warning treated as an error. An audit records, for each headline result, exactly which foundational assumptions it rests on, so any change in that list is caught. A validation ledger tracks the status of each claim row by row. And a battery of guard scripts checks the things a compiler can't see, statements that hold for empty reasons, hypotheses that are carried but never used, prose claims that outrun what the proofs actually connect, and glossary anchors such as the ones behind this page.

Three commitments make the posture distinctive. Postulates are hypotheses rather than axioms, honest notes on scope live inside the modules themselves rather than in a separate document, and a stated rule requires that an obstacle be reported as an obstacle rather than hidden behind a placeholder.

What is actually proved

The kernel-checked corpus spans the frequency layer, the measure and Born tiers, measurement dynamics, the entangled tier, the record layer, thermodynamics and the finite field track. An axiom-audit suite pins every headline constant's axiom set, and every pinned constant reports exactly Lean's three foundational axioms, propext, Classical.choice and Quot.sound, so the corpus imports no axiom of its own. The staging tree contributes Mathlib-candidate infrastructure, the partial trace and the general Lie-Trotter formula among it, built CSD-free.

The quantum-information layer is reached from the posits by theorems rather than by instantiation, as the density operator of a preparation on the surface is the barycentre of its rays, channels are the environment marginals of volume-preserving flows that lift a unitary, and the second law, data processing, Landauer's bound, concavity, the Holevo capacity of the de-isolation channel and error correction on the three-qubit register are all stated for preparations on the surface. Strong subadditivity remains conditional on an explicit data-processing hypothesis, which the audit records.

Related entries

• Witness and engineA working model proves that the machinery runs, and it doesn't prove that the machinery is the world, so CSD names that distinction and audits itself against it.
• LF1 main theoremIn a deterministic world with repeated preparations, the frequencies you observe converge to volume ratios with probability one, and the theorem is machine-checked with no randomness anywhere in the dynamics.
• Partial traceMathlib has no partial trace for matrices, so the corpus built one, the staple operation of quantum information, with its working properties proved and staged for contribution upstream.
• Lie-Trotter product formulaAlternate many tiny steps of two operations that don't commute and the result converges to the exponential of their sum, with an error that shrinks like one over the number of steps, and CSD proves this in textbook generality, in a form ready for the Mathlib library, because its open-systems tier needed it and nothing on the shelf existed.
• Does CSD make new predictions?Not yet, and the programme doesn't pretend otherwise, as the present claim is that CSD reproduces the predictions of quantum mechanics from fewer postulates, with the reproduction machine-checked, while candidate departures are recorded as owed future work rather than asserted.