nonlinearRegge_exact_canonical_split
plain-language theorem explainer
On any incidence-consistent 3D triangulation, the full nonlinear Regge action at a vertex potential equals the flat (zero-potential) value plus the canonical J/Dirichlet quadratic term plus an explicit Taylor remainder. Gravity and discrete-geometry workers cite it when routing J-cost into Regge curvature. The proof is a one-line specialization of the general Regge Taylor decomposition to the canonical Hessian.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation and $\xi$ a real vertex potential on $K$. Then the nonlinear Regge action of $(K,\xi)$ equals the Regge action at the zero potential, plus the canonical J/Dirichlet quadratic term in $\xi$, plus the Taylor remainder of the Regge action relative to the canonical Regge Hessian evaluated at $\xi$.
background
This module states the local nonlinear target that follows the weak-field quadratic bridge in Recognition Gravity. It does not claim global equality between the full Regge action and a summed J-cost action. Near a flat configuration, the nonlinear Regge action is the flat value plus a canonical quadratic jet plus a cubic remainder.
The Regge action is the discrete curvature action on a 3D triangulation with incidence consistency. A vertex potential assigns a real scalar to each vertex; the zero potential is the flat reference. The canonical quadratic term is the second-order jet identified with the J-cost / Dirichlet form (the unique cost forced by the Recognition Composition Law and T5). The remainder is the higher-order part of the Taylor expansion about that Hessian.
Upstream, the general identity is the Regge action Taylor decomposition at an arbitrary Hessian; the present statement fixes that Hessian to the canonical Regge Hessian and names the quadratic piece as the canonical J quadratic term.
proof idea
One-line term proof. Apply the general Regge Taylor decomposition at the canonical Regge Hessian and the given vertex potential, then rewrite the quadratic summand by the definition of the canonical J quadratic term (simpa on that definition). No new estimates or case splits.
why it matters
This identity is the exact algebraic spine of the local nonlinear Regge/J-cost correspondence: full action = flat value + canonical J/Dirichlet quadratic + remainder. Downstream it is consumed by the unified forcing-chain bridge t5_to_nonlinear_regge_jcost_bridge_holds, whose doc-comment states that T5 routes J-cost into the nonlinear Regge curvature-action surface.
In the forcing chain, T5 forces $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The present split makes that unique cost appear as the quadratic jet of discrete gravity, so the nonlinear target is not an extra postulate but a named decomposition of the Regge action. The module explicitly leaves global exact equality open; only the local jet-plus-remainder surface is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.