Geometry Regge Action Nonlinear Correspondence Canonical Jquadratic Term Eq Diri

The quadratic bridge

In discrete gravity, the Regge action is a standard way to write the gravitational action on a triangulated space: it sums the deficit angles around hinges, weighted by the hinge lengths. The Recognition Science framework's library, a machine-checked collection of formal theorems, proves a local statement about this action. The declaration canonicalJQuadraticTerm_eq_dirichlet establishes that a certain quadratic term, built from the second derivative of the Regge action at a flat background, is exactly equal to half the canonical Dirichlet energy of the vertex potential. In plain terms: the leading, second-order piece of the discrete gravitational action is just the familiar quadratic energy of a scalar field on the lattice.

This equality is not the whole story, and the library is explicit about that. The full nonlinear Regge action is not claimed to equal the quadratic term globally. Instead, the theorem nonlinearRegge_exact_canonical_split gives an exact algebraic decomposition: the full action equals its flat value, plus the canonical quadratic term, plus a remainder. A separate definition, NonlinearReggeJCostLocalCorrespondence, states the precise local sense in which the correspondence holds: for small perturbations, the difference between the full action and the flat value plus the quadratic term is bounded by a constant times the cube of the perturbation size. This is a Taylor-style statement with a controlled cubic error, not an exact equality.

The quadratic term itself is nonnegative, as shown by canonicalJQuadraticTerm_nonneg, which follows directly from the equality with the Dirichlet energy. The symmetry of the full weighted J-cost action under sign reversal of the potential is also proved, matching the evenness of the quadratic term. These are the concrete, checkable facts the library delivers. What it does not deliver is a claim that the full nonlinear Regge action is literally equal to the full weighted J-cost action summed over edges. The docstring for the strongest replacement theorem says so in so many words: it does not assert literal equality with the full weighted J-cost action. The correspondence is deliberately local and quadratic-core.

What this means for the reader is that the framework has a precise, machine-checked handle on how discrete gravity relates to its own cost function at the quadratic level, with the error term under control. The bridge between the Regge action and the J-cost is not a guess or a numerical coincidence; it is a proved local equivalence with a stated remainder. The open question, flagged by the library's own structure, is whether a global or exact nonlinear correspondence exists beyond this local quadratic jet. That remains a target, not a result.

theorem canonicalJQuadraticTerm_eq_dirichlet
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    canonicalJQuadraticTerm K hK ξ =
      (1 / 2) * canonicalDirichletEnergy K hK ξ := by
  unfold canonicalJQuadraticTerm
  rw [canonicalReggeHessian_quadratic_eq_dirichlet]

/-- Exact algebraic split of the full nonlinear Regge action into the flat
value, the canonical quadratic J/Dirichlet term, and the nonlinear remainder. -/
theorem nonlinearRegge_exact_canonical_split
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    reggeAction K hK ξ =
      reggeAction K hK (zeroPotential K) +
        canonicalJQuadraticTerm K hK ξ +
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ := by
  simpa [canonicalJQuadraticTerm] using
    reggeAction_taylor_decomposition K hK (canonicalReggeHessian K hK) ξ

theorem canonicalJQuadraticTerm_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ canonicalJQuadraticTerm K hK ξ := by
  rw [canonicalJQuadraticTerm_eq_dirichlet]
  exact mul_nonneg (by norm_num) (canonicalDirichletEnergy_nonneg K hK ξ)

/-- Local nonlinear Regge/J-cost correspondence: the full action differs from
its flat value plus the canonical J/Dirichlet quadratic jet by a cubic
remainder. -/
def NonlinearReggeJCostLocalCorrespondence
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ‖reggeAction K hK ξ -
          reggeAction K hK (zeroPotential K) -
          canonicalJQuadraticTerm K hK ξ‖ ≤
        C * ‖ξ‖ ^ (3 : ℕ)

What this page does not claim

The full nonlinear Regge action is not asserted to equal the full weighted J-cost action summed over all edges. The local correspondence does not claim to hold for large perturbations; it is bounded only within a small neighborhood of the flat configuration. The quadratic term equality does not by itself establish the physical equivalence of discrete gravity and the J-cost framework beyond the second order.

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