speedFromAnchors
plain-language theorem explainer
Extracts the canonical calibration speed from a pair of measurement anchors: the ratio of the length anchor to the time anchor, or zero when the time anchor vanishes. Anyone working on RS unit packs, band checks, or uniqueness-up-to-units cites this as the speed witness. The body is a one-line conditional definition.
Claim. Given measurement anchors $(a_1, a_2)$ (time and length scales, with the consistency rule that $a_1 = 0$ forces $a_2 = 0$), the canonical speed is $0$ if $a_1 = 0$, and $a_2 / a_1$ otherwise.
background
In RecogSpec, physical calibration is packaged as a pair of real anchors: a time scale $a_1$ and a length scale $a_2$. The structure carries a consistency hypothesis: if the time anchor vanishes, the length anchor must vanish too, so that a speed $c$ with $c \cdot \tau_0 = \ell_0$ remains solvable.
Recognition Science works in RS-native units where $c$ is fixed by calibration rather than postulated. The speed extracted from anchors is the ratio that will be identified with the units-pack field $c$ when a bridge is declared calibrated. Upstream, Anchors is the minimal interface used by band checks; sibling definitions build units packs and equivalence from this ratio.
The local module sets the specification layer: anchors, calibration witnesses, band acceptance, and the quotient of anchors by equal induced speed.
proof idea
Pure definition, not a proved theorem. Branch on whether the time anchor equals zero: return $0$ in the degenerate case, otherwise return the quotient of the length anchor by the time anchor. No lemmas are applied; the consistency field on anchors is not invoked inside the definition itself (it is used by downstream uniqueness and calibration lemmas).
why it matters
This ratio is the single scalar that turns a raw anchor pair into a physical speed. Downstream, calibration is defined by matching $\tau_0$, $\ell_0$, and $c$ to the anchors with $c$ equal to this value. Equivalence of anchors is literally equality of the induced speeds, and the quotient type of anchors is built on that relation.
Uniqueness-up-to-units theorems for bridges calibrated from the same ledger reduce to equality of these speeds. Band-meeting witnesses and calibrated unit packs all thread through this definition. In the broader RS picture it is the operational stand-in for $c = 1$ in native units once anchors are fixed, feeding the display-layer constants and band checks rather than the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.