exact_flat_agrees_with_linearized
plain-language theorem explainer
When all log-potentials vanish on a weighted ledger graph, the exact nonlinear J-cost action equals the linearized Laplacian action, both zero. Researchers extending the J-cost to Regge correspondence beyond quadratic order cite this as the flat vacuum base case. The proof is a term-mode reduction that rewrites via the exact decomposition and flat Laplacian evaluation, unfolds the quartic and cosh remainders, and simplifies.
Claim. For any weighted ledger graph $G$ on $n$ vertices, the exact J-cost action of $G$ with the zero log-potential function equals the Laplacian action of $G$ with the zero log-potential function.
background
The module defines the nonlinear J-cost action on a simplicial ledger as the sum over weighted edges of $w_{ij} (J(e^{ε_i - ε_j}))$ where $J(x) = cosh(log x) - 1$, valid at all orders in the potential differences $ε$. This reduces to the quadratic Laplacian action at leading order, with the difference given by nonnegative quartic and cosh remainders from the Taylor expansion of cosh. The local setting is the nonlinear bridge addressing Beltracchi §6, which separates the exact J-cost side (no weak-field assumption needed) from the Regge deficit-angle side (still a hypothesis). Upstream results include the exact decomposition identity and the flat evaluation of the Laplacian action.
proof idea
The proof is a one-line wrapper that applies the exact decomposition identity together with the flat Laplacian evaluation lemma, then unfolds the quarticRemainder and coshRemainder definitions and simplifies.
why it matters
This result confirms consistency of the nonlinear J-cost extension in the vacuum limit and supplies the base case for the weak-field J ↔ Regge identity. It supports the module's claim that the J-cost side holds for arbitrary fields while the Regge side remains a separate hypothesis. The declaration sits in the forcing chain after T5 J-uniqueness and before any strong-field extensions, closing the flat case of the nonlinear matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.