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

sin2ThetaW_error

show as:
view Lean formalization →

The declaration supplies the numerical uncertainty assigned to the Weinberg angle prediction in the Recognition Science model. A researcher working on electroweak precision tests would cite this value when comparing the φ-derived sin²(θ_W) against experimental data. The definition is a direct constant assignment with no further computation.

claimThe uncertainty in the weak mixing angle is defined by the constant value $0.0003$, so that the predicted interval for sin²(θ_W) is taken to have half-width 0.0003.

background

The module derives the Weinberg angle θ_W from the 8-tick phase geometry of Recognition Science, where electroweak mixing corresponds to an embedding of gauge groups constrained by φ optimization. The target value is sin²(θ_W) ≈ 0.2229 at the M_Z scale, which fixes the relative strengths of the electromagnetic and weak forces. The local setting therefore treats the angle as an output of the discrete phase space supplied by the eight-tick octave.

proof idea

The declaration is a direct constant assignment of the real number 0.0003; no lemmas or tactics are invoked.

why it matters in Recognition Science

This definition supplies the tolerance used in sibling comparisons such as bestPrediction and best_prediction_close_to_observed, thereby closing the numerical side of the SM-004 claim that the Weinberg angle emerges from φ-structure. It directly supports the paper proposition on electroweak mixing from information-theoretic principles and anchors the 8-tick geometry landmark (T7) to an observable precision test.

scope and limits

formal statement (Lean)

  42noncomputable def sin2ThetaW_error : ℝ := 0.0003

proof body

Definition body.

  43
  44/-- **THEOREM**: sin²(θ_W) is between 0.22 and 0.23. -/

depends on (5)

Lean names referenced from this declaration's body.