exactJCostAction_flat
plain-language theorem explainer
The exact J-cost action on a weighted ledger graph vanishes identically when the log-potential field is the zero function. Researchers extending the J-cost to Regge identification into the strong-field regime would cite this as the flat vacuum base case. The proof is a direct unfolding of the action definition followed by simplification, since every cosh(0) - 1 term is zero.
Claim. For any natural number $n$ and weighted ledger graph $G$ on $n$ vertices, the exact J-cost action defined by $S(G,0) = 0$, where $S(G,ε) = ∑_{i,j} w_{ij} (cosh(ε_i - ε_j) - 1)$.
background
The exact J-cost action is defined in this module as the sum over all pairs of simplices of the edge weight times (cosh of the difference of log-potentials minus one). This expression equals the quadratic Laplacian action at leading order and supplies the exact nonlinear coupling valid at all field strengths. The module addresses Beltracchi's concern that prior J-cost identifications were limited to weak fields by removing that restriction on the J-cost side.
proof idea
The proof is a one-line wrapper that unfolds the definition of exactJCostAction and applies simplification. Every term reduces to cosh(0) - 1 = 0, so the sum is identically zero.
why it matters
This theorem supplies the exact_flat_zero clause inside nonlinearJCostReggeCert. It confirms the nonlinear J-cost action satisfies the flat-space condition needed for the bridge to the Regge action. In the Recognition Science setting it supports the claim that the J-cost side of the identification holds without weak-field assumptions, feeding the decomposition into Laplacian plus non-negative quartic remainder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.