exactJCostAction
plain-language theorem explainer
The exact J-cost action on a weighted ledger graph is the double sum over vertex pairs of edge weight times (cosh of log-potential difference minus one). Researchers extending J-cost gravity into strong-field or black-hole regimes would cite this definition to remove the weak-field restriction. It is introduced as a direct definition matching the Recognition Composition Law, with no approximation or additional lemmas required.
Claim. Let $G$ be a weighted ledger graph on $n$ vertices with non-negative symmetric edge weights $w_{ij}$, and let $ε$ be a log-potential function. The exact J-cost action is defined by $∑_{i,j} w_{ij} (cosh(ε_i - ε_j) - 1)$.
background
This declaration sits in the Nonlinear J-Cost / Regge Bridge module, which directly addresses Beltracchi §6 by supplying a J-cost functional valid at all orders in the potential difference. The module defines the nonlinear coupling via $J(exp(ε_i - ε_j)) = cosh(ε_i - ε_j) - 1$, which follows from the Recognition Composition Law and the J-uniqueness property $J(x) = cosh(log x) - 1$. WeightedLedgerGraph is the structure carrying a non-negative symmetric weight function on Fin n × Fin n; LogPotential is the type of functions Fin n → ℝ that assign log-potentials to vertices. Upstream results supply the constants G and the cost functional from MultiplicativeRecognizerL4 and ObserverForcing, both of which reduce to the same J-cost expression.
proof idea
This is a direct definition that unfolds immediately to the double summation over the graph weights and the cosh expression. No tactics or lemmas are applied inside the body; the definition is the explicit transcription of the Recognition Composition Law into graph language.
why it matters
This definition supplies the nonlinear extension required by the downstream decomposition theorem exact_decomposition, which writes exactJCostAction = laplacian_action + quarticRemainder with the remainder non-negative. It closes the strong-field gap in the J-cost ↔ Regge identification, allowing the framework to treat black-hole regimes without a weak-field assumption. The construction rests on T5 J-uniqueness and the Recognition Composition Law; it feeds the stationarity corollary jcost_stationarity_to_regge_nonlinear and the flat-vacuum agreement theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.