Pith. sign in
module module high

IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound

show as:
view Lean formalization →

Exact third-order Taylor control for the canonical nonlinear Regge remainder near a flat configuration. Finite-dimensional cubic remainder estimates specialize the classical Taylor theorem to the Regge action's defect from its flat value. Downstream nonlinear correspondence and remainder-closure audits cite this bound. The module packages the estimate as a theorem surface fed by jet and Hessian inputs rather than a fresh calculation.

claimNear a flat Regge configuration, the canonical remainder $R$ of the nonlinear Regge action admits a third-order Taylor estimate: $R(0)=0$, $DR(0)=0$, and $|R(v)-\tfrac12 D^2R(0)(v,v)|\le C\|v\|^3$ for small $v$, with the quadratic term identified with the canonical incidence Hessian. Equivalent forms package the same bound via jet inputs, line-potential restrictions, and identically-zero remainder cases.

background

Recognition Gravity bridges discrete Regge calculus to the continuum J-cost action. The first paper closes the weak-field quadratic bridge; the nonlinear follow-on asks only for a local expansion near flat configurations, not global equality of the full Regge action with a summed J-cost.

The upstream Hessian module isolates the hard second-derivative identity: the second directional derivative of the nonlinear Regge action at the flat potential must equal the canonical incidence Hessian. That identity is the endpoint of a chain-rule calculation, not a new physical assumption.

This module supplies the next analytic ingredient: a finite-dimensional cubic Taylor theorem specialized to the canonical Regge remainder. Sibling surfaces include jet-input forms, line-potential cubic estimates along segments in the unit interval, and reduction lemmas that recover the bound when the remainder vanishes identically or when flat-configuration smoothness holds at zero.

proof idea

The module is a theorem-interface layer, not a single monolithic proof. Core objects state the cubic Taylor theorem for the nonlinear Regge remainder and equivalent local-bound formulations. Reduction lemmas show the theorem follows from remainder jet inputs, from identically-zero remainder, or from contDiff-at-zero of the canonical remainder on a flat configuration. Line-potential lemmas bound the restriction of the remainder along rays (norm control on $[0,1]$, scaling identities) and feed a dedicated cubic estimate target on those lines. Overall structure: package classical third-order Taylor control in the exact shape the nonlinear correspondence needs, with the Hessian identity imported from upstream.

why it matters in Recognition Science

The nonlinear Regge/J-cost correspondence target needs a local expansion: near flat configurations the full nonlinear Regge action equals its flat value plus the canonical J/Dirichlet quadratic form plus a controlled cubic remainder. This module is that remainder bound.

It is imported by the nonlinear correspondence module (local equality target without claiming global exactness) and by the Regge remainder closure audit (lane-local Track 1B-REM certificate for the analytic-remainder branch, kept separate from finite-Freudenthal combinatorics). Together with the upstream Hessian identity, it closes the analytic half of the weak-to-nonlinear bridge in the geometry layer of Recognition Science.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (55)