module module high

`IndisputableMonolith.Unification.CouplingLaw`

The Unification.CouplingLaw module defines the cosh enhancement factor S(t) as the exact-to-perturbative ratio of J-cost in logarithmic coordinates. Researchers deriving RS coupling constants or mass ladders beyond quadratic approximations would cite these definitions. The module consists of core definitions for exactCost and perturbativeCost together with elementary lemmas establishing bounds, symmetry, and the identity relating them.

claimThe cosh enhancement factor is given by $S(t) = 2(cosh(t)-1)/t^2$ for $t≠0$, with $S(0):=1$. This equals the ratio of exact J-cost to its quadratic perturbative approximation $J_pert$.

background

The module operates in the Recognition Science setting where the J-cost function J(x) = ½(x + x^{-1}) - 1 is central. In log coordinates this becomes cosh(t) - 1, a convex bowl with minimum at t = 0, as stated in the DiscretenessForcing upstream result. Constants supplies the RS time quantum τ₀ = 1 tick, while RSBridge.Anchor provides the fermion species, ZOf charge index, and gap function F(Z) = ln(1 + Z/φ)/ln(φ) used in mass anchoring.

proof idea

This is a definition module, no proofs. It introduces coshEnhancement, perturbativeCost, exactCost and exactCost_eq, then establishes coupling_identity and the inequalities enhancement_ge_one, enhancement_gt_one, enhancement_at_zero, enhancement_symmetric, enhancement_near_one by direct algebraic verification of the defining expressions.

why it matters in Recognition Science

The module supplies the exact correction factor required to move from perturbative J-cost to the full recognition cost when constructing coupling laws. It feeds the unification machinery that produces the alpha band (137.030, 137.039) and the phi-ladder mass formula. The doc-comment positions S(t) as the universal ratio bridging exact and approximate costs in the forcing chain from T5 onward.

scope and limits

Does not compute numerical values for any coupling constant.
Does not incorporate higher-order loop corrections beyond the cosh factor.
Does not address gravitational or non-Abelian gauge couplings.
Does not derive the eight-tick octave or D = 3 from this enhancement.

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