module module high

`IndisputableMonolith.Unification.CouplingLaw`

The Unification.CouplingLaw module defines the cosh enhancement factor S(t) that converts between exact J-cost and its quadratic perturbative approximation. Mass and unification calculations cite its exactCost and coupling_identity results. The module supplies a collection of definitions and elementary inequalities for S(t) derived from the imported convexity properties of cosh.

claim$S(t) = \frac{2(\cosh t - 1)}{t^2}$ for $t \neq 0$, with $S(0) = 1$, equals the ratio of exact J-cost to perturbative J-cost.

background

Recognition Science starts from the J-cost J(x) = (x + x^{-1})/2 - 1. In logarithmic coordinates this becomes cosh(t) - 1, a convex bowl with minimum at t = 0, as stated in the DiscretenessForcing module.

Constants supplies the RS time quantum τ₀ = 1 tick. RSBridge.Anchor supplies the Z-map and gap function that later convert the cost ratio into mass values on the phi-ladder.

The CouplingLaw module isolates the universal ratio S(t) between the exact cost 2(cosh(t) - 1) and the perturbative t²/2 approximation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the exact-to-perturbative correction required by the coupling law in the unification chain. It feeds the enhancement bounds and identities used by downstream mass and alpha calculations that connect the J-cost landscape to the observed particle spectrum.

scope and limits

Does not derive the numerical value of alpha.
Does not compute explicit particle masses.
Does not address corrections beyond the quadratic term.
Does not prove uniqueness of the J minimum.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Masses.RSBridge.Anchor module_import

declarations in this module (20)

def coshEnhancement L59
def perturbativeCost L63
def exactCost L66
theorem exactCost_eq L68
theorem coupling_identity L72
theorem cosh_ge_one_plus_half_sq L90
theorem cosh_gt_one_plus_half_sq L113
theorem enhancement_ge_one L134
theorem enhancement_gt_one L142
theorem enhancement_at_zero L148
theorem enhancement_symmetric L152
theorem enhancement_near_one L160
theorem enhancement_unbounded L183
def geometricResidue L214
structure PerturbativeResidue L217
def recognitionStrength L222
theorem coupling_law_determines_strength L232
theorem structural_dominance L242
structure CouplingLawCert L253
theorem coupling_law_cert L265