anchors_eq_of_same_speed
plain-language theorem explainer
Two anchors that induce the same calibration speed are equivalent under the speed-based anchor relation. Calibration and uniqueness arguments in RecogSpec cite this when quotienting anchor choices. The proof is a one-line unfolding of the equivalence definition.
Claim. If $A_1$ and $A_2$ are anchors with equal induced calibration speed, then $A_1$ and $A_2$ are equivalent: they stand in the relation that identifies anchors precisely when those speeds coincide.
background
In RecogSpec, an anchor pair supplies the dimensional reference used to read a bridge off a ledger. The map from anchors to calibration speed extracts the single scalar that sets how those anchors convert ledger structure into physical units.
Equivalence of anchors is defined to be equality of that induced speed. The relation is the intended quotient for "unique up to units": anchors that yield the same speed represent the same physical calibration up to overall scale.
The local setting is the specification layer that ties ledgers, bridges, and band constraints to a unique calibration. Degenerate anchors (vanishing first component) need separate consistency checks elsewhere; the main nondegenerate case is direct.
proof idea
One-line wrapper. The goal is the anchor equivalence proposition, whose definition is exactly equality of induced speeds. simpa unfolds that definition and discharges the goal from the given speed-equality hypothesis.
why it matters
Feeds the uniqueness theorem that any two anchor choices calibrating bridges from the same ledger are equivalent whenever their induced speeds match. That parent result is the RecogSpec statement of calibration uniqueness up to units: once speed agrees, the anchors are identified in the quotient.
Without this bridge lemma, uniqueness proofs would re-unfold the equivalence at every use site. It is bookkeeping rather than new physics, but it locks the quotient relation used when comparing calibrated bridges and band-meeting certificates in the specification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.