exact_decomposition
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish a nonlinear form for the Regge action itself.
- Does not supply explicit magnitude bounds on the remainder beyond non-negativity.
- Does not impose any smallness condition on potential differences.
- Does not invoke specific constants such as G or phi.
Lean usage
rw [exact_decomposition G ε]formal statement (Lean)
210theorem exact_decomposition {n : ℕ} (G : WeightedLedgerGraph n)
211 (ε : LogPotential n) :
212 exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε := by
proof body
Term-mode proof.
213 rw [laplacian_action_prod_form]
214 unfold exactJCostAction quarticRemainder coshRemainder
215 -- Right side: (1/2) Σ Σ w x² + Σ Σ w (cosh - 1 - x²/2)
216 -- = Σ Σ w [x²/2 + cosh - 1 - x²/2]
217 -- = Σ Σ w (cosh - 1) = left side.
218 rw [show (1 : ℝ) / 2 * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
219 = ∑ i : Fin n, ∑ j : Fin n, G.weight i j * ((ε i - ε j) ^ 2 / 2) by
220 rw [Finset.mul_sum]
221 apply Finset.sum_congr rfl
222 intro i _
223 rw [Finset.mul_sum]
224 apply Finset.sum_congr rfl
225 intro j _
226 ring]
227 rw [← Finset.sum_add_distrib]
228 apply Finset.sum_congr rfl
229 intro i _
230 rw [← Finset.sum_add_distrib]
231 apply Finset.sum_congr rfl
232 intro j _
233 ring
234
235/-- **WEAK-FIELD LIMIT.** When every log-potential difference is
236 zero, `exactJCostAction = laplacian_action = 0`. This is the
237 flat vacuum limit. -/