theorem proved term proof

`weak_range_short`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 104theorem weak_range_short : weakRange_fm < 0.01 := by

proof body

Term-mode proof.

 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²). -/

depends on (3)

Lean names referenced from this declaration's body.

wBosonMass_GeV in IndisputableMonolith.Physics.ElectroweakBosons decl_use
hbar_c_GeV_fm in IndisputableMonolith.Physics.WeakForceEmergence decl_use
weakRange_fm in IndisputableMonolith.Physics.WeakForceEmergence decl_use