exactJCostAction_flat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish non-negativity of the action for nonzero potentials.
- Does not address the Regge deficit-angle side of the identification.
- Does not invoke specific values of G, phi, or other constants.
- Applies only to the zero function, not to general or perturbed fields.
formal statement (Lean)
104theorem exactJCostAction_flat {n : ℕ} (G : WeightedLedgerGraph n) :
105 exactJCostAction G (fun _ => (0 : ℝ)) = 0 := by
proof body
Term-mode proof.
106 unfold exactJCostAction
107 simp
108
109/-- The exact J-cost action is non-negative. -/