pith. machine review for the scientific record. sign in
theorem proved tactic proof

electron_strength_gt_100

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  82theorem electron_strength_gt_100 (rg_val : ℝ) (h_rg : rg_val = 0.04942583) :
  83    (100 : ℝ) < electron_strength rg_val := by

proof body

Tactic-mode proof.

  84  unfold electron_strength recognition_strength
  85  -- rewrite rg residue value
  86  rw [h_rg]
  87  have hden_pos : (0 : ℝ) < (0.04942583 : ℝ) := by norm_num
  88  have hnum_gt : (13.953 : ℝ) < geometric_residue Fermion.e := electron_geo_gt_13_953
  89  -- It suffices to show 100 * 0.04942583 < 13.953.
  90  have h100 : (100 : ℝ) * (0.04942583 : ℝ) < (13.953 : ℝ) := by norm_num
  91  have hnum_gt' : (100 : ℝ) * (0.04942583 : ℝ) < geometric_residue Fermion.e :=
  92    lt_trans h100 hnum_gt
  93  -- divide by positive denominator
  94  exact (lt_div_iff₀ hden_pos).2 hnum_gt'
  95
  96/-! ## Structural Dominance -/
  97
  98/-- The "Zero Parameter" hypothesis: The mass is determined by the Geometric Residue,
  99    not the Perturbative Residue. The RG running is a small correction or shadow.
 100
 101    m_i = m_struct * φ^(F(Z))
 102
 103    The standard RG relation m = m_struct * φ^(f_RG) is **REPLACED** by the
 104    stronger geometric lock-in. -/

depends on (20)

Lean names referenced from this declaration's body.