PerturbativeResidue
plain-language theorem explainer
PerturbativeResidue packages a positive real number as the perturbative RG running value for any given fermion species. It is referenced by proofs that equate recognition strength to the cosh enhancement factor evaluated at that value. The declaration is a plain structure definition that enforces positivity on the residue.
Claim. For a fermion $f$, a perturbative residue is a pair consisting of a real number $v$ together with a proof that $v > 0$, where $v$ stands for the perturbative renormalization-group running value of $f$.
background
The Unification.CouplingLaw module resolves the mismatch between large geometric residues $F(Z)$ required by the Recognition Science mass formula and the small perturbative residues $f_{RG}$ obtained from Standard Model running. The module document states that the ratio is explained by the J-cost enhancement $S(t) = 2(cosh(t)-1)/t^2$, which follows from the Recognition Composition Law forcing $J = cosh - 1$ and the eight-tick octave structure. Upstream, Fermion is an inductive type enumerating the species (electron, up, down, etc.) in both the RSBridge.Anchor and SMVerification modules; Spin.value supplies the corresponding half-integer spin as a real number.
proof idea
This is a structure definition that introduces the type PerturbativeResidue f together with the two fields value : ℝ and positive : 0 < value. No lemmas or tactics are applied; the declaration simply bundles the data and the positivity constraint.
why it matters
The structure supplies the perturbative input required by the module's main results: coupling_law_determines_strength (recognition strength equals coshEnhancement evaluated at the residue) and structural_dominance (geometric residue strictly exceeds the perturbative value). It therefore closes the bridge between the φ-ladder geometry and perturbative running that the module document identifies as the central open gap. The definition touches the question of whether the observed O(10²–10³) strength ratios are fully accounted for by the Taylor expansion of cosh.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.