nonlinearReggeCubicTaylorTheorem_closed
plain-language theorem explainer
On an incidence-consistent 3D Regge triangulation, flatness plus first- and second-variation jet data for the action remainder yield the full nonlinear cubic Taylor theorem for the Regge action. Geometry and discrete-gravity workers cite it as the closed analytic-remainder endpoint of Track 1B-REM. The proof is a one-line term application of the cubic-Taylor extractor on the closed remainder-analytic certificate.
Claim. Let $K$ be an incidence-consistent 3D Regge triangulation. Assume a flat edge-length configuration, first-variation vanishing input for the action remainder against the canonical Regge Hessian, and second-variation input for that remainder. Then the nonlinear Regge cubic Taylor theorem holds for $K$: the Regge action admits a controlled cubic Taylor expansion about the flat background with remainder bounds as packaged by the cubic-Taylor bound module.
background
This module is a lane-local audit for Track 1B-REM. The broader Regge closure progress audit pulls in finite-Freudenthal combinatorics, so this file isolates the analytic-remainder branch and supplies a buildable closure certificate for that branch alone.
Regge calculus discretizes Einstein–Hilbert gravity on a triangulation by edge lengths and deficit angles. Here $K$ is a 3D triangulation assumed incidence-consistent. A flat configuration means vanishing curvature deficits at the background. The canonical Regge Hessian is the second-variation operator of the Regge action at that background. First- and second-variation inputs for the remainder encode the jet data needed to control the nonlinear remainder after the quadratic Hessian term.
Upstream, the closed analytic-remainder certificate (remainderAnalyticClosed) already packages analytic control of the remainder; its closure projection exposes a cubic-Taylor extractor that consumes flatness and the two jet hypotheses.
proof idea
One-line term proof. Project the global closed analytic-remainder certificate to the given triangulation via its closure map, then apply the method cubic_taylor_from_flat_and_jets, feeding the flat-configuration hypothesis and the first- and second-variation remainder inputs. No additional algebraic work occurs at this site; the theorem is the explicit endpoint packaging of that extractor.
why it matters
This declaration is the explicit theorem-form endpoint for the full cubic Taylor statement in the Regge remainder audit. Downstream, nonlinearReggeLocalHessianTaylorInputs_closed uses it as the direct handoff from the closed analytic-remainder certificate into the local Hessian/Taylor input package consumed by the nonlinear correspondence layer; that parent leaves only non-remainder data (flatness, the nonlinear Hessian theorem, and first-variation vanishing for the canonical remainder).
In the Recognition geometry stack this closes the analytic side of discrete curvature control needed before matching Regge action remainders to J-cost local correspondence (sibling closure theorems in the same audit). It does not itself invoke the forcing chain T0–T8 or the Recognition Composition Law, but it supplies the cubic jet control that later nonlinear Regge–J-cost replacement theorems rely on when linking discrete gravity to the RS cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.