NonlinearReggeJCostLocalCorrespondence
plain-language theorem explainer
Local cubic-control statement for nonlinear Regge gravity on a 3D triangulation: near the flat (zero) vertex potential, the full Regge action equals its flat value plus the canonical J/Dirichlet quadratic term, up to a remainder bounded by C‖ξ‖³. Gravity and discrete-geometry workers cite it as the precise nonlinear target after the weak-field quadratic bridge. It is a Prop definition, not a proved theorem; discharge routes package Taylor or cubic-bound hypotheses into this surface.
Claim. For an incidence-consistent 3D triangulation $K$, the local nonlinear Regge/J-cost correspondence holds if there exist $r>0$ and $C\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, $\bigl\|S_{\mathrm{Regge}}(K,\xi)-S_{\mathrm{Regge}}(K,0)-Q_J(K,\xi)\bigr\|\le C\|\xi\|^3$, where $Q_J$ is the canonical J/Dirichlet quadratic term.
background
Recognition Gravity's first paper closes the weak-field quadratic bridge between discrete Regge curvature and the Recognition Science J-cost. This module states the follow-on nonlinear target without claiming global exact equality of the full Regge action with a summed weighted J-cost action.
The setting is a 3D triangulation $K$ with incidence consistency. Vertex potentials $\xi$ deform edge lengths (or deficit data) away from a flat reference. The Regge action $S_{\mathrm{Regge}}$ is the usual sum of deficit angles times hinge areas. The canonical J/Dirichlet quadratic term is the second-order jet of that action at the flat configuration; sibling lemmas identify it with the Dirichlet form coming from $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$), the unique cost forced by T5 and the Recognition Composition Law.
The module deliberately keeps the target local and quadratic-core: full nonlinear Regge equals flat value plus that quadratic jet, with an explicitly controlled cubic Taylor remainder.
proof idea
No proof body: this is a Prop-valued definition packaging the local cubic remainder inequality. Downstream theorems discharge it by supplying witnesses $(r,C)$.
Typical route: assume a LocalCubicRemainderBound (or the cubic Taylor theorem, or local Hessian/Taylor inputs, or identically vanishing remainder), unpack the existential, and refine into this Prop. One-line wrappers such as nonlinearRegge_localCorrespondence_of_cubicBound and nonlinearRegge_localCorrespondence_of_taylorTheorem do exactly that. Stronger geometric packages (eventually-zero edge stencil plus mixed-hinge deficit data on a flat configuration) feed the same surface after building the cubic bound.
why it matters
This is the canonical nonlinear theorem surface for Regge/J-cost correspondence in the geometry layer. It feeds StrongestTrueReggeJCostReplacement and the iff linking that replacement to local correspondence, and it is the geometric payload of T5_To_NonlinearReggeJCost_Bridge in the unified forcing chain: T5's uniqueness of $J$ is certified to connect to a controlled nonlinear Regge curvature action, not merely the quadratic weak-field limit.
Framework landmarks: T5 forces $J(x)=\cosh(\log x)-1$; the eight-tick / $D=3$ chain already fixes the spatial triangulation setting. The definition deliberately refuses global equality with the full weighted J-cost action, matching the module's stated open gap after the first Recognition Gravity paper. Closing routes are the cubic-bound and Taylor-input theorems in this same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.