Element
plain-language theorem explainer
A dimensionless knob of a physics framework: a natural-number id, a state in the framework's state space, and a real value. Downstream exclusivity and measurement arguments cite it to attach finitary encodings to concrete states. Pure structure definition; no proof obligations.
Claim. For a physics framework $F$ (state space, evolution, observables, measurement), an element is a triple $(n, s, v)$ with $n \in \mathbb{N}$ an identifier for finitary encodings, $s$ a state in $F$'s state space, and $v \in \mathbb{R}$ the associated numerical value (a dimensionless knob).
background
The module supplies shared core definitions for NoAlternatives and necessity proofs, avoiding circular imports. A physics framework is the minimal interface to "do physics": a state space, an evolution map, an observable type, and a measure map from states to observables.
Elements are the dimensionless knobs that framework carries. By convention each knob is a real together with a state witness, so later arguments can recover a finitary description tied to a concrete state rather than a free-floating parameter.
The natural-number id is the handle used for algorithmic or enumeration-based encodings; the state field pins the knob to $F$'s dynamics; the value is the measured real.
proof idea
No proof: this is a structure declaration (three fields). Inhabitants are constructed by supplying id, state, and value. Downstream, MeasurementProcedure packages a step-indexed family of such elements.
why it matters
Elements are the atomic observations that measurement procedures sample. MeasurementProcedure is a natural id plus a map $\mathbb{N} \to$ Element $F$, enabling canonical enumeration and the predicate that a procedure yields a knob.
That interface feeds exclusivity and zero-parameter arguments in the verification layer: frameworks are compared by what dimensionless elements they can produce, not by informal narrative. Chemistry and Standard Model modules that touch period structure, affinities, or CKM unitarity sit further downstream of the same shared framework vocabulary, even when they do not construct Element values directly.
In the Recognition setting this keeps "parameters" as state-tied reals rather than free floats, which is the right shape for later claims that a framework has zero free parameters or derives its observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.