coupling_law_determines_strength
plain-language theorem explainer
Recognition strength for a fermion equals the cosh enhancement factor at its perturbative residue value once the coupling law equates geometric residue to the product of enhancement and residue. Researchers bridging geometric mass ladders to Standard Model renormalization group running would cite this to fix the unexplained ratio. The proof is a short term-mode reduction that unfolds the strength definition then rewrites and cancels using the given law and positivity.
Claim. Let $f$ be a fermion and $pr$ a perturbative residue for $f$ with positive real value $v$. If the geometric residue satisfies $F(f) = S(v) · v$ where $S$ is the cosh enhancement factor, then the recognition strength of $pr$ equals $S(v)$.
background
The Unification.CouplingLaw module resolves the gap between geometric φ-ladder masses and perturbative SM renormalization. J-cost satisfies J(e^t) = cosh(t) − 1, so exact running uses the full cosh while the perturbative approximation is the quadratic t²/2. The enhancement is S(t) = 2(cosh(t) − 1)/t² for t ≠ 0 (with S(0) = 1), forced by the Recognition Composition Law. PerturbativeResidue packages a positive real value v as the RG residue f_RG. Recognition strength is the ratio of geometric residue to this perturbative value. The upstream coshEnhancement definition supplies S(t) := if t = 0 then 1 else 2*(Real.cosh t − 1)/t².
proof idea
The proof is a short term-mode script. It unfolds recognitionStrength to the quotient geometricResidue f / pr.value. The hypothesis replaces the numerator by coshEnhancement pr.value * pr.value. Multiplication-division associativity rewrites the quotient to coshEnhancement pr.value times (pr.value / pr.value). Simplification cancels the ratio using the positivity hypothesis pr.value > 0.
why it matters
This theorem realizes the coupling law in the module documentation: the ratio between geometric and perturbative physics is fixed by the Taylor structure of cosh, forced by the Recognition Composition Law. It closes the structural dominance claim that geometric always exceeds perturbative for non-vanishing coupling. The result supports the mass formula resolution where geometric residues are O(10) while perturbative values are O(0.1), producing enhancement factors of order 10²–10³. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.