strongestTrueReggeJCostReplacement_closed
plain-language theorem explainer
On an incidence-consistent 3D triangulation that is flat, the full nonlinear Regge action equals its flat value plus the canonical Dirichlet/J quadratic form, up to a controlled cubic remainder. Geometers and RS auditors cite this as the strongest true local Regge-to-J-cost replacement surface (not global weighted equality). The proof is a one-line alias of the already-closed local correspondence certificate.
Claim. Let $K$ be an incidence-consistent 3D triangulation that admits a flat configuration. Assume the exact second-directional-variation theorem for the nonlinear Regge action at the zero potential, and that the first variation of the nonlinear remainder (relative to the canonical graph-Laplacian Hessian) vanishes at zero. Then the strongest true local replacement holds: the nonlinear Regge action equals its flat value plus the canonical $J$/Dirichlet quadratic term, up to a controlled cubic remainder.
background
This module is the lane-local closure audit for Track 1B-REM analytic remainders. It isolates the remainder branch from the broader Regge closure progress audit so the finite-Freudenthal combinatorics import does not block a buildable certificate.
The target surface is deliberately local and quadratic-core. Upstream, StrongestTrueReggeJCostReplacement is defined to be exactly the nonlinear Regge/$J$-cost local correspondence: full nonlinear Regge action = flat value + canonical $J$/Dirichlet quadratic, with a controlled cubic remainder. It does not claim literal equality with a full weighted $J$-cost action.
Inputs package the analytic hypotheses: a flat configuration; the directional Hessian theorem (second derivative of the action along lines equals the Hessian quadratic of the canonical dual-weight Laplacian at zero); and the named first-variation input that the remainder's Fréchet derivative at the zero potential vanishes. The canonical Hessian is the graph Laplacian from incidence dual weights.
proof idea
One-line term wrapper. The goal is definitionally NonlinearReggeJCostLocalCorrespondence, and the proof applies the already-proved sibling certificate nonlinearReggeJCostLocalCorrespondence_closed at the same triangulation, incidence hypothesis, flat configuration, directional Hessian theorem, and remainder first-variation input. No extra algebra or case split.
why it matters
Closes the strongest true replacement surface in the Regge remainder audit: local quadratic-core correspondence with controlled cubic remainder. That is the honest analytic link between discrete Regge geometry and the RS $J$-cost / Dirichlet quadratic core, without overclaiming global weighted $J$-action equality.
In the Recognition framework this sits on the geometry side of the forcing chain's discrete action story (eight-tick / $D=3$ combinatorics feeding continuum limits). The cubic remainder control is what lets local Taylor analysis stay compatible with the $J$-cost calculus forced by T5 and the Recognition Composition Law. No downstream consumers are wired yet in the graph; the declaration is an end-of-lane audit stamp rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.