Observable
plain-language theorem explainer
An observable is a real-valued map on RS units that is invariant under anchor rescaling (fixed c). It packages the dimensionless displays that the verification bridge may evaluate. Anyone citing bridge evaluation, K-gate equality, or certified band invariance uses this type. The declaration is a two-field structure: the map plus a proof of dimensionless invariance.
Claim. An observable is a pair $(f, h)$ where $f : \mathrm{RSUnits} \to \mathbb{R}$ and $h$ asserts that $f$ is dimensionless: whenever two unit systems $U, U'$ are related by anchor rescaling with fixed $c$, one has $f(U) = f(U')$.
background
The module supplies the minimal bridge-invariance layer for the certified surface (RS spec and band invariance). It keeps the import closure small: units rescaling, observables, bridge evaluation, and the K-gate bridge equality.
RSUnits is the minimal RS unit record: fundamental time $\tau_0$, length $\ell_0$, speed $c$, with the structural law $c,\tau_0 = \ell_0$. Anchor rescaling (UnitsRescaled) relates two such records while holding $c$ fixed. A numeric display $f$ is dimensionless when it is constant on that relation: $U \sim U' \Rightarrow f(U)=f(U')$.
This structure packages exactly those displays. It is the verification-side counterpart of other "observable" notions in the repo (recognition-forcing value maps, RS-native measurement extractors, quantum observables), specialized to dimensionless bridge-ready displays rather than general state-to-value maps.
proof idea
No proof body: this is a structure definition. The first field is the display map $f : \mathrm{RSUnits}\to\mathbb{R}$. The second field is a term of Dimensionless f, i.e. a proof that $f$ is invariant under every UnitsRescaled pair. Downstream code constructs instances by supplying both the formula and the invariance proof (often via anchor_invariance after BridgeEval).
why it matters
Bridge evaluation and certified K-gate equality only make sense on dimensionless displays; this type is the gatekeeper. Downstream, BridgeEval evaluates such an $f$ under anchors and is invariant by construction; K_gate_bridge and the K-display falsifier sit on top of that. Recognition-forcing results (recognition_necessary, recognition_forcing_complete) and the T4 analytic-recognition refinement in the unified forcing chain consume the same observable language when they treat nontrivial value separation as forcing recognition structure.
In the RS framework this is the certified-surface cut of the display layer: only quantities stable under unit-anchor changes enter the bridge, so band claims (including alpha-band style comparisons elsewhere) cannot smuggle dimensional artifacts. Astrophysics observability limits and PTA structural baselines also reuse the type when they need a dimensionless observable slot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.