structural_dominance
plain-language theorem explainer
The structural dominance result states that whenever the coupling law holds, the geometric residue strictly exceeds the perturbative residue for any fermion carrying positive coupling strength. Mass-hierarchy calculations in Recognition Science cite it to confirm that phi-ladder contributions always outrank perturbative running. The proof rewrites the hypothesis and invokes the strict enhancement inequality together with nlinarith on the positivity assumption.
Claim. Let $f$ be a fermion and let $r > 0$ be its perturbative residue. If the geometric residue of $f$ equals the product of the cosh enhancement evaluated at $r$ and $r$, then $r$ is strictly smaller than the geometric residue.
background
The module establishes the universal coupling law that bridges the geometric phi-ladder side of Recognition Science with perturbative renormalization-group running in the Standard Model. The perturbative residue is the structure that packages a positive real RG-running value for a given fermion species. The geometric residue is the exact non-perturbative quantity obtained from the J-cost function, where J(e^t) = cosh(t) - 1 and the enhancement factor S(t) = 2(cosh(t) - 1)/t^2 satisfies S(t) > 1 for all t ≠ 0.
proof idea
The term proof first rewrites the equality hypothesis to substitute the product expression. It then applies the sibling lemma enhancement_gt_one to the positive value, obtaining the strict inequality S(r) > 1. The final nlinarith step combines this inequality with the positivity hypothesis to conclude the desired strict dominance.
why it matters
The declaration supplies the key dominance step required by the coupling-law certificate in the same module. It directly realizes the second key property listed in the module documentation: geometric running always dominates perturbative running for nonzero coupling. Within the Recognition Science chain this closes the gap between the phi-ladder mass formula and Standard-Model residues, confirming that the O(10^2–10^3) ratios arise solely from J-cost enhancement without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.