exactJCostAction_nonneg
plain-language theorem explainer
The exact J-cost action on a weighted ledger graph with arbitrary log-potentials is non-negative. Researchers extending the J-cost identification to strong-field Regge calculus cite this to confirm a lower bound that holds without weak-field restrictions. The proof unfolds the double-sum definition and chains non-negativity of edge weights, finite sums, and the inequality cosh(x) ≥ 1.
Claim. For any natural number $n$, weighted ledger graph $G$ on $n$ vertices with non-negative edge weights $w_{ij}$, and log-potential assignment $ε$, the exact J-cost action satisfies $0 ≤ ∑_{i,j} w_{ij} (cosh(ε_i − ε_j) − 1)$.
background
This declaration sits in the Nonlinear J-Cost / Regge Bridge module, which supplies the exact nonlinear primitive needed to address Beltracchi §6. The module defines the nonlinear J-cost coupling between simplices as J(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1, valid at all orders rather than only the quadratic truncation. The exact J-cost action is the corresponding global sum Σ w_{ij} (cosh(ε_i − ε_j) − 1), which reduces to the Laplacian action at leading order. Upstream, the identity J(exp(t)) = cosh(t) − 1 is taken from Cost.Jcost_exp_cosh, while non-negativity of the weights w_{ij} is supplied by the WeightedLedgerGraph structure.
proof idea
The proof unfolds exactJCostAction to a double Finset sum. It applies Finset.sum_nonneg twice, inserts the non-negativity of each edge weight, invokes Real.one_le_cosh to obtain cosh(ε_i − ε_j) ≥ 1, and closes with linarith on the resulting non-negative terms.
why it matters
This result supplies the exact_well_defined clause inside nonlinearJCostReggeCert, the top-level certificate that the nonlinear J-cost side of the Regge identity is well-defined and non-negative for arbitrary field strengths. It directly fills the gap noted in the module doc-comment: the J-cost action requires no weak-field assumption, unlike the geometric Regge side. The theorem therefore anchors the strong-field extension of the Recognition Composition Law and the J-uniqueness fixed point (T5) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.