Gravity Analysis Regge4 Dalgebraic Closer

The 4D algebraic closer

In the Recognition Science framework, gravity is studied by discretizing spacetime into a lattice of hinges and orbits, then checking whether the discrete sums reproduce the smooth equations of Einstein's general relativity. The module called Regge 4D algebraic closer is a status report from that campaign. It is a machine-checked collection of formal theorems, a ledger in the sense of a discrete record of events, that records which algebraic identities about gravitational wave polarizations have been proven and which have not.

The classical background is Regge calculus, a 1961 method by Tullio Regge that approximates curved spacetime with flat pieces, like a geodesic dome approximating a sphere. The module works in four dimensions and focuses on the two transverse-traceless (TT) polarizations of a gravitational wave, conventionally called plus and cross. The central question is whether the discrete, lattice-based calculation of the wave's energy-momentum matches the continuum result from Einstein's theory, where the TT coefficient is -1/4.

What the module proves is a set of banked witnesses. It proves that the plus and cross polarizations, when properly normalized, are indeed TT polarizations. It proves that a certain one-orbit calculation gives -3, which is not the continuum value of -1/4, a decoy that shows the naive single-orbit sum is wrong. It proves that a pure gauge mode gives zero, as it should. And it proves that the full zero-momentum moment, summed over all hinge orbit types, vanishes on the axis TT plus polarization and on the decoy gauge. These are exact, checked identities, not numerical approximations.

The module is equally explicit about what it does not prove. Three targets are named as OPEN, with status flags set to false: full TT isotropy for every direction, pure gauge vanishing for every direction, and agreement between plus and cross symbols. The module does not prove that the discrete sum converges to the Einstein-Hilbert action in four dimensions, and it does not flip the gap action recovery flag. The axiom footprint is the standard three, with no new axioms and no sorry.

What this establishes in plain language is a precise map of the terrain. The framework has proven the algebraic pieces it can, and it has named exactly where the proof stops. The reader can see that the decoy is real, the witnesses are real, and the open targets are real. The consequence is that the framework's claim about gravity is not a vague hope but a checklist with four items checked and three items still on the board.

/-- Nonvacuity of the TT hypothesis class used by continuum targets. -/
theorem tt_witnesses_nonvacuous :
    IsTTPolarization4D axisWave axisTTPlusNormalized ∧
      IsTTPolarization4D axisWave axisTTCrossNormalized :=
  continuum_target_hypothesis_nonvacuous

/-- Decoy: the single-orbit `(1,1)` m² coefficient is not the continuum EH
target. -/
theorem decoy_one_orbit_m2_ne_eh_coefficient :
    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
      einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) ∧
        (-3 : ℝ) ≠ -(1 / 4 : ℝ) :=
  decoy_one_orbit_m2_is_not_continuum_target

/-- Gauge: the closed-form `(1,1)` m² symbol vanishes on `decoyGauge`. -/
theorem gauge_m2Symbol_vanishes_on_decoy :
    ReggeBlochM2Symbol4D.m2Symbol decoyGauge = 0 :=
  m2Symbol_decoyGauge

/-- Zero-momentum full moment vanishes on axis TT plus. -/
theorem fullMomentZeroMomentum_axisTTPlus :
    fullMomentZeroMomentum axisTTPlus = 0 := by
  rw [fullMomentZeroMomentum_eq_trueWeight,
    trueWeightZeroMomQuadratic_axisTTPlus]

/-- Zero-momentum full moment vanishes on decoy gauge. -/
theorem fullMomentZeroMomentum_decoyGauge :
    fullMomentZeroMomentum decoyGauge = 0 := by
  rw [fullMomentZeroMomentum_eq_trueWeight,
    trueWeightZeroMomQuadratic_decoyGauge]

What this page does not claim

This module does not prove that the discrete sum converges to the Einstein-Hilbert action in four dimensions. This module does not prove full TT isotropy for all directions or pure gauge vanishing for all directions. This module does not claim the plus and cross symbols agree.

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