Geometry Regge Action Cubic Taylor Bound Iterated Deriv Within One Canonical Rem

The cubic remainder bound

In Recognition Science (a framework that derives physical structure from a discrete record of events, called a ledger), the declaration iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs establishes a precise analytic fact about the Regge action, a discrete version of the Einstein-Hilbert action used in numerical relativity. The theorem states that the remainder term in a cubic Taylor expansion of this action, evaluated along a straight line in the space of vertex potentials, is bounded by a constant times the cube of the perturbation's size. This is a local, third-order estimate: it says that for small enough perturbations, the error in approximating the action by its quadratic part grows no faster than the cube of the perturbation's magnitude.

The theorem is proved in a machine-checked library of formal theorems, meaning every step is verified by a computer. It is a THEOREM: it follows from the definitions and axioms with no gaps. The proof works by first showing that the remainder function is smooth (infinitely differentiable) at the flat configuration, then bounding its third derivative along the line, and finally applying a standard Taylor estimate. The key inequality is that for any perturbation ξ with norm less than some radius r, the norm of the remainder at ξ is at most C times ‖ξ‖³, for some constants r > 0 and C ≥ 0.

This result is a technical foundation for the framework's treatment of geometry. It provides the rigorous control needed to show that the Regge action, when expanded around a flat configuration, has a well-behaved cubic error term. This is not a claim about physics directly; it is a statement about the mathematical structure of the action functional. It does not, for example, prove that the Regge action is the correct discrete gravity action, nor does it establish any physical prediction. It is a necessary analytic ingredient for further developments, ensuring that the approximation scheme is mathematically sound.

What the theorem does not claim is equally important. It does not say the bound is sharp, nor does it provide a numerical value for the constants C and r. It does not apply to arbitrary perturbations, only to those within a small neighborhood of zero. It does not address the global behavior of the action, only its local cubic error. And it does not, by itself, imply anything about the physical validity of the framework's geometric models. It is a pure analytic lemma, albeit one that the framework relies on for its geometric foundations.

/-- One-dimensional line form of the remaining cubic Taylor estimate.

For every conformal direction `ξ`, restrict the canonical remainder to the line
`t ↦ tξ`.  A standard one-variable Taylor theorem with zero value, first
variation, and second variation at `t = 0` should prove this estimate from a
uniform bound on third derivatives along the segment. -/
def CanonicalRemainderLineCubicEstimateTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ‖reggeActionRemainder K hK (canonicalReggeHessian K hK)
          (linePotential K ξ 1)‖ ≤
        C * ‖ξ‖ ^ (3 : ℕ)

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ξ

/-- **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

What this page does not claim

This theorem does not prove that the Regge action is the correct discrete gravity action. It does not establish any physical prediction or numerical value for the bound's constants. It does not address the global behavior of the action, only its local cubic error. It does not claim the bound is sharp or that it applies to arbitrary perturbations.

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: