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. Gravity and discrete-geometry workers cite it when they need a single closed interface rather than the separate cubic-Taylor and J-cost correspondence modules. Structure is a thin closure layer re-exporting already-proved local bounds.

claimNear a flat configuration, every local analytic remainder for the nonlinear Regge action is closed: the cubic Taylor remainder is controlled by a third-derivative bound on the finite-dimensional vertex-potential space, and the nonlinear Regge action equals its flat value plus the canonical $J$/Dirichlet quadratic plus a controlled higher-order jet remainder.

background

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

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 the local Regge/$J$-cost target without overclaiming globally. This audit module sits on top of both and records that the remainder surface required by the 1B-REM program is fully closed from those inputs.

proof idea

Not a free-standing analytic proof. It is a closure/audit layer: it imports the cubic Taylor bound module and the nonlinear Regge/$J$-cost correspondence module, then exposes named closed certificates (remainder analytic closed, canonical remainder third-derivative bound, nonlinear cubic Taylor theorem, local Hessian Taylor inputs, $J$-cost local correspondence, strongest true Regge/$J$-cost replacement). Each certificate is the corresponding upstream theorem specialized to the flat-configuration plus first- and second-variation jet setting demanded downstream.

why it matters in Recognition Science

In the Recognition geometry stack this is the 1B-REM proof surface: the single place that asserts every local analytic remainder target is closed. Downstream consumers that need a clean interface to nonlinear Regge remainders (rather than the separate Taylor-bound and correspondence developments) are meant to import here. It does not advance a new forcing-chain step (T0–T8); it seals the local analytic remainder half of the nonlinear Regge/$J$-cost bridge after the weak-field quadratic bridge is already in place. No further used-by edges are recorded yet, so its role is interface consolidation for later gravity and discrete-action theorems.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)