Pith. sign in
module module moderate

IndisputableMonolith.Physics.SineSqThetaWFromPhiLadder

show as:
view Lean formalization →

Module packaging the Recognition Science prediction for the weak mixing angle sin²θ_W read from the φ-ladder. Precision electroweak and RS-phenomenology work cites the certified value, band, and PDG proximity lemmas. Content is definitional constants plus a short certificate that the RS figure sits near the measured central value.

claimDefines the RS prediction $\sin^2\theta_W$ on the $\varphi$-ladder, a numerical band around it, the PDG reference value, and a certificate that the RS figure lies near the PDG central value.

background

Recognition Science fixes dimensionless couplings from the unique cost $J(x)=(x+x^{-1})/2-1$ and the self-similar scale $\varphi$ forced at T5–T6. The weak mixing angle $\sin^2\theta_W$ is the electroweak parameter that rotates the neutral gauge fields; RS obtains a definite number by evaluating the appropriate combination of rungs on the $\varphi$-ladder.

The module sits in the physics layer and imports only Mathlib plus Constants (which supplies the RS time quantum $\tau_0$ and the derived $\varphi$-native constants). Sibling declarations expose the raw RS value, a comparison band, the PDG reference, a proximity statement, and a named certificate bundle.

proof idea

Definition-and-certificate module, not a forcing-chain derivation. It records the ladder-evaluated RS number for $\sin^2\theta_W$, stores the PDG central value, and packages a short certificate (SineSqThetaWCert / sineSqThetaWCert) asserting that the RS figure lies inside a stated neighborhood of experiment. No multi-step tactic proof lives here; the arithmetic is inherited from Constants and elementary interval checks.

why it matters in Recognition Science

Gives the concrete RS number for $\sin^2\theta_W$ that any downstream electroweak or precision-test development can quote. The certificate pattern matches other RS coupling certificates (notably the $\alpha^{-1}$ band inside $(137.030,137.039)$). Although the current graph lists no used_by edges, the module closes the phenomenology gap between the abstract $\varphi$-ladder and a laboratory electroweak observable, sitting downstream of T5–T6 uniqueness of $J$ and $\varphi$.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)