uniqueCalibration_any
plain-language theorem explainer
For any ledger, bridge, and anchor triple there is a unique RS units pack calibrated to those anchors. Absolute-layer calibration uniqueness is therefore independent of the ledger and bridge choice. Anyone citing the absolute layer or UniqueCalibrationCert needs this. The proof exhibits the anchor-built units pack and forces componentwise equality of any other calibrated pack.
Claim. For every ledger $L$, every bridge $B$ on $L$, and every anchor triple $A$, there exists a unique RS-native units pack $U$ such that $U$ is calibrated to $A$: any other units pack calibrated to $A$ equals $U$.
background
In RecogSpec, the absolute layer separates units calibration from band checks. Calibration means a units pack (tick $\tau_0$, length $\ell_0$, speed $c$) matches a fixed anchor triple. The predicate UniqueCalibration asserts existence of one such pack together with uniqueness among all packs that meet the anchors.
The constructive witness is the units pack built directly from the anchors: speed is recovered from the anchor data, then $\tau_0$, $\ell_0$, and $c$ are filled so the pack is calibrated by construction. RS-native gauge sets $\tau_0 = 1$ tick, $\ell_0 = 1$ voxel, $c = 1$, but here the anchors may be arbitrary; the lemma only cares that calibration pins the pack uniquely.
Ledger and bridge appear in the signature so the absolute-layer interface is uniform across recognition data, yet neither enters the calibration equations. Upstream structure only supplies the types: a ledger is a double-entry event list; a bridge is a commuting native/display/observe triple.
proof idea
Unfold the uniqueness predicate and take the units pack built from the anchors as the witness. The first conjunct is the sibling fact that this pack is calibrated. For uniqueness, take any other calibrated pack, case on its record structure, and simplify the calibration equations together with the anchor-built definitions of speed and units. The three component equalities collapse by rfl, so the packs agree.
why it matters
This is the absolute-layer uniqueness fact for RecogSpec: calibration is forced once anchors are fixed, with no residual units freedom. Downstream, inevitability_absolute_holds is a one-line application over all ledger/bridge/anchor triples, discharging the absolute half of the inevitability scaffold. absolute_layer_from_eval_invariant packages the same uniqueness with a bands witness. Verification certificates UniqueCalibrationCert and HonestClosureCert quote it as the machine-checked claim that every anchors choice has a unique calibrated units pack.
In the broader RS picture this sits above the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$) and below display of constants in RS-native units. It does not derive $\phi$ or the mass ladder; it only locks the units gauge once anchors are chosen, which is what makes later band and constant claims unambiguous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.