correctedPrediction
plain-language theorem explainer
correctedPrediction supplies a phi-adjusted numerical value for the Weinberg angle in the Recognition Science derivation of electroweak mixing. Researchers comparing RS predictions to experimental sin²θ_W data at the Z-pole would reference this expression. The definition evaluates a simple algebraic combination of the constant one-quarter and the phiCorrection term imported from the same module.
Claim. The corrected prediction is given by $1/4(1 - phiCorrection)$, where $phiCorrection$ denotes the adjustment term arising from the eight-tick phase geometry in Recognition Science.
background
The module StandardModel.WeinbergAngle derives the weak mixing angle θ_W from the φ-structure of Recognition Science, targeting sin²(θ_W) ≈ 0.2229 at the M_Z scale via 8-tick phase geometry that constrains gauge group embeddings. The module documentation states that RS explains both the GUT-scale value 3/8 and the running to approximately 0.23. Upstream results include the scale definition scale(k) := φ^k from Cosmology.LargeScaleStructureFromRS, which supplies the phi-powered scaling, and the theorem from in PrimitiveDistinction that reduces seven axioms to four structural conditions plus three definitional facts.
proof idea
The declaration is a one-line definition that directly constructs the corrected prediction by scaling the difference (1 - phiCorrection) by one quarter. It applies the phiCorrection term, which itself encodes the RS adjustment from the eight-tick geometry, without further tactic steps or lemma applications beyond the imported definition.
why it matters
This definition completes the numerical output for the Weinberg angle prediction in the SM-004 module, feeding the GUT connection where sin²(θ_W) runs from 3/8 at 10¹⁶ GeV to approximately 0.23 at M_Z. It realizes the framework landmark of the eight-tick octave (T7) by embedding the mixing angle in discrete phase space. The parent structure is the overall derivation of electroweak mixing from information-theoretic principles outlined in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.