speedFromAnchors_of_eq_zero
plain-language theorem explainer
If the time anchor vanishes, the canonical speed extracted from a measurement-anchor pair is zero. Band-check and unit-calibration proofs cite this as the zero branch of the speed definition. The proof is a one-line simp unfolding of the if-then definition under the hypothesis a1 = 0.
Claim. Let $A=(a_1,a_2)$ be a measurement-anchor pair. If $a_1=0$, then the canonical speed determined by $A$ equals $0$.
background
In RecogSpec, measurement anchors are a minimal interface for band checks: a pair of real numbers $(a_1,a_2)$ together 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.
The canonical speed from anchors is defined by cases: $\mathrm{speed}(A)=0$ when $a_1=0$, and $a_2/a_1$ otherwise. That definition is the direct source of the present lemma; the zero branch is exactly the claim here.
Sibling material in the same module builds units $(\tau_0,\ell_0,c)$ from the same anchors and records calibration and band-meeting predicates. The lemma is the simp fact that makes the zero-time-anchor case reduce without case-splitting at every use site.
proof idea
One-line wrapper: simp unfolds speedFromAnchors and rewrites with the hypothesis $a_1=0$, selecting the then-branch of the definitional if, which is definitionally $0$.
why it matters
RecogSpec packages the RS measurement interface used by verification bridges and band certificates. Speed from anchors is the ratio that feeds unit calibration (unitsFromAnchors) and the calibrated/unique-calibration predicates downstream in the same module.
This simp lemma closes the zero branch so that later equalities such as units-from-anchors recovering $c$, and band checks under vanishing anchors, do not re-prove the case split. It is local plumbing rather than a forcing-chain step (T0–T8), but it keeps the anchor-to-units path definitionally clean when the time anchor is degenerate.
No external used-by edges are recorded yet; the natural consumers are the sibling lemmas on nonzero speed and on units extracted from anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.