Geometry Regge Action Nonlinear Correspondence Nonlinear Regge Local Corresponde

The local bridge

In classical differential geometry, the Regge action is a discrete way to write gravity: it sums the curvature concentrated along the hinges of a triangulated space, rather than integrating a smooth field. The Recognition Science framework's library contains a machine-checked theorem, nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor, which states a precise, local relationship between this Regge action and the framework's own cost-based action. The theorem says that near a flat configuration, the full nonlinear Regge action equals its flat-space value plus a canonical quadratic term, with the difference bounded by a constant times the cube of the perturbation size.

To see what this means, imagine a gently curved sheet of metal. The Regge action measures the total bending energy concentrated along creases. The theorem says that if you start from a completely flat sheet and add a small deformation, the energy of the deformed sheet is, to second order in the deformation, exactly the energy of a simple quadratic form: the canonical Dirichlet energy, which measures how much the deformation varies from point to point. The error in this approximation is no larger than a constant times the cube of the deformation's size, so for small deformations the quadratic term dominates completely. This is a Taylor expansion result, stated and proved in the framework's formal library.

The theorem's name lists the conditions under which it holds. The triangulation must be incidence-consistent, meaning its edges and vertices connect in a regular way. The configuration must be flat to begin with. The edge stencil, a pattern of how curvature is distributed along edges, must eventually become zero away from the hinge. And a cubic Taylor theorem must hold for the Regge action. Under these conditions, the theorem derives the local correspondence. It does not claim that the full Regge action equals the weighted sum of cost functions exactly, everywhere. That global equality remains a target, not a proved result.

The consequence is a bridge between two languages. The framework's cost function, which arises from its foundational axioms, produces a quadratic term that matches the Regge action's second-order behavior near flat space. This means the cost-based action and the classical Regge action agree in the weak-field limit, the regime where gravity is nearly Newtonian. The theorem makes that agreement precise and machine-checked, with the error term explicitly bounded.

What the theorem does not claim is equally important. It does not prove that the Regge action and the cost action are identical as full nonlinear functionals. It does not establish the correspondence for large deformations, where the cubic remainder can dominate. And it does not derive the Regge action from first principles; it shows a local agreement, not an identity. The global nonlinear correspondence remains an open target in the framework's development.

theorem nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK)
    (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
    (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
    (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
    (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK)
    (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
    NonlinearReggeJCostLocalCorrespondence K hK :=
  nonlinearRegge_localCorrespondence_of_localHessianTaylorInputs K hK hFlat
    (nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor
      K hK hFlat D hZero hEdge hStencil hTaylor)

/-- 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) ξ

What this page does not claim

The theorem does not prove global equality between the full Regge action and the weighted sum of cost functions. The theorem does not establish the correspondence for large deformations. The theorem does not derive the Regge action from the framework's axioms.

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: