nonlinear_field_curvature_identity
plain-language theorem explainer
Under the nonlinear Regge-J-cost matching hypothesis, the exact J-cost action on a weighted ledger graph equals one over the conversion factor times the Regge sum evaluated on the conformal edge lengths induced by the log-potential. Researchers extending discrete gravity models to strong-field regimes would cite this to justify J-cost stationarity beyond quadratic order. The proof is a short calc block that inserts the hypothesis after field simplification and ring rewriting.
Claim. Assume the nonlinear Regge-J-cost identity holds for a nonlinear deficit functional $D$, scale $a>0$, hinge list, and weighted ledger graph $G$. Then for any log-potential $ε$, the exact J-cost action of $G$ on $ε$ equals $(1/κ)$ times the Regge sum of $D$'s functional on the conformal edge length field from $a$ and $ε$ at the hinges, where $κ$ is the J-cost to Regge conversion factor.
background
This theorem belongs to the Nonlinear J-Cost / Regge Bridge module, which extends the J-cost identification to arbitrary field strengths to address applicability concerns for black-hole physics. The exact J-cost action is the sum over weighted edges of (cosh(Δε) − 1), the full nonlinear expression arising from the J-function; it reduces to the Laplacian action at leading order with a nonnegative quartic remainder from the Taylor series of cosh. The NonlinearDeficitFunctional structure augments a standard deficit-angle functional with the hypothesis that the Regge sum on conformal lengths equals κ times the exact action. Upstream results supply the RS-native gravitational constant G and cost functionals induced by multiplicative recognizers.
proof idea
The tactic proof first obtains that the conversion factor is nonzero. It instantiates the hypothesis at the supplied log-potential ε. A calc block then rewrites the left-hand side by inserting the factor and its reciprocal, applies ring simplification to regroup, and substitutes the hypothesis equality via rewriting.
why it matters
The result is invoked inside nonlinearJCostReggeCert to supply the nonlinear identity clause of the certificate. It directly closes the gap identified in the module documentation for Beltracchi §6 by establishing equivalence of the J-cost and Regge stationarity conditions without a weak-field restriction. In the Recognition Science framework it supports use of the exact J-cost action (derived from J-uniqueness in the forcing chain) on simplicial complexes at all orders, consistent with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.