exactCost
plain-language theorem explainer
exactCost defines the exact J-cost in logarithmic coordinates by direct alias to J_log. Researchers bridging geometric phi-ladder masses with perturbative renormalization flows cite this when deriving the universal enhancement factor S(t). The definition is a one-line alias to the upstream J_log implementation.
Claim. The exact J-cost function is defined by exactCost$(t) = J(t)$ for $t$ real, where $J(t) = $cosh$(t) - 1$.
background
The module develops the universal coupling law bridging geometric phi-ladder masses with perturbative Standard Model renormalization. exactCost supplies the precise non-perturbative J-cost in log coordinates, J(e^t) = cosh(t) - 1, a convex bowl minimized at t = 0. This follows the J_log definition from DiscretenessForcing, documented as 'J in log coordinates: J(eᵗ) = cosh(t) - 1. This is a convex bowl centered at t = 0.' A parallel form appears in the ContinuumBridge module.
proof idea
This is a one-line definition that directly aliases the J_log function from the upstream discreteness forcing module.
why it matters
This definition underpins the coupling identity theorem asserting exactCost t = coshEnhancement t * perturbativeCost t for t ≠ 0, and is packaged inside the CouplingLawCert structure. It realizes the J-cost non-perturbative enhancement resolving the residue gap between geometric mass formulas and perturbative running, as described in the module documentation. It connects to the Recognition Composition Law forcing J = cosh - 1 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.