PerturbativeResidue

formal source

 214def geometricResidue (f : Fermion) : ℝ := gap (ZOf f)
 215
 216/-- The perturbative residue packages a positive RG running value. -/
 217structure PerturbativeResidue (f : Fermion) where
 218  value : ℝ
 219  positive : 0 < value
 220
 221/-- Recognition strength: the ratio geometric/perturbative. -/
 222def recognitionStrength {f : Fermion} (pr : PerturbativeResidue f) : ℝ :=
 223  geometricResidue f / pr.value
 224
 225/-- **THE COUPLING LAW**: Recognition strength equals the cosh enhancement
 226evaluated at the perturbative residue.
 227
 228  S_i = F(Z_i) / f_RG_i = coshEnhancement(f_RG_i)
 229
 230The ratio between geometric and perturbative physics is not free — it is
 231determined by the Taylor structure of cosh, forced by the RCL. -/
 232theorem coupling_law_determines_strength {f : Fermion}
 233    (pr : PerturbativeResidue f)
 234    (hlaw : geometricResidue f = coshEnhancement pr.value * pr.value) :
 235    recognitionStrength pr = coshEnhancement pr.value := by
 236  unfold recognitionStrength
 237  rw [hlaw, mul_div_assoc]
 238  simp [ne_of_gt pr.positive]
 239
 240/-- **STRUCTURAL DOMINANCE**: Under the coupling law, geometric always
 241exceeds perturbative for any species with non-vanishing coupling. -/
 242theorem structural_dominance {f : Fermion} (pr : PerturbativeResidue f)
 243    (hlaw : geometricResidue f = coshEnhancement pr.value * pr.value) :
 244    pr.value < geometricResidue f := by
 245  rw [hlaw]
 246  have hS := enhancement_gt_one pr.value (ne_of_gt pr.positive)
 247  have hv := pr.positive