Encyclopedia Geometry Geometry Regge Action Cubic Taylor Bound Canonical Remainder Iterated Fderiv3 Lo

ARTICLE 3 claims 3 theorems

Geometry Regge Action Cubic Taylor Bound Canonical Remainder Iterated Fderiv3 Lo

A machine-checked theorem shows that near a flat configuration, the error term of the nonlinear Regge action is locally controlled by the cube of the perturbation size.

Verify this page

The local third-derivative bound

The Regge action is a discrete model of gravity built from a triangulated space, where the geometry is encoded in the edge lengths and the action is a sum over the triangular hinges. In the Recognition Science framework, the action is treated as a function on a finite-dimensional space of vertex potentials, and the question is how its nonlinear remainder behaves under small perturbations. The declaration canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration establishes a precise local bound on the third derivative of that remainder, under the condition that the configuration is flat.

In plain terms, the theorem says: if the geometry is flat (meaning the curvature is zero), then there exists a small radius around the origin in the space of vertex potentials such that, for every perturbation within that radius, the norm of the third iterated derivative of the remainder is bounded by a constant. This is a local statement: it holds only in a neighborhood of the flat configuration, not globally. The bound is the key analytic ingredient needed to control the error term in a third-order Taylor expansion of the nonlinear Regge action, which in turn is what makes the framework's treatment of the action's variation rigorous.

The theorem is part of a larger chain in the machine-checked library of formal theorems, which isolates the analytic content needed after the nonlinear Hessian has been identified. It is a finite-dimensional result, specialized to the canonical Regge remainder, and it is proved in the Lean 4 proof assistant. The declaration is a theorem, not a definition, and it is axiom-clean: its proof relies only on the standard axioms of the ambient type theory, with no framework-specific axioms.

What the theorem does not claim is equally important. It does not assert that the bound holds for all configurations, only for flat ones. It does not provide an explicit value for the constant M or the radius δ; it only asserts their existence. It does not establish that the remainder itself is small, only that its third derivative is bounded in a neighborhood. And it does not, by itself, prove that the Regge action is well-behaved globally; it is a local analytic tool, not a global statement.

The consequence of this theorem is that the framework can proceed with a rigorous third-order Taylor expansion of the nonlinear Regge action near flat configurations, which is a necessary step for the framework's treatment of the action's variation and for any subsequent stability or quantization arguments. Without this bound, the remainder term would be uncontrolled, and the Taylor expansion would be only formal. With it, the expansion is justified, at least locally, and the framework has a solid analytic foundation for the next steps in its derivation.

THEOREM canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:791 
/-- **CLOSURE: `CanonicalRemainderIteratedFDerivLocalBoundTarget`.**

The third Fréchet derivative of the canonical remainder is locally bounded
at the flat point: by `ContDiffAt` and `ContDiffAt.continuousAt_iteratedFDeriv`,
`iteratedFDeriv ℝ 3 R` is continuous at `0`, so `‖iteratedFDeriv ℝ 3 R z‖ < ‖0‖ + 1`
for `z` close to `0`. We take `M := ‖iteratedFDeriv ℝ 3 R 0‖ + 1` and `δ` from
the continuity δ-ε statement. -/
theorem canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    CanonicalRemainderIteratedFDerivLocalBoundTarget K hK := by
  -- ContDiffAt of R at zeroPotential at order ⊤.
  have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (zeroPotential K) :=
    canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
  -- iteratedFDeriv 3 R is continuous at zeroPotential K.
  have hContAt :
      ContinuousAt
        (iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ'))
        (zeroPotential K) := by
    refine hContR.continuousAt_iteratedFDeriv (k := 3) ?_
    exact (WithTop.coe_le_coe).mpr le_top
  -- Set the bound `M := ‖iteratedFDeriv 3 R 0‖ + 1`.
  set M : ℝ := ‖iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (zeroPotential K)‖ + 1 with hM_def
  have hM_nonneg : 0 ≤ M := by
    have hpos : 0 ≤ ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (zeroPotential K)‖ := norm_nonneg _
    linarith
  -- Continuity at zeroPotential K with tolerance 1.
  rw [Metric.continuousAt_iff] at hContAt
  obtain ⟨δ, hδ_pos, hδ⟩ := hContAt 1 (by norm_num : (0 : ℝ) < 1)
  refine ⟨δ, M, hδ_pos, hM_nonneg, ?_⟩
  intro z hz
  -- ‖z - zeroPotential K‖ = ‖z‖ since zeroPotential K is the zero element.
  have hz_dist : dist z (zeroPotential K) < δ := by
    rw [dist_eq_norm]
    have h_zp : (zeroPotential K) = (0 : VertexPotential K) := by
      funext i; simp [zeroPotential]
    rw [h_zp]
    simpa using hz
  -- Apply continuity bound.
  have h_dist := hδ hz_dist
  -- h_dist : dist (iteratedFDeriv 3 R z) (iteratedFDeriv 3 R 0) < 1
  rw [dist_eq_norm] at h_dist
  -- ‖A - B‖ < 1 implies ‖A‖ ≤ ‖B‖ + 1 = M.
  have h_le : ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z‖
        ≤ ‖iteratedFDeriv ℝ 3
            (fun ξ' : VertexPotential K =>
              reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
            (zeroPotential K)‖ + 1 := by
    have h_tri := norm_sub_norm_le
      (iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z)
      (iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (zeroPotential K))
    linarith
  exact h_le
THEOREM CanonicalRemainderIteratedFDerivLocalBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
CanonicalRemainderIteratedFDerivLocalBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:731 
/-- Sub-target (b): the local norm bound on the third Fréchet derivative of
`R` in a neighborhood of the flat point. This is `ContDiffAt` plus
`ContDiffAt.continuousAt_iteratedFDeriv`; we expose it as a named target so
the third-deriv bound is theorem-grade conditional on it. -/
def CanonicalRemainderIteratedFDerivLocalBoundTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ (δ M : ℝ), 0 < δ ∧ 0 ≤ M ∧
    ∀ z : VertexPotential K, ‖z‖ < δ →
      ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          z‖ ≤ M
THEOREM CanonicalRemainderIteratedFDerivLocalBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean
CanonicalRemainderIteratedFDerivLocalBoundTarget · IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean:731 
/-- Sub-target (b): the local norm bound on the third Fréchet derivative of
`R` in a neighborhood of the flat point. This is `ContDiffAt` plus
`ContDiffAt.continuousAt_iteratedFDeriv`; we expose it as a named target so
the third-deriv bound is theorem-grade conditional on it. -/
def CanonicalRemainderIteratedFDerivLocalBoundTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ (δ M : ℝ), 0 < δ ∧ 0 ≤ M ∧
    ∀ z : VertexPotential K, ‖z‖ < δ →
      ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          z‖ ≤ M

What this page does not claim

The theorem does not prove that the remainder itself is small, only that its third derivative is bounded. The theorem does not provide explicit values for the bound constant or the radius of the neighborhood. The theorem does not apply to non-flat configurations, where the bound may fail.

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