AnchorsEqv_trans
plain-language theorem explainer
Anchor equivalence is transitive: equal calibration speeds compose. Anyone building the setoid (or quotient) of measurement anchors by physical calibration cites this. The proof is a one-line term that hands the two equalities to Eq.trans.
Claim. Let $A,B,C$ be measurement anchors. If $\mathrm{speed}(A)=\mathrm{speed}(B)$ and $\mathrm{speed}(B)=\mathrm{speed}(C)$, then $\mathrm{speed}(A)=\mathrm{speed}(C)$, where speed is the calibration speed induced by the anchor pair.
background
Measurement anchors are pairs $(a_1,a_2)\in\mathbb{R}^2$ with the consistency rule that a vanishing time anchor forces a vanishing length anchor, so $c,\tau_0=\ell_0$ stays solvable. From an anchor one extracts a calibration speed via speedFromAnchors (zero when the time anchor vanishes, otherwise the ratio of the two components).
AnchorsEqv declares two anchors equivalent precisely when those induced speeds agree. The doc-comment states the intent: this is the quotienting relation for "unique up to units," so anchors that yield the same speed represent the same physical calibration up to overall scale.
The local module packages RecogSpec band checks and calibration uniqueness; the three equivalence laws (refl, symm, trans) are the setoid ingredients.
proof idea
One-line term proof. AnchorsEqv is definitionally equality of real numbers (speedFromAnchors A = speedFromAnchors B), so the two hypotheses are ordinary equalities. The proof applies Eq.trans (written h1.trans h2) and is done. No unfolding of anchors or speed formulas is required.
why it matters
Feeds the setoid instance anchorsSetoid, whose iseqv triple is exactly refl/symm/trans for AnchorsEqv. That setoid is the gateway to the quotient of anchors by speed-equivalence, which is how RecogSpec formalizes "unique calibration up to units." Without transitivity the quotient does not exist as a Lean Setoid.
In the broader Recognition stack this sits under the RecogSpec calibration layer (bands, unique calibration, units from anchors), not under the T0–T8 forcing chain itself. It is bookkeeping that makes the physical identification of anchors rigorous before band checks and uniqueness theorems run on the quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.