IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound
Packages the exact finite-dimensional cubic Taylor estimate for the canonical nonlinear Regge remainder near a flat configuration. Gravity and discrete-geometry workers cite it when controlling the o(|v|^2) error in the Regge/J-cost bridge. The argument specializes third-order Taylor and line-potential bounds to jet inputs already fixed by the Hessian interface.
claimNear a flat configuration the canonical Regge remainder $R$ admits a third-order Taylor bound: the difference between $R(v)$ and its jet of order two is $O(\|v\|^3)$ on a neighborhood of the origin in the potential space, with explicit control along line potentials $t\mapsto tv$ for $t\in[0,1]$.
background
Recognition Gravity treats the continuum limit of a discrete Regge action on a triangulation. The weak-field quadratic bridge is already closed; the remaining analytic work is a local nonlinear expansion of the full Regge action about a flat potential. The canonical remainder is that nonlinear piece after the flat value and the quadratic (Dirichlet/J-cost) form have been subtracted.
The imported Hessian module isolates the hard second-derivative identity: the second directional derivative of the nonlinear action at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, a standard finite-dimensional Taylor theorem supplies the cubic remainder bound needed for local correspondence.
This module therefore sits between the Hessian calculation and the nonlinear target statement. It does not re-prove the Hessian; it consumes jet regularity and second-derivative data and returns a uniform $O(|v|^3)$ estimate, including elementary comparison lemmas for line potentials on the unit interval.
proof idea
The module is theorem-shaped rather than a pure definition dump. Core objects include a cubic Taylor theorem for the nonlinear Regge remainder, an equivalence between that theorem and a local bound form, and constructors that discharge the theorem from remainder jet inputs or from an identically zero remainder.
Supporting pieces handle smoothness of the canonical remainder at a flat configuration, line-potential normalization and scaling ($t\mapsto tv$), and a norm bound for line potentials with $t\in[0,1]$. The cubic estimate along those rays is packaged as an explicit target, then lifted to a neighborhood statement via the usual one-variable Taylor remainder on each line, combined with continuity of the third derivative (or jet data) at the origin.
why it matters in Recognition Science
The first Recognition Gravity paper closes only the weak-field quadratic bridge between Regge and summed J-cost. The nonlinear correspondence module states the follow-on local target: near a flat configuration the full nonlinear Regge action equals its flat value plus the canonical J/Dirichlet quadratic plus a controlled remainder. This cubic Taylor bound is exactly the analytic input that target needs.
It is also imported by the lane-local Regge remainder closure audit (Track 1B-REM), which wants a buildable certificate for the analytic-remainder branch separate from the finite-Freudenthal combinatorics path. In the broader forcing picture the estimate is geometry-side scaffolding for matching discrete curvature action to the RS cost calculus, not a new forcing step (T0-T8), but a necessary error control once the Hessian identity is available.
scope and limits
- Does not prove the second-derivative/Hessian identity; that lives upstream.
- Does not claim global equality of full Regge action and summed J-cost.
- Does not supply a numerical constant C independent of triangulation data unless jet inputs do.
- Does not address continuum limits or infinite-dimensional function spaces.
- Does not close the full nonlinear correspondence theorem by itself.
used by (2)
depends on (1)
declarations in this module (55)
-
def
NonlinearReggeCubicTaylorTheorem -
def
reggeActionCubicRemainderInput_of_taylorTheorem -
theorem
nonlinearReggeCubicTaylorTheorem_iff_localBound -
theorem
follows -
theorem
nonlinearReggeCubicTaylorTheorem_of_identically_zero -
theorem
canonicalRemainder_contDiffAt_zero_of_flatConfiguration -
def
CanonicalRemainderCubicTaylorFromJetInputsTarget -
theorem
nonlinearReggeCubicTaylorTheorem_of_remainderJetInputs -
theorem
linePotential_one -
theorem
linePotential_eq_smul -
theorem
norm_linePotential_le_of_mem_Icc_zero_one -
def
CanonicalRemainderLineCubicEstimateTarget -
theorem
nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate -
theorem
abs_value_le_cubic_of_taylor_data -
def
CanonicalRemainderLineTaylorDataTarget -
def
CanonicalRemainderLineContDiffTarget -
theorem
canonicalRemainderLineContDiff_of_flatConfiguration -
def
CanonicalRemainderLineQuadraticTaylorZeroTarget -
def
CanonicalRemainderLineThirdDerivBoundTarget -
theorem
min_pos3 -
theorem
lineTaylorData_of_splitTargets -
theorem
lineCubicEstimate_of_lineTaylorData -
theorem
nonlinearReggeCubicTaylorTheorem_of_lineTaylorData -
def
cubicRemainderInput_of_hessian_and_taylor -
structure
NonlinearReggeLocalHessianTaylorInputs -
def
nonlinearReggeLocalHessianTaylorInputs_of_hessian_and_taylor -
def
nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor -
def
nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_remainderJetTarget -
theorem
canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration -
theorem
canonicalRemainderLine_value_at_zero -
theorem
hasDerivAt_linePotential -
theorem
canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar -
theorem
iteratedDerivWithin_zero_canonicalRemainderLine -
theorem
zero_mem_Icc_zero_one -
theorem
iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs -
theorem
iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs -
theorem
canonicalRemainderLineQuadraticTaylorZero_of_jetInputs -
theorem
reggeActionRemainderSecondVariationInput_of_flat_directionalHessian -
theorem
canonicalRemainderLineQuadraticTaylorZero_of_flat_first_and_directionalHessian -
def
lineCLM -
theorem
lineCLM_apply -
theorem
lineCLM_eq_linePotential -
theorem
lineCLM_one -
theorem
canonicalRemainder_line_eq_comp -
def
CanonicalRemainderLineChainRuleBoundTarget -
def
CanonicalRemainderIteratedFDerivLocalBoundTarget -
theorem
canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm -
theorem
canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration -
theorem
canonicalRemainderLineChainRuleBound_of_flatConfiguration -
theorem
canonicalRemainderLineThirdDerivBound_of_flatConfiguration -
theorem
canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm -
theorem
canonicalRemainderLineTaylorData_of_flat_and_remainderJets -
theorem
nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets -
structure
CanonicalRemainderAnalyticClosureCert -
def
canonicalRemainderAnalyticClosureCert