Jcost_ratio_eq_cosh_minus_one
plain-language theorem explainer
The identity equates the J-cost of the exponential ratio exp(ε_i − ε_j) to cosh(ε_i − ε_j) minus one for any real log-potential difference. Researchers extending the J-cost action beyond quadratic order in simplicial gravity models would cite this result to justify the exact nonlinear action. The proof is a direct one-line application of the upstream lemma Jcost_exp_cosh.
Claim. For all real numbers ε_i and ε_j, Jcost(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1, where Jcost denotes the J-cost function on positive reals.
background
This declaration sits in the Nonlinear J-Cost / Regge Bridge module, which supplies the exact nonlinear coupling J(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1 to address Beltracchi §6 on strong-field validity. The module defines the exact J-cost action as the sum over edges of weights times this Jcost term, reducing to the quadratic Laplacian action at leading order. The upstream lemma Jcost_exp_cosh states: Jcost (Real.exp t) = Real.cosh t - 1, proved via Jlog_as_cosh, and supplies the single-edge building block.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_exp_cosh from the Cost module directly to the difference (εi - εj).
why it matters
This supplies the exact single-edge formula underlying the downstream theorem exactJCostAction_via_Jcost, which rewrites the exact J-cost action as a sum of Jcost contributions. It completes the module's demonstration that the J-cost side remains well-defined for arbitrary ε without weak-field assumptions, instantiating the T5 J-uniqueness property J(x) = cosh(log x) − 1 from the forcing chain. The result supports the decomposition exactJCostAction = laplacian_action + quartic_remainder while leaving the Regge side as a separate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.