ExperimentalMeasurement
This structure packages an experimental datum for the Weinberg angle as a named triple of string identifier, central value, and uncertainty. Electroweak precision physicists cite it when tabulating LEP, SLD, and PDG results for comparison against Recognition Science predictions. The definition is a direct record constructor with no computational reduction or lemmas.
claimAn experimental measurement consists of a string label, a real number $v$ for the observed value of the Weinberg angle, and a real number $e$ for its reported uncertainty.
background
The module derives the weak mixing angle from the eight-tick phase geometry of Recognition Science, where electroweak mixing arises as an embedding constrained by phi optimization. The structure ExperimentalMeasurement supplies the data carrier that holds tabulated observations for direct comparison with the RS-native prediction sin²(theta_W) approx 0.2229 at the M_Z scale. Upstream, the SpinStatistics.value definition supplies the actual spin as a real number obtained by dividing twice the spin label by 2.
proof idea
This is a plain structure definition that introduces the record type with three fields. No lemmas or tactics are invoked; the declaration is a direct inductive data constructor.
why it matters in Recognition Science
It supplies the typed container used by the measurements list that aggregates LEP Z-pole, SLD, and PDG values for benchmarking the RS-derived Weinberg angle. The declaration supports the paper proposition on electroweak mixing from information-theoretic principles and connects to the eight-tick octave (T7) and phi-ladder mass formula in the forcing chain.
scope and limits
- Does not compute or predict any value of sin²(theta_W).
- Does not incorporate running of the angle with energy scale.
- Does not validate measurements against theory or RS constants.
- Does not specify normalization or units beyond the real numbers.
formal statement (Lean)
200structure ExperimentalMeasurement where
201 name : String
202 value : ℝ
203 error : ℝ
204