def
definition
geometricResidue
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.CouplingLaw on GitHub at line 214.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
211/-! ## §6. The Coupling Law at the Anchor Scale -/
212
213/-- The geometric residue for species f. -/
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