jcost_stationarity_to_regge_nonlinear
plain-language theorem explainer
The theorem shows that vanishing of the exact J-cost action on a weighted ledger graph is equivalent to vanishing of the Regge sum on the associated conformal edge lengths, provided the nonlinear matching hypothesis holds. Researchers extending discrete gravity to strong-field regimes would cite it to justify J-cost stationarity for black-hole physics. The tactic proof reduces the biconditional to substitution via the identity and a case split on the product being zero, using the non-vanishing of the conversion factor.
Claim. Let $D$ be a nonlinear deficit-angle functional, $a>0$, hinges a list of hinge data, and $G$ a weighted ledger graph. Assume the nonlinear Regge-J-cost identity holds. Then for any log-potential $ε$, the exact J-cost action of $G$ at $ε$ vanishes if and only if the Regge sum of the functional of $D$ on the conformal edge length field determined by $a$ and $ε$ vanishes.
background
The module addresses Beltracchi's §6 concern that prior J-cost to Regge identifications held only at quadratic order. The exact J-cost action is the sum over weighted edges of (cosh(ε_i − ε_j) − 1), which remains valid at all orders. A NonlinearDeficitFunctional extends DeficitAngleFunctional by satisfying the nonlinear matching identity. The NonlinearReggeJCostIdentity is the hypothesis that equates the Regge sum on conformal lengths to the conversion factor times the exact J-cost action. Upstream results include the non-vanishing of that factor and the exact decomposition of the J-cost action into Laplacian plus quartic remainder.
proof idea
Obtain the non-vanishing of the conversion factor via jcost_to_regge_factor_ne_zero. Instantiate the nonlinear identity at ε to relate the two sides. For the forward direction substitute and simplify by ring. For the converse form the product, apply mul_eq_zero from IntegersFromLogic to obtain a disjunction, and rule out the factor-zero case by contradiction.
why it matters
This corollary supplies the strong-field equivalence of stationarity conditions, completing the nonlinear bridge under the named hypothesis and directly answering the module's §6 separation of weak-field (theorem) from strong-field (hypothesis). It relies on the exact decomposition and quartic non-negativity from sibling results. In the Recognition framework it extends J-uniqueness (T5) and the self-similar fixed point (T6) to full nonlinear discrete gravity on simplicial meshes, with the eight-tick octave and D=3 implicit in the ledger construction. The open question remains discharge of the nonlinear identity via Cayley-Menger determinants or the Cheeger-Müller-Schrader theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.