2.17. What proved is checked to mean🔗

A proved status is stronger than "a theorem of that name compiles", and two guarantees that lake build does not enforce on its own are carried by a dedicated validation suite (PropertyKindCalculus.Tests, one probe per requirement group), built by CI alongside the dimension and uncertainty layers so that all twenty verifiable requirements — not only those whose theorems live in the Mathlib-free core — are under regression on every change.

First, each verifiable requirement's theorem has its axiom profile pinned with #guard_msgs over #print axioms, so proved means sorry-free as certified by the axiom set, not merely that no sorry keyword appears: a proof relocated behind a sorry raises no warning at its call sites, and only the axiom profile exposes it. (The exportable core is largely axiom-free — most of its capstones depend on nothing at all, the rest on propext and Quot.sound from omega and structure equality, with Classical.choice reached by a single declaration; the Mathlib-backed layers use the three standard classical axioms. What the suite pins is each theorem's profile exactly, whatever it is, so a change to any of them is a build failure rather than a footnote.) Second, each theorem is applied to a concrete witness whose premises are discharged — and, at the degenerate boundary where a premise fails, shown genuinely excluded — so that no requirement is satisfied vacuously: an empty quantifier or an unsatisfiable hypothesis would leave a theorem true but empty, and the witness is what rules that out.

What a proved status rests on is the stack Figure 2 draws: a domain model's trust traces down through PhysLib and cslib, the two peers on Mathlib, and through TorchLean with FloatLib under it, to Mathlib and then to the Lean kernel with its three classical axioms — the one band that is believed rather than derived, checked, or enumerated. The axiom profile pinned above is that band's cost, stated per theorem.