Gravity Analysis Regge4 Dalgebraic Closer Full Moment Zero Momentum Eq True Weig

The zero-momentum identity

In the framework's machine-checked library of formal theorems, recognition, a discrete record of events, builds up a four-dimensional lattice. The declaration fullMomentZeroMomentum_eq_trueWeight proves that two distinct sums over that lattice give the same number at zero momentum. One sum adds contributions orbit by orbit; the other uses a single "true weight" quadratic form. The theorem states that for any matrix H, the full zero-momentum moment equals the true-weight zero-momentum quadratic form. The proof is a definitional unfolding: both sides reduce to the same expression by rfl, so the identity holds by construction.

This identity is a banked witness, not a physical claim. It feeds three concrete vanishing results: the full moment vanishes on the axis TT-plus polarization, on the decoy gauge, and on the decoy trace. Each of those uses the identity to rewrite the full moment into the true-weight form, which is already known to vanish. The theorem also connects to a bilinear form, showing the moment is quadratic in H. These are algebraic facts about the lattice sums, with no claim about the continuum limit or about general relativity.

What the declaration does not claim matters as much as what it proves. It does not prove that the full moment matches the Einstein-Hilbert coefficient of -1/4 for all directions and polarizations. That isotropy target, named Regge4DFullTTIsotropyTarget, remains OPEN with status flag false. The pure-gauge vanishing target and the plus-cross agreement target are also OPEN. The status record regge4DAlgebraicCloserStatus sets all three to false, and a theorem confirms the banked identity does not flip them. The identity also does not prove convergence to the Einstein-Hilbert action in four dimensions, and it does not recover the gap action. Those targets stay false.

The practical consequence is a clean algebraic core: the zero-momentum moment is well-defined and consistent across two summation schemes, and it vanishes on the specific test cases checked. That consistency is what the framework banks. The reader should not take it as evidence that the full gravitational recovery is done. The honest summary is one sentence: the identity proves an algebraic equivalence, not a physical limit.

theorem fullMomentZeroMomentum_eq_trueWeight (H : Mat4) :
    fullMomentZeroMomentum H = trueWeightZeroMomQuadratic H := by
  unfold fullMomentZeroMomentum fullMomentOrbitContribution
    trueWeightZeroMomQuadratic
  rfl

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

/-- Zero-momentum full moment vanishes on decoy trace / homothety. -/
theorem fullMomentZeroMomentum_decoyTrace :
    fullMomentZeroMomentum decoyTrace = 0 := by
  rw [fullMomentZeroMomentum_eq_trueWeight,
    trueWeightZeroMomQuadratic_decoyTrace]

theorem regge4DAlgebraicCloserStatus_flags :
    regge4DAlgebraicCloserStatus.decoyOneOrbitClosed = true ∧
      regge4DAlgebraicCloserStatus.plusCrossWitnessesClosed = true ∧
        regge4DAlgebraicCloserStatus.gaugeM2SymbolClosed = true ∧
          regge4DAlgebraicCloserStatus.fullMomentZeroMomClosed = true ∧
            regge4DAlgebraicCloserStatus.fullTTIsotropyClosed = false ∧
              regge4DAlgebraicCloserStatus.pureGaugeVanishesClosed = false ∧
                regge4DAlgebraicCloserStatus.plusCrossAgreeClosed = false ∧
                  regge4DAlgebraicCloserStatus.srsConvergesEH4d = false ∧
                    regge4DAlgebraicCloserStatus.gapActionRecovery = false := by
  decide

What this page does not claim

The identity does not prove convergence to the Einstein-Hilbert action in four dimensions. The identity does not establish the full TT isotropy target for all directions and polarizations. The identity does not recover the gap action or flip any OPEN status flag to true.

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: