`parity_violation`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.WeakForceEmergence
domain: Physics
line: 84 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 84.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  81def rightHandedCouples : Bool := false
  82
  83/-- Parity violation: L ≠ R. -/
  84theorem parity_violation : leftHandedCouples ≠ rightHandedCouples := by
  85  decide
  86
  87/-! ## Weak Isospin Doublets -/
  88
  89/-- Lepton doublet: (νe, e⁻). -/
  90def leptonDoublet : ℕ := 2
  91
  92/-- Quark doublet: (u, d). -/
  93def quarkDoublet : ℕ := 2
  94
  95/-- Each generation has 2 isospin doublets. -/
  96def doubletsPerGeneration : ℕ := 2
  97
  98/-- Total doublets for 3 generations. -/
  99def totalDoublets : ℕ := 3 * doubletsPerGeneration
 100
 101/-! ## Range and Strength -/
 102
 103/-- Weak interaction range is ~10⁻³ fm. -/
 104theorem weak_range_short : weakRange_fm < 0.01 := by
 105  -- 0.197327 / 80.3692 ≈ 0.00245 fm < 0.01
 106  simp only [weakRange_fm, hbar_c_GeV_fm, wBosonMass_GeV]
 107  norm_num
 108
 109/-- G_F relation: G_F / (ℏc)³ = √2 g² / (8 m_W²). -/
 110def gf_from_mw : ℝ := sqrt 2 * (weak_coupling_g)^2 / (8 * wBosonMass_GeV^2)
 111
 112/-- G_F matches the derived value (approximate, within 10%).
 113    The derivation is: G_F = sqrt(2) * g² / (8 * mW²) where g = 2*mW/v.
 114    Simplifying: G_F = sqrt(2) / (2 * v²).

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.