Physics Weak Mixing Angle3 From Jcost

The weak mixing angle

The weak mixing angle, often written θ_W, is a number that describes how the weak nuclear force and electromagnetism blend together. In the Standard Model of particle physics, the W and Z bosons, the particles that carry the weak force, are not purely weak: each is a mixture of two more basic fields. The angle of that mixture is θ_W, and it predicts the ratio of the W and Z boson masses. The measured value of sin²(θ_W) is about 0.231, a result confirmed by decades of experiments at particle colliders.

A common way to express the angle is through the boson masses: sin²(θ_W) = 1 − (M_W/M_Z)². With the measured masses, this gives approximately 0.223, close to but not exactly the precision value. The angle also appears in the electroweak theory, where it links the coupling strengths of the weak and electromagnetic forces. It is not a free parameter in the deepest sense; the Standard Model predicts its value only after other quantities, like the Higgs boson mass, are fixed.

In Recognition Science, the framework models this angle through its cost function. The module defines domainCost, a cost that measures the price of recognition when one quantity is compared to another, as J(m/e), where J is the framework's forced cost function. The module proves three general facts about this cost: it is zero when the two quantities are equal, it is never negative for positive inputs, and the golden-ratio threshold φ − 3/2 is positive. These are properties of the cost function itself, not of the weak mixing angle.

The module does not derive the measured value 0.231. Its docstring records a research note sketching possible paths from the cost to sin²(θ_W), such as 1 − 1/φ ≈ 0.382, but that number does not match experiment. The Lean code proves nothing specific to the weak mixing angle because the definition of domainCost uses only the ratio m/e without connecting m and e to the boson masses. The module is a template: it establishes the cost's basic behavior, and what would turn it into a theorem about θ_W is a definition of m and e in the electroweak theory's own terms.

What the module does establish, in plain language, is a small set of guaranteed properties for any ratio-based cost in the framework. A reader can rely on the cost being zero at equality and nonnegative everywhere positive. That is a foundation for future work, not a prediction of the measured angle.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The module does not derive or predict the measured value of the weak mixing angle. The module does not connect the cost function to the W and Z boson masses. The research note's sketch of sin²(θ_W) = 1 − 1/φ is not a proved result.

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/Physics/Weak_Mixing_Angle3_FromJCost.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: