Masses Vevconsistency Sin2 Cos2 Product

The mixing product

The electroweak mixing angle, usually written θ_W, is the angle that rotates the neutral electroweak fields into the photon and the Z boson. Its sine and cosine appear throughout the standard model, and their product sin²θ_W · cos²θ_W is a common combination in formulas for particle masses and couplings. Physicists measure sin²θ_W at accelerator experiments; at the Z pole it is about 0.231, which makes the product about 0.177.

In the Recognition Science framework, the mixing angle is not a free parameter. The framework derives sin²θ_W = (3 − φ)/6, where φ is the golden ratio, approximately 1.618. From that single input, a proved theorem in the machine-checked library of formal theorems establishes the closed form sin²θ_W · cos²θ_W = (8 − φ)/36. The proof is a short algebraic chain: it uses the defining identity φ² = φ + 1 to simplify the product of (3 − φ)/6 and its cosine counterpart (3 + φ)/6. Numerically, (8 − φ)/36 is about 0.1773, which sits inside the narrow band between 0.176 and 0.178 that two further theorems in the same library certify.

This identity matters because it feeds directly into the tree-level formula for the Higgs vacuum expectation value (VEV), the constant that sets the scale of electroweak symmetry breaking. The formula v² = m_Z² · sin²θ_W · cos²θ_W · α⁻¹/π combines the Z mass, the mixing product, the inverse fine-structure constant, and π. With the closed form for the mixing product, the VEV formula becomes algebraically equivalent to an expression involving only the Z mass, the golden ratio, the inverse coupling, and π, with zero free parameters. A further theorem proves this closed form for the VEV squared.

In Recognition Science, this is a structural consistency result: the Higgs VEV is determined by other derived quantities rather than being an independent input. The framework is explicit about what it does not claim. The inverse fine-structure constant α⁻¹ is not derived; it is a boundary datum, and the framework's certified window for it, (137.030, 137.039), is about 429000 times wider than the CODATA 2022 measurement and holds the construction and the measurement at once. The tree-level VEV formula overshoots the measured PDG value by about 2.8 percent, and the framework attributes that gap to the standard QED running of α from zero momentum to the Z pole, a well-established loop calculation in the standard model.

What the reader can take away: the mixing product identity is a proved theorem with a short, checkable derivation, and it shows how a framework-internal constant, the golden ratio, enters a standard electroweak formula. The framework's claim is about algebraic structure and parameter reduction, not about matching every measured number to high precision.

/-- sin²θ_W · cos²θ_W = (8-φ)/36.
    Proof: (3-φ)/6 × (3+φ)/6 = (9-φ²)/36 = (9-(φ+1))/36 = (8-φ)/36. -/
theorem sin2_cos2_product :
    ElectroweakMasses.sin2_theta_W_rs * ElectroweakMasses.cos2_theta_W_rs =
    (8 - phi) / 36 := by
  unfold ElectroweakMasses.cos2_theta_W_rs
  unfold ElectroweakMasses.sin2_theta_W_rs
  have hsq : phi ^ 2 = phi + 1 := phi_sq_eq
  field_simp
  nlinarith [hsq]

/-- sin²θ_W · cos²θ_W = (8-φ)/36.
    Proof: (3-φ)/6 × (3+φ)/6 = (9-φ²)/36 = (9-(φ+1))/36 = (8-φ)/36. -/
theorem sin2_cos2_product :
    ElectroweakMasses.sin2_theta_W_rs * ElectroweakMasses.cos2_theta_W_rs =
    (8 - phi) / 36 := by
  unfold ElectroweakMasses.cos2_theta_W_rs
  unfold ElectroweakMasses.sin2_theta_W_rs
  have hsq : phi ^ 2 = phi + 1 := phi_sq_eq
  field_simp
  nlinarith [hsq]

/-- The product sin²θ_W · cos²θ_W > 0.176.
    (8-φ)/36 > 0.176 ⟺ 8-φ > 6.336 ⟺ φ < 1.664 ✓ -/
theorem sin2_cos2_gt : (0.176 : ℝ) < ElectroweakMasses.sin2_theta_W_rs *
    ElectroweakMasses.cos2_theta_W_rs := by
  rw [sin2_cos2_product]
  have : phi < 1.62 := phi_lt_onePointSixTwo
  linarith

/-- The product sin²θ_W · cos²θ_W < 0.178.
    (8-φ)/36 < 0.178 ⟺ 8-φ < 6.408 ⟺ φ > 1.592 ✓ -/
theorem sin2_cos2_lt : ElectroweakMasses.sin2_theta_W_rs *
    ElectroweakMasses.cos2_theta_W_rs < (0.178 : ℝ) := by
  rw [sin2_cos2_product]
  have : phi > 1.61 := phi_gt_onePointSixOne
  linarith

/-- The VEV formula uses the RS-derived closed form for the mixing product.
    This shows v_tree² is algebraically equivalent to a formula involving
    only (z_pred, φ, αInv, π), with zero free parameters. -/
theorem vev_tree_sq_closed_form :
    vev_tree_sq = ElectroweakMasses.z_pred ^ 2 * ((8 - phi) / 36) *
    alphaInv / Real.pi := by
  unfold vev_tree_sq
  have h := sin2_cos2_product
  -- Left-associativity: z² * sin² * cos² = (z² * sin²) * cos²
  -- Regroup to expose sin² * cos² for substitution
  have hassoc : ElectroweakMasses.z_pred ^ 2 * ElectroweakMasses.sin2_theta_W_rs *
      ElectroweakMasses.cos2_theta_W_rs =
      ElectroweakMasses.z_pred ^ 2 * (ElectroweakMasses.sin2_theta_W_rs *
      ElectroweakMasses.cos2_theta_W_rs) := by ring
  rw [hassoc, h]

What this page does not claim

The inverse fine-structure constant α⁻¹ is not derived by the framework; it is a boundary datum with a certified window. The tree-level VEV formula does not match the measured PDG value; the framework attributes the 2.8 percent gap to standard QED running. The identity does not claim that the measured Weinberg angle equals the golden-ratio expression to experimental precision.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/VEVConsistency.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: