def
definition
recognition_strength
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.RecognitionCoupling on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
58
59/-- The Recognition Strength for species f: the factor by which the geometric
60 structure exceeds the perturbative RG effect. -/
61def recognition_strength (f : Fermion) (rg_val : ℝ) : ℝ :=
62 geometric_residue f / rg_val
63
64/-! ## The Electron Case -/
65
66/-- For the electron, the perturbative residue is approx 0.0494. -/
67def electron_rg_val_hypothesis : Prop :=
68 -- Predicate for the specific electron value.
69 True
70
71/-- The derived recognition strength for the electron. -/
72def electron_strength (rg_val : ℝ) : ℝ := recognition_strength Fermion.e rg_val
73
74/-- Lower bound on the geometric residue for the electron (from the proven gap bounds). -/
75theorem electron_geo_gt_13_953 : (13.953 : ℝ) < geometric_residue Fermion.e := by
76 -- ZOf e = 1332, so this is exactly the lower bound on gap(1332).
77 have hZ : ZOf Fermion.e = 1332 := by native_decide
78 simpa [geometric_residue, hZ] using (gap_1332_bounds).1
79
80/-- A basic (non-universal) strength statement: if `rg_val = 0.04942583`,
81then the ratio `F(Z)/f_RG` is certainly > 100 for the electron. -/
82theorem electron_strength_gt_100 (rg_val : ℝ) (h_rg : rg_val = 0.04942583) :
83 (100 : ℝ) < electron_strength rg_val := by
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 :=