measurements
plain-language theorem explainer
This definition supplies a list of three experimental determinations of sin²θ_W at the Z-pole scale. A physicist comparing Recognition Science electroweak predictions to data would cite it to anchor the φ-derived mixing angle. The body is a direct list literal of ExperimentalMeasurement records with no computation or lemmas.
Claim. The list of experimental measurements for sin²θ_W consists of the LEP Z-pole entry with central value 0.2312 and uncertainty 0.0002, the SLD asymmetries entry with central value 0.2310 and uncertainty 0.0002, and the PDG average entry with central value 0.2229 and uncertainty 0.0003.
background
In the StandardModel.WeinbergAngle module the Weinberg angle is derived from the eight-tick phase geometry of Recognition Science, where electroweak mixing arises as an embedding angle constrained by φ optimization. The ExperimentalMeasurement structure is a record containing a name string, a real central value, and a real uncertainty; the supplied list records the three most precise Z-pole determinations.
proof idea
The definition is a direct list literal of three ExperimentalMeasurement constructors. No upstream lemmas are invoked; the body simply enumerates the named records.
why it matters
This definition supplies the experimental anchor for the SM-004 derivation of θ_W from φ-structure and the eight-tick octave (T7). It is referenced by downstream results including ledger_forces_separation, K_gate_tolerance, cmbAcousticPeakRatiosCert, and rsPredictions, allowing direct numerical comparison between the RS prediction and laboratory data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.