speedFromAnchors_of_ne_zero
plain-language theorem explainer
When the time anchor is nonzero, the canonical speed extracted from a measurement-anchor pair equals the plain ratio of length anchor to time anchor. Calibration and units-from-anchors proofs cite this to discharge the nonzero branch of the speed definition. The proof is a one-line simp unfolding of that definition under the nonzero hypothesis.
Claim. Let $A=(a_1,a_2)$ be a pair of real measurement anchors. If $a_1\neq 0$, then the canonical speed determined by $A$ equals $a_2/a_1$.
background
RecogSpec packages the minimal measurement interface used by band checks and unit calibration. An Anchors pair carries a real time-like anchor $a_1$ and a length-like anchor $a_2$, together with the consistency rule that vanishing $a_1$ forces vanishing $a_2$ so the relation $c,\tau_0=\ell_0$ stays solvable.
The canonical speed from anchors is defined by cases: it is $0$ when $a_1=0$, and otherwise the ratio $a_2/a_1$. That definition is the sole upstream object this lemma specializes. Sibling lemmas handle the zero branch and the full units triple $(\tau_0,\ell_0,c)$ built from the same anchors.
proof idea
One-line wrapper: simp unfolds speedFromAnchors and rewrites with the hypothesis $a_1\neq 0$, selecting the else-branch $a_2/a_1$. No further lemmas are needed.
why it matters
Feeds the private rescale certificate speedFromAnchors_rescale in UnitsFromAnchorsRescaleCert, which shows that positive rescaling of both anchors leaves the extracted speed invariant. That invariance is part of the verification path that units calibrated from anchors are well-defined up to overall scale, so band checks and display constants do not depend on an arbitrary anchor normalization.
In the broader Recognition stack this is bookkeeping rather than a forcing-chain step: it keeps the speed leg of the units triple honest when anchors are nonzero, which is the generic physical case ($c$ finite and positive). It does not itself force $c=1$ in RS-native units; that normalization lives elsewhere in the constants layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.