exactCost_eq
plain-language theorem explainer
Exact cost equals cosh of the log coordinate minus one for any real argument. Workers on the geometric-perturbative bridge cite the equality to justify the enhancement factor that resolves large mass residues. The proof is a direct reflexivity that follows from how exactCost is introduced in the module.
Claim. For every real number $t$, the exact cost function satisfies $exactCost(t) = cosh(t) - 1$.
background
The module resolves the gap between geometric φ-ladder residues F(Z) and perturbative f_RG corrections in the mass formula. J-cost obeys the Recognition Composition Law, which forces the closed form J(e^t) = cosh(t) - 1 in logarithmic coordinates; the perturbative approximation truncates to the quadratic term t²/2. Upstream, the identity event from ObserverForcing sits at the J-cost minimum x = 1, while UniversalForcingSelfReference supplies the structural orbit axioms that underwrite the log map.
proof idea
The proof is a term-mode reflexivity that directly unfolds the definition of exactCost to the hyperbolic expression.
why it matters
This equality anchors the coupling law S(t) = 2(cosh(t) - 1)/t² that explains the O(10²–10³) ratios between geometric residues and perturbative running. It feeds the coupling_identity declaration in the same module and aligns with T5 J-uniqueness in the forcing chain. The result closes the exact-versus-approximate gap with no free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.