exact_decomposition
plain-language theorem explainer
The exact nonlinear J-cost action on a weighted ledger graph decomposes unconditionally into the quadratic Laplacian action plus a non-negative quartic remainder drawn from the Taylor expansion of cosh. Researchers extending discrete gravity models beyond weak fields cite this result to justify the full J-cost expression without small-potential restrictions. The term-mode proof unfolds the definitions, rescales the quadratic sum, and regroups via sum distributivity and ring to recover the cosh identity.
Claim. Let $G$ be a weighted ledger graph on $n$ vertices with edge weights $w_{ij}$ and let $ε : Fin n → ℝ$ be a log-potential. Then exactJCostAction$(G,ε) = $laplacian_action$(G,ε) + $quarticRemainder$(G,ε)$, where exactJCostAction is $∑_{i,j} w_{ij} (cosh(ε_i - ε_j) - 1)$, laplacian_action is $(1/2) ∑_{i,j} w_{ij} (ε_i - ε_j)^2$, and quarticRemainder is the sum of the higher-order terms $w_{ij} (cosh x - 1 - x^2/2)$ with $x = ε_i - ε_j$.
background
The Nonlinear J-Cost / Regge Bridge module defines the exact J-cost action as $∑ w_{ij} (cosh(ε_i - ε_j) - 1)$, which is the Recognition Science J-function evaluated at the exponential of the log-potential difference. The Laplacian action, defined in ContinuumBridge, supplies the quadratic truncation $(1/2) ∑ w_{ij} (diff)^2$. WeightedLedgerGraph is the structure carrying symmetric non-negative weights that represent the simplicial ledger. The module doc states that this decomposition is unconditional and addresses Beltracchi §6 by showing the J-cost side remains well-defined for arbitrary potentials.
proof idea
The term-mode proof begins by rewriting laplacian_action via its product form, then unfolds exactJCostAction, quarticRemainder and coshRemainder. It applies a targeted rewrite to pull the factor $1/2$ inside the double sum, followed by two applications of Finset.sum_add_distrib and congruences, closing with ring to verify that the quadratic and remainder terms combine exactly into the cosh expression.
why it matters
This theorem supplies the decomposition clause inside nonlinearJCostReggeCert and is invoked by exact_flat_agrees_with_linearized to recover the flat vacuum limit. It directly implements the module's claim that the J-cost action is valid at all orders, supporting the Recognition Science T5 J-uniqueness and the full functional equation without weak-field truncation. The result closes the strong-field gap noted in the module doc while leaving the Regge-side nonlinearity as a separate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.