nonlinearJCostReggeCert
plain-language theorem explainer
The nonlinear J-cost Regge certificate bundles non-negativity of the exact J-cost action for arbitrary log-potentials, its vanishing on the flat vacuum, its decomposition into Laplacian action plus non-negative quartic remainder, and the nonlinear field curvature identity under the listed hypotheses. Strong-field Regge-calculus workers cite it to justify J-cost beyond weak-field order. The proof is a term-mode construction that directly supplies the five fields from the supporting lemmas exactJCostAction_nonneg, exactJCostAction_flat, exact_de,
Claim. Let $G$ be a weighted ledger graph on $n$ vertices and let $ε$ be a log-potential. The exact J-cost action $∑_{i,j} w_{ij}(cosh(ε_i−ε_j)−1)$ is non-negative for all $ε$, equals zero when $ε≡0$, equals the Laplacian action plus a non-negative quartic remainder, and the nonlinear field-curvature identity holds whenever the dimension, area, hinge, and nonlinear hypotheses are satisfied.
background
A SimplicialLedger is a non-empty collection of 3-simplices that cover a manifold (scaffold). The exact J-cost action on a weighted ledger graph $G$ with log-potential $ε$ is defined as $∑{i,j} w{ij}(cosh(ε_i−ε_j)−1)$, which equals the quadratic Laplacian action plus the quartic remainder $∑{i,j} w{ij}(cosh(x)−1−x^2/2)$ where $x=ε_i−ε_j$. The module works in the setting of the Recognition Science forcing chain (T5 J-uniqueness, T6 phi fixed point) and supplies the strong-field side of the J-cost ↔ Regge identification requested by Beltracchi §6.
proof idea
Term-mode construction of the NonlinearJCostReggeCert structure. The five fields are filled by direct application of the sibling lemmas: exact_well_defined uses exactJCostAction_nonneg, exact_flat_zero uses exactJCostAction_flat, decomposition uses exact_decomposition, remainder_nonneg uses quarticRemainder_nonneg, and nonlinear_identity_under_hypothesis uses nonlinear_field_curvature_identity.
why it matters
This proved certificate supplies the J-cost half of the nonlinear bridge, removing the weak-field restriction that previously blocked black-hole applications. It rests on the unconditional decomposition theorem and the non-negativity of the cosh remainder. In the Recognition framework it extends the J-cost action past quadratic order while leaving the Regge-side nonlinear identity as a separate hypothesis. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.