Geometry Regge Action Cubic Taylor Bound Canonical Remainder Line Third Deriv Bo

The line third-derivative bound

The declaration canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm is a theorem in the machine-checked library of formal theorems. It concerns the Regge action, a discrete geometric action used in lattice quantum gravity, built from edge lengths of a triangulation. The theorem states that a certain third-derivative bound for the remainder term of a Taylor expansion follows from two other conditions: a chain-rule bound and a local norm bound. In plain terms, it proves that if the remainder's third derivative is controlled along a line and locally in a neighborhood, then a cubic estimate holds for the remainder itself.

The theorem is stated for a finite-dimensional vertex-potential space. It assumes an incidence-consistent triangulation and a flat configuration, meaning the geometry is locally flat. The chain-rule condition controls the third derivative of the remainder composed with a line map, while the local norm condition bounds the third iterated derivative of the remainder in a neighborhood of zero. The conclusion is an explicit estimate: for small perturbations, the norm of the remainder is bounded by a constant times the cube of the perturbation norm.

This result is a technical step in a larger proof. It feeds into a chain of theorems that establish the cubic Taylor bound for the nonlinear Regge remainder. The bound is what allows the framework to treat the remainder as negligible to third order, which is needed for the second variation of the action and for connecting the discrete action to a continuum limit. The theorem itself is proved in the Lean 4 proof assistant, with no axioms beyond the standard kernel ones.

What the declaration does not claim is equally important. It does not assert that the chain-rule or local norm conditions actually hold for any particular triangulation; those are separate hypotheses. It does not prove that the Regge action itself is cubic, only that the remainder is bounded cubically under the stated conditions. It does not establish the physical relevance of the Regge action to quantum gravity; that is a modeling choice, not a theorem. The theorem is purely analytic, about the structure of the remainder, not about the physical content of the action.

/-- **CLOSURE CONDITIONAL ON CHAIN-RULE + LOCAL NORM BOUND.**

Given the chain-rule pointwise bound and the local norm bound on the third
Fréchet derivative of `R`, the line-restricted third-derivative bound holds
with the same `M` and `r := δ`, valid for all `‖ξ‖ < r` and all `t ∈ [0, 1]`.

Proof: for `‖ξ‖ < δ` and `t ∈ [0, 1]`, the point `t • ξ` has norm
`|t| · ‖ξ‖ ≤ ‖ξ‖ < δ`, so the local norm bound applies and yields
`‖iteratedFDeriv ℝ 3 R (t • ξ)‖ ≤ M`. The chain-rule pointwise bound then
gives `|iteratedDeriv 3 R_line t| ≤ M · ‖ξ‖³`. -/
theorem canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hChain : CanonicalRemainderLineChainRuleBoundTarget K hK)
    (hLocal : CanonicalRemainderIteratedFDerivLocalBoundTarget K hK) :
    CanonicalRemainderLineThirdDerivBoundTarget K hK := by
  rcases hLocal with ⟨δ, M, hδ, hM, hBound⟩
  rcases hChain with ⟨εC, hεC, hChainBnd⟩
  refine ⟨min δ εC, M, lt_min hδ hεC, hM, ?_⟩
  intro ξ hξ t ht
  have hξC : ‖ξ‖ < εC := lt_of_lt_of_le hξ (min_le_right _ _)
  have hξL : ‖ξ‖ < δ := lt_of_lt_of_le hξ (min_le_left _ _)
  -- Apply the localized chain-rule pointwise bound.
  have hChainPt := hChainBnd ξ hξC t ht
  -- Local norm bound at point `t • ξ`.
  have h_tξ_norm : ‖t • ξ‖ < δ := by
    have h_t_abs : |t| ≤ 1 := by
      rw [abs_of_nonneg ht.1]; exact ht.2
    rw [norm_smul, Real.norm_eq_abs]
    calc |t| * ‖ξ‖ ≤ 1 * ‖ξ‖ := by
            exact mul_le_mul_of_nonneg_right h_t_abs (norm_nonneg ξ)
      _ = ‖ξ‖ := one_mul _
      _ < δ := hξL
  have h_local := hBound (t • ξ) h_tξ_norm
  -- Combine: |iteratedDeriv 3 R_line t| ≤ ‖iteratedFDeriv 3 R (t • ξ)‖ · ‖ξ‖³ ≤ M · ‖ξ‖³.
  calc |iteratedDeriv 3
          (fun s : ℝ =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK)
              (linePotential K ξ s)) t|
        ≤ ‖iteratedFDeriv ℝ 3
            (fun ξ' : VertexPotential K =>
              reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
            (t • ξ)‖
          * ‖ξ‖ ^ (3 : ℕ) := hChainPt
      _ ≤ M * ‖ξ‖ ^ (3 : ℕ) := by
          have hξ3 : 0 ≤ ‖ξ‖ ^ (3 : ℕ) := by positivity
          exact mul_le_mul_of_nonneg_right h_local hξ3

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 nonlinearReggeCubicTaylorTheorem_of_lineTaylorData
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hData : CanonicalRemainderLineTaylorDataTarget K hK) :
    NonlinearReggeCubicTaylorTheorem K hK :=
  nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate K hK
    (lineCubicEstimate_of_lineTaylorData K hK hData)

What this page does not claim

The theorem does not prove that the chain-rule or local norm conditions hold for any particular triangulation. The theorem does not establish the physical relevance of the Regge action to quantum gravity. The theorem does not show that the Regge action itself is cubic, only that the remainder is bounded cubically under the stated conditions.

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: