AnchorsEqv
plain-language theorem explainer
Two measurement anchors are equivalent precisely when they induce the same calibration speed. Calibration and uniqueness-up-to-units arguments cite this relation as the quotienting predicate on anchor pairs. The body is a one-line definitional equality of the two induced speeds.
Claim. Two anchors $A_1=(a_1,a_2)$ and $A_2=(a_1',a_2')$ are equivalent if and only if the calibration speeds they determine coincide: $\mathrm{speed}(A_1)=\mathrm{speed}(A_2)$, where $\mathrm{speed}(A)=0$ if the time anchor vanishes and $a_2/a_1$ otherwise.
background
In RecogSpec, an anchor pair is a minimal measurement interface: two real numbers (time-like and length-like) together with a consistency side-condition that if the time anchor is zero then the length anchor is zero, so that $c,\tau_0=\ell_0$ remains solvable.
From any such pair one extracts a canonical calibration speed: zero in the fully degenerate case, otherwise the ratio of length anchor to time anchor. That speed is the only numerical invariant used here.
The local setting is the specification layer that turns raw anchors into units and band checks for bridge calibration. Equivalence of anchors is meant to capture "same physical calibration up to overall scale," not pointwise equality of the two real components.
proof idea
Definitional, not a proved lemma. The predicate is literally equality of the two values of the canonical speed map. No tactics, no upstream lemmas beyond the speed definition itself. Reflexivity, symmetry, and transitivity are discharged later by ordinary equality properties of that real number.
why it matters
This is the intended quotienting relation for "unique up to units" in the Recognition specification stack. It feeds the setoid instance on anchors, the three equivalence-law lemmas, the thin wrapper that same speed implies equivalence, and the uniqueness theorem that any two uniquely calibrated bridges from the same ledger yield equivalent anchors when their speeds match. Downstream, the anchors-rescale equivalence certificate in Verification reuses the same relation. Within RS, it separates physical calibration content (the induced $c$) from arbitrary choice of overall units, which is the right granularity for band checks and bridge certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.