exactJCostAction_via_Jcost
plain-language theorem explainer
The theorem states that the exact J-cost action on a weighted ledger graph equals the double sum over vertex pairs of the edge weight times the J-cost of the exponential ratio of log-potentials. Researchers extending Recognition Science actions to strong fields cite this to confirm the nonlinear cosh form is defined without weak-field restrictions. The proof is a term-mode reduction that unfolds the action definition, applies sum congruence twice, and rewrites each term via the identity Jcost(ratio) equals cosh of the difference minus one.
Claim. For a weighted ledger graph $G$ on $n$ vertices and log-potential function $ε$, the exact J-cost action equals $∑_{i,j} w_{ij} · J( exp(ε_i − ε_j) )$, where $J(x) = cosh(log x) − 1$.
background
The module defines the nonlinear J-cost coupling between simplices as $J(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1$, valid at all orders in the potential difference. The exact J-cost action is the sum $Σ w_{ij} · (cosh(ε_i − ε_j) − 1)$, which reduces to the quadratic Laplacian action at leading order with a non-negative quartic remainder from the Taylor series of cosh. Upstream results include the cost function induced by multiplicative recognizers and the log-coordinate reparametrization of functionals, which supply the J-cost identity used here.
proof idea
The term proof unfolds exactJCostAction, applies Finset.sum_congr twice to isolate individual edge terms, and rewrites each via the lemma Jcost_ratio_eq_cosh_minus_one that equates Jcost of the ratio to cosh of the difference minus one.
why it matters
This result supplies the exact nonlinear J-cost action, directly answering Beltracchi §6 by showing the J-cost side requires no weak-field assumption and remains well-defined for arbitrary potentials. It positions the quadratic Laplacian action as the leading truncation plus non-negative remainder, supporting the full Recognition Science framework beyond the T5 J-uniqueness and phi-ladder steps. No downstream theorems yet reference it, leaving its use in strong-field Regge comparisons open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.