best_prediction_close_to_observed
plain-language theorem explainer
The theorem shows that the RS geometric prediction (3 - φ)/6 for sin²θ_W lies within 0.01 of the measured value 0.2229 when 1.61 < φ < 1.62. Electroweak phenomenologists and unification modelers would cite it to connect 8-tick phase geometry to the observed mixing parameter. The tactic proof unfolds the definitions, invokes the two phi bounding lemmas, derives the prediction interval by linarith, and closes the absolute-value inequality with rw [abs_lt] and constructor.
Claim. $|(3 - φ)/6 - 0.2229| < 0.01$, where φ is the golden ratio.
background
The StandardModel.WeinbergAngle module derives the weak mixing angle from RS φ-structure via 8-tick phase geometry. The 8-tick circle supplies discrete phases at kπ/4; electroweak mixing arises from embedding SU(2) and U(1) such that the angle is fixed by φ optimization. The module imports Constants for the golden-ratio bounds and RSNativeUnits for the fundamental tick. Upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the interval 1.61 < φ < 1.62 that pins the prediction.
proof idea
The proof unfolds bestPrediction, prediction3 and sin2ThetaW_observed to reach |(3 - φ)/6 - 0.2229|. It obtains 1.61 < φ < 1.62 from phi_gt_onePointSixOne and phi_lt_onePointSixTwo, then applies linarith twice to bound the prediction between 0.23 and 0.232. The final steps rewrite the absolute value via rw [abs_lt], split with constructor, and discharge both inequalities by linarith.
why it matters
This result supplies the numerical match required by the downstream theorem row_best_prediction_match in Physics.WeinbergAngleScoreCard. It realizes the SM-004 target stated in the module documentation, linking the prediction to the eight-tick octave (T7) and φ fixed point (T6) of the UnifiedForcingChain. The theorem advances the PRL claim on electroweak mixing from information-theoretic principles while leaving open the derivation of the φ interval without external bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.