Pith. sign in
module module high

IndisputableMonolith.Geometry.ReggeRemainderClosureAudit

show as:
view Lean formalization →

Audit module that packages the 1B-REM remainder surface: every local analytic remainder target for nonlinear Regge action is discharged from a flat configuration plus standard first- and second-variation jet data. Geometers working the Regge/J-cost bridge cite it as the closed checklist after the cubic Taylor bound and nonlinear correspondence modules. Structure is a thin closure layer re-exporting named closed theorems rather than new analysis.

claimNear a flat configuration, every local analytic remainder target for the nonlinear Regge action is closed: the cubic Taylor remainder of the vertex-potential map is controlled by a third-derivative bound, and the local nonlinear Regge action equals its flat value plus the canonical $J$/Dirichlet quadratic plus a remainder whose jet inputs match the first- and second-variation data.

background

Recognition Gravity already closes a weak-field quadratic bridge between Regge action and $J$-cost. The follow-on nonlinear target is deliberately local: near a flat configuration one does not claim global equality of the full Regge action with a summed $J$-cost action, only that the nonlinear Regge action equals its flat value plus the canonical $J$/Dirichlet quadratic plus controlled higher-order remainder.

The cubic Taylor module isolates the final analytic step after the nonlinear Hessian is identified: a local third-order bound in the finite-dimensional vertex-potential space. The nonlinear correspondence module states that local theorem surface without overclaiming global exactness.

This audit module sits on top of those two imports. Its doc-comment fixes the contract: the 1B-REM proof surface needed downstream is that every local analytic remainder target is closed from a flat configuration plus the standard first- and second-variation remainder jet inputs.

proof idea

Not a definition-only module and not a single deep proof. It is a closure/audit layer: named sibling theorems (remainder analytic closed, canonical remainder-line third-derivative bound closed, nonlinear Regge cubic Taylor theorem closed, local Hessian Taylor inputs closed, $J$-cost local correspondence closed, strongest true Regge/$J$-cost replacement closed) re-export or discharge the remainder obligations already proved in the cubic Taylor bound and nonlinear correspondence modules. Argument structure is checklist assembly from those two imports rather than fresh analytic estimates.

why it matters in Recognition Science

In the Recognition geometry stack this is the bookkeeping gate after the nonlinear Hessian and cubic remainder analysis. Downstream consumers that need a single 1B-REM surface can import the closed flags instead of threading separate cubic-bound and correspondence lemmas. The parent scientific claim is the local nonlinear Regge/$J$-cost correspondence: flat value plus canonical $J$/Dirichlet quadratic plus controlled remainder, not global action equality. No further used-by edges are recorded yet; the module exists so later gravity or continuum-limit theorems can treat remainder closure as a finished local analytic package. Framework link is the geometric side of the Recognition composition law and cost $J$, restricted to the local flat neighborhood where the quadratic bridge already holds.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)