SineSqThetaWCert
plain-language theorem explainer
The declaration defines a structure that certifies the Recognition Science prediction for sin²θ_W lies inside (0.228, 0.232) and within 0.005 of the PDG value 0.2312. Electroweak precision tests and BSM model builders would cite the certificate when checking RS-derived constants against data. The definition is a direct structure with two field assertions, one for the numerical band and one for proximity to experiment.
Claim. Let $s = (3 - φ)/6$ where $φ$ is the golden ratio. The structure asserts $0.228 < s < 0.232$ and $|s - 0.2312| < 0.005$.
background
In the Recognition Science module on the Weinberg angle, sin²θ_W is obtained from the (3,2,1) rank decomposition of the gauge couplings as sin²θ_W = g'²/(g² + g'²) with the self-similar correction yielding the closed form (3 - φ)/6. The module states the numerical target 0.230 versus the PDG MS-bar value 0.2312 at the Z pole, claiming 0.4 % agreement. Upstream, sin2thetaW is defined as the noncomputable real (3 - φ)/6 and sin2thetaWPDG as the constant 0.2312; the band field re-uses the arithmetic conjunction pattern from PreLogicalCost to package the interval check.
proof idea
This is a structure definition (def_or_abbrev style) whose body consists solely of the two field declarations. No tactics or lemmas are invoked inside the structure itself; the interval and proximity assertions are left as Prop fields to be populated by the downstream constructor sineSqThetaWCert using the sibling proofs sin2thetaW_band and rs_near_pdg.
why it matters
The structure supplies the certified numerical agreement between the phi-ladder prediction and experiment, feeding directly into the sineSqThetaWCert instance that closes the module. It records the link from T5 J-uniqueness and the eight-tick octave to an electroweak observable, supporting the claim that Standard-Model parameters emerge from the Recognition Composition Law without extra inputs. The declaration touches the open question of whether the same ladder reproduces the full set of gauge couplings and fermion masses to comparable precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.