Encyclopedia Geometry Geometry Regge Action Cubic Taylor Bound Canonical Remainder Line Taylor Data Of

ARTICLE 3 claims 3 theorems

Geometry Regge Action Cubic Taylor Bound Canonical Remainder Line Taylor Data Of

How a machine-checked proof shows the leftover error in a discrete gravity action shrinks at least as fast as the cube of a small perturbation.

Verify this page

The cubic remainder bound

In numerical analysis, a Taylor expansion approximates a smooth function near a point by a polynomial, and the remainder is the difference between the true value and the polynomial. The classical third-order Taylor theorem says that if a function is three times continuously differentiable, then the remainder at a point is bounded by a constant times the cube of the distance from the expansion point. This is a standard tool, proved in every analysis course.

The Recognition Science framework applies this classical theorem to a specific object: the remainder of the Regge action, a discrete model of gravity built from edge lengths of a triangulation. The framework's machine-checked library of formal theorems contains a result, canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm, that assembles the hypotheses needed to conclude the cubic bound. The name describes its inputs: jet inputs (the function's derivatives), a chain rule bound, and a local norm bound.

In plain terms, the declaration establishes that if three conditions hold, then the remainder of the Regge action, after subtracting its quadratic part, is bounded by a constant times the cube of the perturbation size. The three conditions are: the remainder is three times continuously differentiable along a line through the origin; its quadratic Taylor term vanishes at the origin; and its third derivative is locally bounded. The proof combines these to produce a cubic estimate, which is then used to conclude the full nonlinear cubic Taylor theorem for the Regge remainder.

The declaration does not claim that the remainder is exactly zero, nor that the bound is sharp, nor that the conditions hold for all triangulations. It is a conditional statement: given the inputs, the cubic bound follows. The theorem is a building block in a larger argument, not a standalone physical law. It does not assert anything about the values of the constants in the bound, only their existence.

What this fact changes is the analytic foundation for the Regge action: it provides the rigorous error estimate needed to justify treating the quadratic part as the leading behavior near a flat configuration. Without such a bound, the approximation would be heuristic. With it, the framework can proceed to use the Regge action's second variation with confidence that the neglected terms are controlled by a cubic power.

THEOREM lineTaylorData_of_splitTargets · lineCubicEstimate_of_lineTaylorData · nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
lineTaylorData_of_splitTargets · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:274 
theorem lineTaylorData_of_splitTargets
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hCont : CanonicalRemainderLineContDiffTarget K hK)
    (hTaylorZero : CanonicalRemainderLineQuadraticTaylorZeroTarget K hK)
    (hThird : CanonicalRemainderLineThirdDerivBoundTarget K hK) :
    CanonicalRemainderLineTaylorDataTarget K hK := by
  rcases hCont with ⟨rC, hrC, hC⟩
  rcases hTaylorZero with ⟨rT, hrT, hT⟩
  rcases hThird with ⟨rD, M, hrD, hM, hD⟩
  refine ⟨min (min rC rT) rD, M, min_pos3 hrC hrT hrD, hM, ?_⟩
  intro ξ hξ
  have hξC : ‖ξ‖ < rC := lt_of_lt_of_le hξ (min_le_left (min rC rT) rD |>.trans (min_le_left rC rT))
  have hξT : ‖ξ‖ < rT := by
    have hle : min (min rC rT) rD ≤ rT :=
      le_trans (min_le_left (min rC rT) rD) (min_le_right rC rT)
    exact lt_of_lt_of_le hξ hle
  have hξD : ‖ξ‖ < rD := lt_of_lt_of_le hξ (min_le_right (min rC rT) rD)
  exact ⟨hC ξ hξC, hT ξ hξT, hD ξ hξD⟩
lineCubicEstimate_of_lineTaylorData · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:293 
theorem lineCubicEstimate_of_lineTaylorData
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hData : CanonicalRemainderLineTaylorDataTarget K hK) :
    CanonicalRemainderLineCubicEstimateTarget K hK := by
  rcases hData with ⟨r, M, hr, hM, hdata⟩
  refine ⟨r, M / 6, hr, div_nonneg hM (by norm_num), ?_⟩
  intro ξ hξ
  rcases hdata ξ hξ with ⟨hCont, hTaylorZero, hBound⟩
  have h :=
    abs_value_le_cubic_of_taylor_data
      (fun t : ℝ =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK)
          (linePotential K ξ t))
      M (‖ξ‖ ^ (3 : ℕ)) hCont hTaylorZero hBound
  simpa [Real.norm_eq_abs] using h
nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:146 
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ξ
THEOREM CanonicalRemainderLineContDiffTarget · CanonicalRemainderLineQuadraticTaylorZeroTarget · CanonicalRemainderLineThirdDerivBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
CanonicalRemainderLineContDiffTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:206 
def CanonicalRemainderLineContDiffTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ r : ℝ, 0 < r ∧
    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ContDiffOn ℝ (3 : ℕ)
        (fun t : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            (linePotential K ξ t))
        (Set.Icc (0 : ℝ) 1)
CanonicalRemainderLineQuadraticTaylorZeroTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:250 
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
CanonicalRemainderLineThirdDerivBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:260 
def CanonicalRemainderLineThirdDerivBoundTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ (r M : ℝ), 0 < r ∧ 0 ≤ M ∧
    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ∀ t ∈ Set.Icc (0 : ℝ) 1,
        |iteratedDeriv 3
          (fun s : ℝ =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK)
              (linePotential K ξ s)) t| ≤ M * ‖ξ‖ ^ (3 : ℕ)
THEOREM lineCubicEstimate_of_lineTaylorData · nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
lineCubicEstimate_of_lineTaylorData · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:293 
theorem lineCubicEstimate_of_lineTaylorData
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hData : CanonicalRemainderLineTaylorDataTarget K hK) :
    CanonicalRemainderLineCubicEstimateTarget K hK := by
  rcases hData with ⟨r, M, hr, hM, hdata⟩
  refine ⟨r, M / 6, hr, div_nonneg hM (by norm_num), ?_⟩
  intro ξ hξ
  rcases hdata ξ hξ with ⟨hCont, hTaylorZero, hBound⟩
  have h :=
    abs_value_le_cubic_of_taylor_data
      (fun t : ℝ =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK)
          (linePotential K ξ t))
      M (‖ξ‖ ^ (3 : ℕ)) hCont hTaylorZero hBound
  simpa [Real.norm_eq_abs] using h
nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:146 
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ξ

What this page does not claim

The declaration does not claim the remainder is exactly zero. It does not claim the cubic bound is sharp or that the constants are known explicitly. It does not assert the three conditions hold for all triangulations.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND