Geometry Regge Action Nonlinear Correspondence Strongest True Regge Jcost Replac

The local correspondence

The Regge action is a standard way to write gravity on a triangulated space, a space built from flat tetrahedral pieces. It sums the angles by which the pieces fail to meet flatly, weighted by the length of the shared hinge. The framework's machine-checked library of formal theorems proves a local statement about this action: near a flat configuration, the full nonlinear Regge action equals its flat value plus a canonical quadratic term, with the difference bounded by a constant times the cube of the displacement. The quadratic term is the one supplied by the second derivative, the Hessian, of the Regge action at flat space.

That quadratic term is not an arbitrary choice. The library proves it equals half the canonical Dirichlet energy, a standard measure of how much a field varies across the triangulation. The theorem also proves the term is always nonnegative, so it behaves like an energy that penalizes deviation from flatness. The full statement, named strongestTrueReggeJCostReplacement_of_eventuallyZero_edgeStencil_and_taylor, assembles these pieces: it takes a flat configuration, a package of derivative data, and three technical hypotheses about the edge stencil, the deficit derivative, and a cubic Taylor bound, and concludes that the local correspondence holds. The name encodes the conditions, not the conclusion.

The conclusion is deliberately local and quadratic-core. It says the action matches its flat value plus the canonical J/Dirichlet quadratic term up to a controlled cubic remainder. It does not assert literal equality with the full weighted J-cost action, a separate nonlinear expression built from the framework's cost function in log coordinates. That stronger global claim remains open. The theorem is the strongest true replacement currently proved: it gives the quadratic core exactly and bounds the nonlinear part, rather than claiming the two actions coincide everywhere.

In Recognition Science, this local correspondence is the bridge between the framework's cost function and classical gravity. The cost function J, forced by the framework's axioms, appears in log coordinates as cosh(t) minus 1, an even function. The weighted J-cost action sums this over edges with canonical weights. The theorem shows that near flat space, the Regge action sees exactly the quadratic jet of that J-cost action, with a cubic error controlled by a bound. This is the sense in which the framework's cost reproduces gravity's weak-field behavior: not by exact equality, but by matching the quadratic core to second order.

The practical consequence is a precise statement of when the framework's cost can stand in for the Regge action: only near flat configurations, and only up to a bounded cubic error. The bound is explicit in the theorem's statement, with a radius r and a constant C. This is not a vague approximation claim. It is a machine-checked inequality, valid for all potentials within the radius. What the theorem does not do is extend that correspondence to strong fields, where the cubic remainder can dominate. That remains a target for future work.

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

/-- 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 : ℕ)

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]

/-- The strongest true nonlinear Regge/J-cost replacement theorem surface.

This is deliberately local and quadratic-core: it says the full nonlinear
Regge action equals its flat value plus the canonical J/Dirichlet quadratic
term up to a controlled cubic remainder.  It does not assert literal equality
with the full weighted J-cost action. -/
def StrongestTrueReggeJCostReplacement
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  NonlinearReggeJCostLocalCorrespondence K hK

theorem strongestTrueReggeJCostReplacement_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) :
    StrongestTrueReggeJCostReplacement K hK :=
  nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor
    K hK hFlat D hZero hEdge hStencil hTaylor

What this page does not claim

Global exact equality between the Regge action and the weighted J-cost action is not asserted. The theorem does not apply to strong-field configurations where the cubic remainder is not controlled. The edge stencil and deficit derivative hypotheses are not proven to hold for all triangulations; they are assumptions of the theorem.

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: