anchorsSetoid
plain-language theorem explainer
Packages the speed-equivalence on measurement anchors as a Mathlib setoid. Two anchors are related exactly when they induce the same calibration speed. Anyone forming the quotient of anchors up to units, or stating uniqueness of calibration, cites this instance. The body is a one-line packaging of the three already-proved equivalence lemmas.
Claim. The binary relation on measurement anchors that holds precisely when two anchors induce the same calibration speed is an equivalence relation, and therefore endows the type of anchors with the structure of a setoid.
background
In RecogSpec, an anchor pair is a minimal measurement interface: two real numbers $(a_1,a_2)$ with the consistency rule that 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 the sibling speedFromAnchors).
The intended physical identification is not pointwise equality of the pair, but equality of that induced speed: anchors that yield the same speed represent the same physical calibration up to an overall scale. That relation is already defined as AnchorsEqv, with separate reflexivity, symmetry, and transitivity lemmas proved by rfl and Eq.symm.
Mathlib's Setoid is the standard carrier for a type equipped with an equivalence relation, and is the prerequisite for forming the quotient type used downstream.
proof idea
Definitional instance: the relation field is set to AnchorsEqv, and the iseqv triple is the product of the three sibling lemmas AnchorsEqv_refl, AnchorsEqv_symm, and AnchorsEqv_trans. No new reasoning; pure packaging into Mathlib's setoid interface.
why it matters
This instance is the setoid substrate for the quotient of anchors by speed-equivalence (AnchorsQuot := Quot anchorsSetoid). That quotient is the formal home of "unique up to units": the theorem anchors_unique_up_to_units states that any two anchor choices calibrating bridges from the same ledger are equivalent when they share calibration speed.
It is also the relation used by the verification certificate AnchorsRescaleEqvCert, which asserts that positive rescaling of anchors is invisible in the quotient (Quot.mk anchorsSetoid A = Quot.mk anchorsSetoid (rescaleAnchors s A)). In the broader Recognition stack this is the units-freedom step that lets band checks and bridge calibration talk about physical content rather than arbitrary scale choices for $(\tau_0,\ell_0)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.