AnchorsQuot
plain-language theorem explainer
The type of physical anchors identified up to equal induced speed. Anyone proving uniqueness of calibration or transporting units between anchor choices works in this quotient. The declaration is a one-line Lean quotient: `Quot` of the speed setoid on anchors.
Claim. Let anchors be identified when they determine the same speed via the anchor-to-speed map. Write $A/\sim$ for the corresponding quotient type. Then $\mathrm{AnchorsQuot}$ is exactly $A/\sim$.
background
RecogSpec packages the Recognition Science specification layer: dimensionless RS predictions are matched to SI through a small set of anchor data (time and length scales) that fix display units. Sibling maps send an anchor pair to a speed and then to a full units package (fundamental time, length, and $c$).
Two anchors are treated as equivalent when they induce the same speed. That relation is packaged as a setoid; the present declaration is the quotient type of that setoid. Downstream calibration language (calibrated units, unique calibration, band membership) is meant to be insensitive to the choice of representative inside a speed class.
Local module setting is the RecogSpec specification surface: bridges, bands, and two-outcome certificates sit beside the anchor calculus so that display constants can be stated without fixing a privileged SI representative.
proof idea
Pure definitional construction. No proof obligations: the type is declared as the Lean quotient Quot of the speed-equivalence setoid on anchors. All equational reasoning is deferred to the setoid laws and to lemmas about the speed map (equal speed implies related anchors; units extracted from related anchors agree).
why it matters
Calibration uniqueness only makes sense up to the freedom to rescale anchors that leave the induced speed fixed. This quotient is the carrier type for that freedom: statements such as unique calibration and units-from-anchors can be read as living on speed classes rather than on raw anchor pairs.
In the broader RS picture this is bookkeeping for the display bridge, not a forcing-chain step. The forcing landmarks (J-uniqueness, $\varphi$, eight-tick period, $D=3$) fix the dimensionless skeleton; anchors and their quotient fix how that skeleton is painted into SI units ($c$, $\hbar$, $G$, and the $\alpha^{-1}$ band). No downstream theorems currently list this declaration as a direct dependency in the graph, so it is infrastructure for the RecogSpec API rather than a cited lemma in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.