UniqueCalibration
plain-language theorem explainer
Absolute-layer calibration asserts that exactly one RS units pack matches the given anchors, forcing the calibration ratio. Anyone citing absolute-layer acceptance, inevitability of calibration, or uniqueness of anchors up to units would reference this. It is a pure existence-uniqueness proposition over the minimal RS units structure (tick, voxel length, speed).
Claim. For a ledger $L$, a bridge $B$ on $L$, and anchors $A$, there exists a unique RS units pack $U=(\tau_0,\ell_0,c)$ satisfying $c\,\tau_0=\ell_0$ that is calibrated to $A$: any other pack calibrated to $A$ equals $U$.
background
RecogSpec packages the absolute layer of Recognition Science: a ledger of recognition events, a bridge extracting display quantities, and anchors that fix the physical scale. The minimal units pack is the structure RSUnits with tick duration $\tau_0$, voxel length $\ell_0$, and speed $c$ linked by $c,\tau_0=\ell_0$. The RS-native gauge sets $\tau_0=1$ tick, $\ell_0=1$ voxel, $c=1$.
Calibration means the units pack is consistent with the chosen anchors (the sibling predicate Calibrated). Unique calibration is the absolute-layer witness that this match is unique, so the calibration ratio is forced rather than free. Downstream absolute-layer acceptance pairs this uniqueness with a bands check (MeetsBands).
proof idea
Definitional, not a proved theorem. The body is an existential-uniqueness proposition: there is some RSUnits pack calibrated to the anchors, and every calibrated pack equals that one. No tactics or lemmas fire at this declaration; discharge happens at use sites that construct a concrete pack (e.g. via unitsFromAnchors) and prove uniqueness from the anchor equations.
why it matters
This is the uniqueness half of absolute-layer acceptance. Parent results bundle it with band matching (absolute_layer_any, absolute_layer_from_eval_invariant, absolute_layer_invariant) and use it for anchor uniqueness up to units (anchors_unique_up_to_units) and the explicit evaluation match (matchesEval_explicit). The inevitability predicate Inevitability_absolute quantifies over all ledgers, bridges, and anchors asserting this property, so the whole absolute layer rests on it. In framework terms it locks the display units once anchors are fixed, which is required before dimensionless predictions (alpha band, mass ladder) can be compared to data without free scale parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.