UniqueCalibrationCert
plain-language theorem explainer
An empty audit certificate whose verified predicate asserts that every recognition ledger, bridge, and anchor triple admits a unique RS-units calibration pack, with speed fixed by the anchors. Spec auditors cite it to make absolute-layer unit uniqueness machine-checked rather than implicit. The companion verified_any result is a one-line wrapper around uniqueCalibration_any.
Claim. A UniqueCalibration certificate is a unit-like witness type. Its verification condition is: for every ledger $L$, every bridge $B$ on $L$, and every anchor pair $A$, the Recognition Spec unique-calibration property holds for $(L,B,A)$ (a unique RS-units pack calibrated to those anchors, speed determined by the anchors).
background
In the Recognition Spec, a ledger is a double-entry collection of recognition events; a bridge maps native structure to display and observable layers under a commuting observation law; anchors fix the absolute calibration data from which speed is recovered. The module packages absolute-layer calibration as an explicit audit certificate rather than an ambient choice.
The underlying claim, stated in the module doc, is that for every ledger/bridge and every anchor pair there is a unique RS-units pack calibrated to those anchors, with speed determined by speedFromAnchors. This certificate only reifies that universal statement as a named, checkable Prop on a trivial carrier type.
proof idea
The structure is empty aside from Repr. The verified predicate is defined as the universal quantification over ledgers, bridges, and anchors of the Spec unique-calibration property. The simp theorem verified_any is a one-line wrapper: introduce $L$, $B$, $A$, then apply RecogSpec.uniqueCalibration_any.
why it matters
This sits in the Verification layer as an audit token: it forces the absolute-layer calibration witness to be named and machine-checked instead of left as an implicit Spec fact. Downstream use is not yet wired in this graph (no used_by edges), so its role is documentary and compositional: any later certificate or end-to-end RS consistency check that needs unique unit packs can require UniqueCalibrationCert.verified rather than re-proving the Spec lemma. It does not itself touch the forcing chain (T5–T8), the RCL, or the mass ladder; it only locks the uniqueness of the RS-units calibration relative to chosen anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.