pith. machine review for the scientific record. sign in
def definition def or abbrev high

measurements

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 205def measurements : List ExperimentalMeasurement := [

proof body

Definition body.

 206  ⟨"LEP Z-pole", 0.2312, 0.0002⟩,
 207  ⟨"SLD asymmetries", 0.2310, 0.0002⟩,
 208  ⟨"Average (PDG)", 0.2229, 0.0003⟩
 209]
 210
 211/-! ## Falsification Criteria -/
 212
 213/-- The derivation would be falsified if:
 214    1. No consistent φ-expression matches the observed value
 215    2. Running with energy doesn't follow φ-ladder
 216    3. GUT unification fails -/

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.