quarticRemainder_nonneg
plain-language theorem explainer
The quartic remainder in the exact J-cost action decomposition is non-negative for any finite weighted ledger graph and log-potential. Researchers extending the J-cost to Regge identification into the strong-field regime would cite this to confirm the nonlinear action remains bounded below by its quadratic truncation. The proof is a direct term-mode argument that unfolds the double-sum definition and applies non-negativity of finite sums together with the product of non-negative weights and the cosh remainder.
Claim. For any natural number $n$, weighted ledger graph $G$, and log-potential $ε$, the quartic remainder satisfies $0 ≤ R_4(G, ε)$, where $R_4$ is the difference exactJCostAction$(G, ε)$ − laplacian_action$(G, ε)$ arising from the Taylor expansion of cosh.
background
The Nonlinear J-Cost / Regge Bridge module defines the exact J-cost action as $∑{i,j} w{ij} (cosh(ε_i − ε_j) − 1)$, which equals the quadratic Laplacian action plus a quartic remainder. The remainder is the sum of weight times the order-four and higher terms in the expansion of cosh(x) − 1 − x²/2. Upstream structures include the J-cost definition from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of; constants such as G appear only indirectly through the graph weights.
proof idea
The term proof unfolds quarticRemainder, then applies Finset.sum_nonneg twice (outer index i, inner index j). The resulting summand is shown non-negative by mul_nonneg applied to G.weight_nonneg i j and coshRemainder_nonneg.
why it matters
This theorem supplies the remainder_nonneg field of nonlinearJCostReggeCert, which certifies that the exact nonlinear J-cost action is well-defined, vanishes on flat configurations, decomposes correctly, and has non-negative remainder. It directly addresses the module's stated goal of removing the weak-field restriction on the J-cost side of the identification, as required for strong-field regimes in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.