AnchorsEqv_symm
plain-language theorem explainer
Symmetry of the anchor speed-equivalence: if two measurement anchors induce the same calibration speed, the reverse pairing does too. Anyone assembling the setoid (or quotient) of anchors by physical calibration cites this. The proof is a one-line appeal to symmetry of propositional equality on the induced speeds.
Claim. Let $A,B$ be measurement anchors. If the calibration speeds they induce are equal, then the reverse holds: $\mathrm{speed}(B)=\mathrm{speed}(A)$. Equivalently, the relation "$A\sim B$ iff $\mathrm{speed}(A)=\mathrm{speed}(B)$" is symmetric.
background
Measurement anchors are pairs of real parameters $(a_1,a_2)$ with a consistency side-condition: if the time anchor vanishes then the length anchor must vanish, so that $c,\tau_0=\ell_0$ remains solvable. From any such pair one extracts a calibration speed via speedFromAnchors.
Two anchors are declared equivalent precisely when those induced speeds coincide. 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 present lemma is one of the three equivalence-relation axioms needed before Lean will accept a Setoid instance on the type of anchors.
proof idea
One-line term proof. The hypothesis is an equality of real numbers (the two induced speeds). Applying the standard symmetry of equality (Eq.symm) immediately yields the reversed equality, which is exactly the reversed instance of the relation.
why it matters
Feeds the setoid instance anchorsSetoid, whose iseqv triple is reflexivity, this symmetry lemma, and the matching transitivity lemma. That setoid is the gateway to the quotient of anchors by speed-equivalence, the formal home of "unique calibration up to units" inside RecogSpec.
In the broader Recognition framework this sits in the units-and-bands layer: once anchors are quotiented by induced speed, band checks and uniqueness-of-calibration statements can be stated on equivalence classes rather than on raw pairs, matching the physical claim that only the calibration speed (not the absolute scale of the two anchors) is observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.