alpha_W_expanded
plain-language theorem explainer
The theorem equates the weak coupling constant to the fine-structure constant divided by ((3 − φ)/6). Particle physicists deriving electroweak parameters from Recognition Science first principles cite this identity when closing the tree-level relation. The proof is a one-line reflexivity that unfolds the definition of the weak coupling and substitutes the explicit gauge-embedding form for sin²θ_W.
Claim. $α_W = α / ((3 − φ)/6)$, where $α$ is the electromagnetic fine-structure constant and $φ$ is the golden ratio fixed point.
background
The module combines the fine-structure constant $α$ from Constants.Alpha with the weak mixing angle expressed as sin²θ_W = (3 − φ)/6. The latter follows from the gauge embedding (D − φ)/(2D) evaluated at D = 3. The upstream definition sets the weak coupling to $α$ divided by this sin²θ_W expression, while the LawOfExistence structure supplies the abstract bundle of CPM constants and RunningCouplings provides a numeric placeholder for comparison.
proof idea
The proof is a term-mode reflexivity. It applies the definition of the weak coupling as $α$ over sin2_theta_W_rs and substitutes the explicit form sin2_theta_W_rs = (3 − Constants.phi)/6.
why it matters
This identity completes the zero-parameter derivation of the weak coupling from RS primitives and supplies the input for the positivity and bound results in the same module. It realizes the T8 step that fixes D = 3 together with the phi fixed point from T6. The result supports the structural claim that the weak coupling is fully RS-derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.