NonlinearReggeJCostIdentity
The NonlinearReggeJCostIdentity defines the hypothesis equating the Regge sum on a nonlinear deficit functional, evaluated at conformal edge lengths, to a constant multiple of the exact J-cost action on any log-potential. Physicists extending Regge calculus to strong-field or black-hole regimes cite it to justify the J-cost Dirichlet principle at all orders. The definition is a direct forall statement of the equality, serving as an explicit interface hypothesis for downstream corollaries.
claimLet $D$ be a nonlinear deficit-angle functional, $a>0$, hinges a list of hinge data, and $G$ a weighted ledger graph. The nonlinear Regge-J-cost identity holds when, for every log-potential $ε$, the Regge sum of $D$ applied to the conformal edge-length field at scale $a$ equals $κ$ times the exact J-cost action of $G$ on $ε$, where $κ$ is the jcost-to-regge conversion factor.
background
The module addresses Beltracchi §6 by extending the J-cost/Regge link beyond quadratic order. The nonlinear J-cost action uses $J(exp(ε_i-ε_j))=cosh(ε_i-ε_j)-1$, valid for arbitrary field strengths; exactJCostAction sums weighted instances of this expression and reduces to the Laplacian action at leading order. NonlinearDeficitFunctional is the structure that augments a standard DeficitAngleFunctional with the requirement that its Regge sum match the exact J-cost action (not merely its quadratic truncation). Upstream constants include the RS-native $G=λ_rec^2 c^3/(π ħ)$ and cost functions induced by multiplicative recognizers and observer forcing.
proof idea
The declaration is a definition that directly encodes the forall equality between regge_sum on the nonlinear functional and jcost_to_regge_factor times exactJCostAction. No lemmas or tactics are invoked; it is the hypothesis interface itself.
why it matters in Recognition Science
This supplies the separated hypothesis for the nonlinear bridge, feeding jcost_stationarity_to_regge_nonlinear (which equates stationarity conditions in the strong-field regime) and nonlinear_field_curvature_identity (which states exactJCostAction equals the full Regge sum). It closes the gap between the exact J-cost action (defined for all ε) and Regge equations, directly addressing the framework's need for strong-field validity while leaving the generic simplicial matching as an open interface.
formal statement (Lean)
266def NonlinearReggeJCostIdentity
267 {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
268 (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
proof body
Definition body.
269 ∀ ε : LogPotential n,
270 regge_sum D.functional (conformal_edge_length_field a ha ε) hinges
271 = jcost_to_regge_factor * exactJCostAction G ε
272
273/-- **THEOREM (under hypothesis).** If the non-linear matching
274 identity holds, then the J-cost Dirichlet principle reproduces
275 the Regge equations in the **full non-linear regime**, not just
276 the weak-field one. Stated: `exactJCostAction` is `(1/κ)` times
277 the full Regge sum. -/