Gravity Analysis Regge4 Dexact Action Symbol

The exact flat cross-term symbol

In numerical relativity, the Regge action is a discrete version of the Einstein-Hilbert action, built from the lengths of edges in a triangulated spacetime. Its second variation, the Hessian, controls the propagation of small perturbations, including gravitational waves. On a flat background, where the deficit angles vanish, the Hessian's cross term takes a simple form: a sum over hinges of the product of the change in area and the change in deficit angle. The framework's machine-checked library of formal theorems defines this cross term exactly for plane-wave strains on a 4D hypercubic lattice, with each hinge's deficit phase resolved by its position in the lattice star.

The central object is the exact flat cross-term fold, a function that takes a 4x4 strain matrix and a wave vector, and returns a number. It does this by summing over hinge orbit types, over the 24 permutations of the lattice, and over the 10 hinge slots, using a position-resolved deficit phasing. Two structural theorems about this fold are established: it is homogeneous of degree two in the strain matrix, meaning scaling the strain by a constant c scales the result by c squared, and it vanishes for the zero strain. These are the expected properties of a Hessian. A separate discrete symbol multiplies this fold by a bookkeeping factor of 2, mirroring a 3D second-difference construction.

In Recognition Science, the framework models this as a discrete ledger of recognition events. The status flags record what is established: the continuum symbol has rebounded to the exact fold, the fold is retained as legacy, and the edge-origin m² certificates for the banked transverse-traceless witnesses are in place. The key check, measured on the banked gauge suite, is that the fold sends normalized transverse-traceless modes on the symbol direction to -1/4. This is not yet a proof for all modes; the limit as the lattice side tends to infinity remains open, as does the isotropy of the e0 direction. The exact action symbol status for the S_RS ledger and gap action recovery is false, meaning those specific constructions are not yet inhabited.

What this establishes in plain language is a precise, machine-checked handle on the quadratic part of discrete gravity on flat space. It gives a concrete, computable object that behaves like a Hessian, with the correct scaling and vanishing properties, and it matches the expected -1/4 value on the tested gravitational wave modes. This is a step toward understanding how the discrete theory reproduces continuum gravity, but it is not the full story. The framework explicitly does not claim the continuum limit for all modes, nor does it claim isotropy, and it does not claim to have recovered the S_RS action or the gap action. These remain open targets, with the exact flat cross-term fold serving as the established foundation.

theorem exactFlatCrossTermFold_smul (c : ℝ) (H : Mat4) (m : Wave4) :
    exactFlatCrossTermFold (c • H) m =
      c ^ 2 * exactFlatCrossTermFold H m := by
  unfold exactFlatCrossTermFold exactFlatCrossTermOrbit
  simp_rw [exactFlatCrossTermSlot_smul]
  -- ∑ ty, w_ty * ∑∑ c² f = c² * ∑ ty, w_ty * ∑∑ f
  have hty : ∀ ty : HingeOrbitType,
      (orbitStarSize ty)⁻¹ *
          ∑ s : Fin 24, ∑ t : Fin 10,
            c ^ 2 * exactFlatCrossTermSlot ty H m s t =
        c ^ 2 *
          ((orbitStarSize ty)⁻¹ *
            ∑ s : Fin 24, ∑ t : Fin 10, exactFlatCrossTermSlot ty H m s t) := by
    intro ty
    simp_rw [Finset.mul_sum]
    ring_nf
  simp_rw [hty, ← Finset.mul_sum]

theorem finiteExactReggeSymbol_zero (j : ℕ) (m : Fin 4 → ℤ) :
    finiteExactReggeSymbol j m 0 = 0 := by
  simpa using finiteExactReggeSymbol_smul (0 : ℝ) j m (1 : Mat4)

theorem discreteExactReggeSymbol_eq (j : ℕ) (m : Fin 4 → ℤ) (E : Mat4) :
    discreteExactReggeSymbol j m E =
      (2 : ℝ) * finiteExactReggeSymbol j m E := by
  unfold discreteExactReggeSymbol discreteBookkeepingFactor
  ring

/-- Local status flags remain open; geometric ContinuumSymbolIs Tendsto
is the Preflight ledger gate.  Edge-origin m² decide-certs are banked
elsewhere and do not inhabit `S_RS`. -/
theorem exact_action_srs_still_open :
    exactActionSymbolStatus.srsInhabited = false ∧
      exactActionSymbolStatus.gapActionRecovery = false := by
  decide

What this page does not claim

The framework does not prove the continuum limit for all modes, only for the banked transverse-traceless witnesses. The framework does not establish isotropy in the e0 direction. The framework does not claim the S_RS action or gap action recovery is inhabited.

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/Gravity/Analysis/Regge4DExactActionSymbol.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: