anchors_unique_up_to_units
plain-language theorem explainer
Two anchor packs that uniquely calibrate bridges on one ledger, and that yield the same derived speed, land in the same class of the anchors quotient. Absolute-layer calibration arguments cite this to treat anchors as unique up to units once speed matches. The proof is a two-line reduction: same-speed implies the anchors equivalence, then quotient soundness.
Claim. Let $L$ be a ledger and $B_1,B_2$ bridges on $L$. Suppose anchors $A_1$ and $A_2$ each admit a unique units pack calibrating the corresponding bridge, and suppose the speeds computed from $A_1$ and $A_2$ are equal. Then $A_1$ and $A_2$ determine the same class in the anchors quotient: they are equivalent up to units.
background
In the RecogSpec layer, a ledger is a double-entry collection of recognition events. A bridge ties that ledger to display units. Anchors are the absolute-layer reference data from which one recovers an RS units pack (time and length scales, hence a speed).
UniqueCalibration is the witness that there exists a unique RSUnits pack calibrated to the given anchors: some units match the anchors, and any other calibrated pack equals that one. Speed is read off anchors by the sibling map that builds $c$ from the anchor scales. The anchors setoid quotients by the equivalence relation that identifies packs differing only by units; equality of quotient classes is the formal "same up to units" statement.
The local setting is the spec envelope that later installs explicit $\varphi$-formulas for the dimensionless pack. Upstream ledger and units infrastructure (ledger forcing, RS units, bridge core) supply the types; this lemma only needs the same-speed equivalence on anchors.
proof idea
From the hypothesis that the two speeds agree, apply the sibling lemma that equal speed implies the anchors equivalence relation. Then Quot.sound lifts that equivalence to equality of the two Quot.mk classes. The unique-calibration hypotheses frame the intended use (absolute-layer calibrated bridges) but are not consulted in the body: speed equality alone forces the setoid identification.
why it matters
Recognition Science fixes $c$, $\hbar$, and $G$ in RS-native units once the absolute layer is calibrated. Without uniqueness up to units, two anchor choices could silently disagree on the units pack even after matching speed. This theorem closes that gap inside RecogSpec: calibrated anchors with the same speed are one point in the quotient.
No downstream consumers are wired yet (used_by is empty). The declaration sits just above the canonical dimensionless defaults (explicit $\varphi$-formulas for the spec envelope), so it underwrites treating the anchor input to those packs as unique once speed is fixed. It is a bookkeeping uniqueness fact, not a forcing-chain step (T5–T8), but it keeps the absolute-layer calibration coherent with the units that feed $\alpha$-band and mass-ladder displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.