Jcost_ratio_eq_cosh_minus_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish a matching identity for Regge deficit angles on the geometric side.
- Does not bound the truncation error when replacing the exact action by its quadratic Laplacian approximation.
- Does not extend to complex-valued or discrete log-potentials.
- Does not address global topological constraints on closed simplicial complexes.
Lean usage
theorem use_in_action {n : ℕ} (G : WeightedLedgerGraph n) (ε : LogPotential n) (i j : Fin n) : G.weight i j * Jcost (Real.exp (ε i - ε j)) = G.weight i j * (Real.cosh (ε i - ε j) - 1) := by rw [Jcost_ratio_eq_cosh_minus_one]formal statement (Lean)
130theorem Jcost_ratio_eq_cosh_minus_one (εi εj : ℝ) :
131 Jcost (Real.exp (εi - εj)) = Real.cosh (εi - εj) - 1 :=
proof body
Term-mode proof.
132 Cost.Jcost_exp_cosh (εi - εj)
133
134/-- The exact J-cost action is a sum of `Jcost`-valued single-edge
135 contributions — the exact form of what the field-theory
136 `laplacian_action` approximates at leading order. -/