Geometry Regge Action Second Variation Regge Action Remainder Cubic Bound

The cubic remainder bound

The Regge action is a discrete version of the Einstein-Hilbert action from general relativity, built on a triangulated 3D geometry. It assigns a number to each way of assigning lengths to the edges of the triangulation. The action is nonlinear: its value does not change linearly with the edge lengths. A standard way to study a nonlinear function near a special point is to expand it as a Taylor series: a constant term, a linear term, a quadratic term, and a remainder that collects everything of higher order. The theorem in question concerns this remainder for the Regge action near a flat configuration, one where the geometry is locally Euclidean.

The declaration reggeActionRemainder_cubic_bound states that, under certain input conditions, the remainder is locally bounded by a constant times the cube of the perturbation size. In symbols: there exist positive radius r and nonnegative constant C such that for any vertex potential ξ with norm less than r, the norm of the remainder is at most C times the norm of ξ cubed. This is a local cubic bound. It says that the remainder shrinks at least as fast as the cube of the perturbation as the perturbation goes to zero. This is exactly the kind of estimate needed to justify treating the quadratic part as the dominant behavior near the flat configuration.

The theorem is conditional. It takes as a hypothesis a structure called ReggeActionCubicRemainderInput, a machine-checked collection of formal theorems that packages the required analytic facts. One constructor for this structure supplies the bound directly. Another, called reggeActionCubicRemainderInput_of_identically_zero, builds the input from the stronger assumption that the remainder is identically zero, in which case the bound holds with constant zero. The theorem itself simply extracts the bound from the input structure. It does not prove that the remainder is actually cubic; it proves that if the input conditions hold, then the cubic bound follows.

The declaration does not claim that the remainder is exactly cubic, nor that the bound is sharp. It does not assert that the cubic bound holds globally, only locally within some radius r. It does not prove that the remainder is identically zero, nor that the canonical Hessian is the correct second variation; those are separate statements, some of which are themselves conditional on other inputs. The theorem is a bridge: it connects a named analytic input, the local cubic bound, to the nonlinear Regge action, making the bound available for further work in the framework's library of formal theorems.

/-- Phase-E cubic remainder theorem, conditional on the named Taylor input. -/
theorem reggeActionRemainder_cubic_bound
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (h_cubic : ReggeActionCubicRemainderInput K hK h_flat) :
    LocalCubicRemainderBound K hK :=
  h_cubic.cubic_bound

/-- Phase-E cubic remainder theorem, conditional on the named Taylor input. -/
theorem reggeActionRemainder_cubic_bound
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (h_cubic : ReggeActionCubicRemainderInput K hK h_flat) :
    LocalCubicRemainderBound K hK :=
  h_cubic.cubic_bound

/-- A strong but useful sanity constructor: if the canonical remainder is
identically zero, it satisfies the local cubic bound with constant zero. -/
def reggeActionCubicRemainderInput_of_identically_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (hZero :
      ∀ ξ : VertexPotential K,
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
    ReggeActionCubicRemainderInput K hK h_flat where
  cubic_bound := by
    refine ⟨1, 0, by norm_num, le_rfl, ?_⟩
    intro ξ _hξ
    rw [hZero ξ]
    simp

What this page does not claim

The declaration does not claim that the remainder is exactly cubic, only that it is bounded by a cubic expression locally. The declaration does not assert that the cubic bound holds globally for all perturbations. The declaration does not prove that the remainder is identically zero, nor that the canonical Hessian is the correct second variation.

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/ReggeActionSecondVariation.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: