Geometry Regge Action Cubic Taylor Bound

The cubic Taylor bound

In numerical approaches to gravity, one often approximates curved spacetime by a patchwork of flat pieces, called a triangulation. The Regge action is the standard way to assign a cost to such a discrete geometry, and its second derivative, the Hessian, describes how that cost responds to small movements of the vertices. The question addressed here is how much error remains after you subtract the first two terms of a Taylor expansion of that action around a flat configuration. The answer, proved in the machine-checked library of formal theorems, is that the error is bounded by a constant times the cube of the perturbation size, for sufficiently small perturbations. This is the cubic Taylor bound.

The theorem's statement is precise. For a three-dimensional triangulation with a consistent incidence structure, and a flat configuration, there exists a positive radius and a nonnegative constant such that for any vertex potential (a small displacement of the vertices) with norm less than that radius, the norm of the remainder of the Regge action, after subtracting the Hessian term, is at most that constant times the cube of the norm of the potential. In symbols, the remainder is O(||ξ||³). The proof works by restricting attention to a line through the origin in the space of vertex potentials, applying the standard one-dimensional Taylor theorem with a third-order remainder, and then lifting the result back to the full space.

The proof is not a single step but a chain of intermediate results, each itself a formal theorem. It first establishes that the remainder, restricted to a line, is three times continuously differentiable near the origin. It then shows that the first two Taylor coefficients vanish, which is a consequence of the remainder being defined by subtracting the Hessian. The core analytic step is a bound on the third derivative along the line, which is obtained by combining a chain rule bound with a local bound on the third derivative of the remainder as a function on the full space. These pieces are assembled to yield the cubic estimate on the line, and then the final theorem follows by evaluating the line at the endpoint.

In Recognition Science, this result is a component in a larger program. The framework derives physical structure from a ledger of recognition events, and it models gravity as a discrete action on a triangulation. The cubic Taylor bound is a technical but necessary step: it shows that the nonlinear remainder is controlled, which is required for the Hessian to be a meaningful object and for the second variation of the action to be well-defined. Without such a bound, the approximation of the action by its quadratic part would not be justified, and the stability analysis of the discrete geometry would be incomplete.

The practical consequence is that the discrete approximation is not merely formal. The bound guarantees that, for small perturbations, the error in the quadratic approximation is genuinely small, and it shrinks in a controlled way as the perturbation is reduced. This is the kind of estimate that makes a numerical scheme trustworthy, and it is a prerequisite for any further analysis of the dynamics of the discrete geometry. The library's proof is a certificate that this estimate holds, and it is a foundation on which further results about the Regge action can be built.

/-- Exact Taylor theorem needed for the nonlinear Regge remainder.  This is
the finite-dimensional third-order Taylor estimate specialized to the canonical
Regge remainder. -/
def NonlinearReggeCubicTaylorTheorem
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  LocalCubicRemainderBound K hK

theorem nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hLine : CanonicalRemainderLineCubicEstimateTarget K hK) :
    NonlinearReggeCubicTaylorTheorem K hK := by
  rcases hLine with ⟨r, C, hr, hC, hineq⟩
  refine ⟨r, C, hr, hC, ?_⟩
  intro ξ hξ
  simpa [linePotential_one K ξ] using hineq ξ hξ

def CanonicalRemainderLineQuadraticTaylorZeroTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ r : ℝ, 0 < r ∧
    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      taylorWithinEval
        (fun t : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            (linePotential K ξ t))
        2 (Set.Icc (0 : ℝ) 1) 0 1 = 0

What this page does not claim

Not a derivation of the Regge action itself from first principles. Not a proof that the Regge action converges to the Einstein-Hilbert action in the continuum limit. Not a statement about the physical meaning of the constants r and C in the bound.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: