Gravity Analysis Regge4 Dalgebraic Closer Full Moment Orbit Contribution Axis Tt

A zero result for one orbit

In the Recognition Science framework's study of gravity, space is built from discrete pieces called hinges, and the framework's machine-checked library of formal theorems tracks how each piece contributes to physical quantities. The declaration fullMomentOrbitContribution_axisTTPlus concerns one such contribution: it proves that for a particular configuration called axisTTPlus, the contribution of any single hinge orbit to a certain zero-momentum moment is exactly zero.

The configuration axisTTPlus is a specific polarization state, one of two standard transverse-traceless modes. The theorem states that for every hinge orbit type, the full moment orbit contribution for this configuration vanishes. This is a concrete algebraic fact, verified by the library's checker, not a numerical approximation. It is one of several banked witnesses: results that are true and proved, but which serve as stepping stones rather than final answers.

The theorem does not claim that the full moment for all configurations vanishes, nor that the framework's discrete gravity matches the continuum theory of general relativity. The library explicitly marks the target of full transverse-traceless isotropy, the agreement between plus and cross polarizations, and the convergence to the Einstein-Hilbert action as open problems. The status flags for these are set to false. The zero result for axisTTPlus is a necessary local check, not a global victory.

What the theorem does establish is a clean, checkable identity: a single orbit's contribution to a specific moment is zero. This is the kind of fact that must hold if a larger theory is to be consistent, and its proof is a small but solid piece of the framework's foundation. It shows the library can handle the algebra of these discrete gravitational objects, even while the big questions remain unanswered.

theorem fullMomentOrbitContribution_axisTTPlus (ty : HingeOrbitType) :
    fullMomentOrbitContribution ty axisTTPlus = 0 :=
  fullMomentOrbitContribution_of_deficit_zero ty _
    (orbitDeficit_dot_axisTTPlus ty)

theorem fullMomentOrbitContribution_axisTTPlus (ty : HingeOrbitType) :
    fullMomentOrbitContribution ty axisTTPlus = 0 :=
  fullMomentOrbitContribution_of_deficit_zero ty _
    (orbitDeficit_dot_axisTTPlus ty)

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

This theorem does not prove that the full moment vanishes for all configurations. This theorem does not establish agreement with general relativity's Einstein-Hilbert action. This theorem does not close the isotropy, gauge-vanishing, or plus-cross agreement targets.

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: