MeasurementProcedure
plain-language theorem explainer
A measurement procedure for a physics framework is a countable sampling map that returns, at each natural-number step, a dimensionless element (knob) of that framework, plus a numeric id for canonical enumeration. Exclusivity and no-alternatives arguments cite it whenever a finitary observation stream is needed. It is a plain two-field structure; the companion predicate is existential range membership of the sample map.
Claim. For a physics framework $F$, a measurement procedure consists of a natural-number identifier together with a map $\mathbb{N}\to\mathrm{Element}(F)$ sending each finite step to a dimensionless element of $F$. An element $e$ is yielded by the procedure when there exists $n\in\mathbb{N}$ such that the sample at $n$ equals $e$.
background
This module holds shared framework definitions used by both the NoAlternatives development and the necessity proofs, so those branches do not import each other circularly.
A physics framework is the minimal interface needed to do physics: a carrier type of states, an evolution map on that carrier, a type of observables, and a measure map from states to observables. Dimensionless elements (knobs) of a framework $F$ package a natural identifier, a concrete state of $F$, and a real value, so later arguments can recover finitary descriptions tied to states.
A measurement procedure sits one layer above elements. It is the formal stand-in for an experimental protocol that, step by step, extracts knobs from the framework.
proof idea
Plain structure definition with two fields: a natural-number identifier and a sample map $\mathbb{N}\to\mathrm{Element}(F)$. The companion predicate (yields) is the existential statement that the target element lies in the image of sample. No lemmas are invoked and there is no proof obligation beyond forming the type.
why it matters
Exclusivity and necessity arguments need a uniform notion of what a framework can actually report. This structure supplies that: a countable protocol of knob extractions, enumerated by a canonical id. Sibling notions in the same module (structural derivations, zero-parameter claims, observable-derivation interfaces, framework isomorphisms, and the alpha-inverse lock) all presuppose some way to name finitary observations; measurement procedures are that naming layer.
In the broader Recognition Science picture, constants such as the forced alpha band and the phi-ladder mass formula are claimed to be read out rather than fitted. Formalizing readout as a countable sample stream is the verification-side counterpart of those forcing claims (T5–T8 and the RCL), even though this declaration itself does not force any constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.