AnchorsEqv_refl
plain-language theorem explainer
Any measurement anchor is equivalent to itself under the speed-calibration relation: two anchors match when they induce the same calibration speed. Anyone building the anchors setoid or the unique-up-to-units quotient cites this. The proof is a one-line reflexivity of equality on the induced speed.
Claim. For every measurement anchor $A$, the pair $(A,A)$ satisfies the anchor equivalence: the calibration speed induced by $A$ equals the calibration speed induced by $A$.
background
Measurement anchors are a minimal pair 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.
Anchor equivalence identifies two anchors precisely when those induced speeds agree. The doc-comment states the intent: anchors that yield the same speed represent the same physical calibration up to an overall scale, which is the quotienting relation for "unique up to units".
This lemma lives in the RecogSpec specification layer, where band checks and calibration uniqueness are packaged before verification bridges.
proof idea
One-line wrapper. Anchor equivalence is definitionally equality of the real number speedFromAnchors A with itself, so rfl discharges reflexivity. No lemmas are invoked beyond the definitional unfolding of the relation.
why it matters
Feeds the setoid instance anchorsSetoid, whose iseqv triple is exactly reflexivity, symmetry, and transitivity of this relation. That setoid is the carrier for the quotient of anchors by speed-equivalence, the formal home of "unique calibration up to units" in RecogSpec.
Without reflexivity the setoid (and any later quotient theorems about calibrated units or band membership independent of representative) cannot form. The step is elementary but mandatory scaffolding for the unique-calibration story that sits above the RS constants and band checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.