ExperimentalMeasurement
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.