Geometry Regge Action Nonlinear Correspondence

The local correspondence

Regge calculus is a discrete approach to general relativity where spacetime is built from flat triangular pieces, like a geodesic dome. The Regge action assigns a number to such a triangulation based on the angles where pieces meet, and its variation gives the discrete Einstein equations. The classical question is how this piecewise-flat action behaves under small deformations of the vertex positions.

The standard answer is a Taylor expansion. Near a flat configuration, the full nonlinear Regge action equals its value at flatness plus a quadratic term, with a remainder bounded by a constant times the cube of the deformation size. The quadratic term is exactly the canonical Dirichlet energy, the sum over edges of squared potential differences, weighted by the triangulation's incidence structure. This is the local nonlinear correspondence: the complicated geometry reduces to a simple quadratic form at second order.

The framework connects this to its own cost function. In Recognition Science, recognition events are recorded in a discrete ledger, a record of pairwise comparisons, and each comparison carries a forced cost. That cost, written J(x) = (x + 1/x)/2 - 1, becomes cosh(t) - 1 in logarithmic coordinates, which is even and has zero linear term. The weighted sum of these costs over the triangulation's edges is the J-cost action. The result proves that this action is even under sign reversal of the potential, a symmetry shared with the Dirichlet energy.

What is established is precise and deliberately limited. It does not claim the full nonlinear Regge action equals the J-cost action globally. Instead, it proves the local statement: near flatness, the Regge action differs from its flat value plus the canonical J/Dirichlet quadratic term by at most a cubic remainder. The strongest true replacement theorem is exactly this local quadratic-core correspondence, not a global equality. This is the honest scope of the result.

The consequence is that the framework's cost function inherits the classical action's small-perturbation behavior. Any computation that relies on the quadratic approximation of Regge calculus, such as linearized gravity or perturbation theory, can be reproduced with the J-cost action in its place. The nonlinear part remains open, but the bridge at second order is closed and checked.

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

/-- 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_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 full weighted J-cost edge action associated to the canonical incidence
weights.  This is the nonlinear J-cost expression; the present local theorem
uses only its quadratic jet. -/
def weightedJCostAction
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) : ℝ :=
  ∑ i : Fin K.nV, ∑ j : Fin K.nV,
    canonicalDualWeight K hK i j * jCostLog (ξ i - ξ j)

theorem weightedJCostAction_neg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    weightedJCostAction K hK (-ξ) = weightedJCostAction K hK ξ := by
  unfold weightedJCostAction
  refine Finset.sum_congr rfl ?_
  intro i _
  refine Finset.sum_congr rfl ?_
  intro j _
  change canonicalDualWeight K hK i j * jCostLog ((-ξ) i - (-ξ) j) =
    canonicalDualWeight K hK i j * jCostLog (ξ i - ξ j)
  congr 1
  have harg : ((-ξ) i - (-ξ) j) = -(ξ i - ξ j) := by
    simp
    ring
  rw [harg, jCostLog_neg]

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

What this page does not claim

Global equality between the full Regge action and the weighted J-cost action. A proof that the cubic remainder vanishes for all triangulations. Any statement about the physical dynamics of the Regge action beyond the local quadratic approximation.

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: