Measurement
plain-language theorem explainer
Measurement is a structure that pairs an arbitrary value of type α with a required protocol, an optional discrete tick-based window, optional uncertainty, and notes. Researchers formalizing RS observables cite it to enforce explicit protocols and prevent hidden windowing choices. The declaration is a direct structure definition with defaults supplied for the optional fields.
Claim. A measurement of value $v : α$ consists of a protocol $P$, an optional window $W$ (start tick $t_0$ and length $len$ in ticks, with $len=0$ instantaneous), optional uncertainty $σ$, and a list of notes $N$.
background
The RS-Native Measurement Framework defines measurements as RS-native using ticks as the base unit with $τ_0=1$. The sibling Window structure supplies a discrete interval via fields $t_0 : ℕ$ (start tick) and $len : ℕ$ (length, zero for instantaneous). Protocols are mandatory so that any coarse-graining or basis choice remains visible rather than implicit. This module is intentionally dependency-light; concrete observables appear in Catalog submodules. Upstream structures such as NucleosynthesisTiers.of supply phi-tier nuclear densities and SpectralEmergence.of supply the gauge and generation content that measurements target.
proof idea
The declaration is a structure definition that directly enumerates the five fields (value, window with default none, protocol, uncertainty with default none, notes with default empty list). No tactics or lemmas are applied; it is a plain inductive type constructor.
why it matters
This structure supplies the core scaffold for all RS measurements and is referenced by forty downstream declarations, including LedgerComputation (explicit observation cost), KGateMeasurement (tau_rec and lambda_kin validation), and w_mass_cdf_measurement (CDF II datum). It directly implements the module goal of making protocols explicit, aligning with the T0-T8 forcing chain and the requirement that arbitrary choices cannot be hidden. It closes the measurement interface used by Constants.KDisplay and Cosmology anomaly comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.