NonlinearDeficitFunctional
plain-language theorem explainer
NonlinearDeficitFunctional n is a wrapper structure around DeficitAngleFunctional n, marking it for use with the full nonlinear J-cost to Regge matching. Researchers extending the J-cost action beyond quadratic order cite it when separating exact cosh couplings from Laplacian approximations. The declaration is a direct structure definition containing only the functional field.
Claim. A nonlinear deficit-angle functional on $n$ vertices is a DeficitAngleFunctional $n$ (a map sending edge-length fields to hinge deficits and areas) intended to satisfy the identity that the Regge sum equals $jcost_to_regge_factor$ times the exact J-cost action $exactJCostAction G ε = ∑_{i,j} w_{ij} (cosh(ε_i - ε_j) - 1)$.
background
The module establishes the nonlinear J-cost / Regge bridge to address Beltracchi §6: the quadratic identification holds only at weak field, so black-hole regimes require the full cosh form. The nonlinear J-cost coupling is $J(exp(ε_i - ε_j)) = cosh(ε_i - ε_j) - 1$, valid at all orders. exactJCostAction G ε is defined as the double sum over weights of (cosh difference minus one); it reduces to laplacian_action at leading order, with the difference given by a nonnegative quartic remainder from the cosh Taylor series. DeficitAngleFunctional n is the upstream structure supplying a deficit map and an area map (with area_pos) from EdgeLengthField n and HingeDatum n; its concrete realization is left open for Cayley-Menger or 3+1 implementations. The present definition simply packages one such functional for use under the separate NonlinearReggeJCostIdentity hypothesis.
proof idea
The declaration is a direct structure definition with a single field of type DeficitAngleFunctional n. No lemmas or tactics are invoked; the structure serves as a type-level marker that downstream statements can quantify over when imposing the nonlinear matching hypothesis.
why it matters
It supplies the type used by nonlinear_field_curvature_identity (which states that exactJCostAction equals (1/κ) times the full Regge sum under the hypothesis) and by jcost_stationarity_to_regge_nonlinear (which transfers stationarity from the exact action to the Regge equations). The definition therefore closes the module's separation of the exact nonlinear action from its quadratic truncation, directly supporting the Recognition Composition Law via the cosh expression. It touches the remaining open question whether the nonlinear identity holds for arbitrary simplicial complexes without additional geometric constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.