pith. sign in
module module high

IndisputableMonolith.Physics.SineSqThetaWFromPhiLadder

show as:
view Lean formalization →

The module supplies the Recognition Science prediction for sin²θ_W derived from the phi-ladder. Physicists comparing RS constants to electroweak measurements would cite it for the native value and its PDG-band certification. It consists of sibling definitions for sin2thetaW, sin2thetaW_band, and the certification object SineSqThetaWCert. No internal theorems are proved; the module simply assembles the expressions and the interval check.

claimDefines the RS-native value of the weak mixing angle squared as sin²θ_W together with its certified band sin²θ_W_band, both obtained from the phi-ladder constants imported from Constants.

background

The module imports IndisputableMonolith.Constants, whose sole documented object is the RS time quantum τ₀ = 1 tick. It therefore operates inside the Recognition Science setting where all dimensionful quantities are expressed in units of this tick and the self-similar fixed point phi. The sibling declarations sin2thetaW, sin2thetaW_band, rs_near_pdg and SineSqThetaWCert introduce the explicit ladder expression for sin²θ_W and the numerical interval that matches the PDG range.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the RS prediction for sin²θ_W that connects the phi-ladder (T5–T8) to the electroweak sector. It feeds the alpha^{-1} band (137.030, 137.039) and the eight-tick octave structure into concrete observable comparisons. Downstream use appears in any calculation that requires the RS-native value of the weak mixing angle.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)