Gravity Analysis Regge4 Dalgebraic Closer Banked Does Not Flip Gap Or Isotropy

The banked verdict

The declaration banked_does_not_flip_gap_or_isotropy is a formal theorem in the framework's machine-checked library of formal theorems. It records a precise status report for a four-dimensional gravity calculation, naming what has been proven and what has not. The theorem's content is a conjunction of three facts: the full isotropy target is not closed, the gap action recovery is not achieved, and a specific one-orbit symbol does not equal the Einstein-Hilbert coefficient.

In plain terms, the calculation concerns how a discrete structure, a ledger of recognition events, might reproduce the behavior of continuous gravity. The theorem states that the work has banked some algebraic identities, but it has not yet shown that the full symmetry of the theory, isotropy, holds, nor that the gap action is recovered. The third fact is a concrete numerical mismatch: the one-orbit symbol for the axis plus polarization is -3, while the Einstein-Hilbert coefficient is -1/4.

The theorem is a negative result in the sense that it explicitly denies two major goals. It proves that the status flags for full isotropy and gap action recovery are both false. This is not a failure of the framework; it is an honest accounting of what remains open. The declaration does not claim that the framework has failed, only that these specific targets are not yet met.

What the theorem does establish is that certain algebraic witnesses are closed. It proves that the plus and cross polarizations are valid transverse-traceless witnesses, that the gauge symbol vanishes on a decoy, and that the full zero-momentum moment object vanishes on axis plus and decoy gauge. These are banked results, but they do not imply the full isotropy target.

The theorem's role is to prevent overclaiming. It is a formal guard that says: the work is not done, the gap is not flipped, and the isotropy is not proven. This is a valuable contribution because it keeps the framework's claims honest and precise.

/-- Honesty: banked one-orbit identities do not inhabit the OPEN isotropy
target, and the ledger flag stays false. -/
theorem banked_does_not_flip_gap_or_isotropy :
    regge4DAlgebraicCloserStatus.fullTTIsotropyClosed = false ∧
      regge4DAlgebraicCloserStatus.gapActionRecovery = false ∧
        ReggeBlochM2Symbol4D.m2Symbol axisTTPlus ≠
          einsteinHilbertTTCoefficient4D := by
  refine ⟨rfl, rfl, ?_⟩
  rw [m2Symbol_axisTTPlus, einsteinHilbertTTCoefficient4D_eq]
  norm_num

/-- Honesty: banked one-orbit identities do not inhabit the OPEN isotropy
target, and the ledger flag stays false. -/
theorem banked_does_not_flip_gap_or_isotropy :
    regge4DAlgebraicCloserStatus.fullTTIsotropyClosed = false ∧
      regge4DAlgebraicCloserStatus.gapActionRecovery = false ∧
        ReggeBlochM2Symbol4D.m2Symbol axisTTPlus ≠
          einsteinHilbertTTCoefficient4D := by
  refine ⟨rfl, rfl, ?_⟩
  rw [m2Symbol_axisTTPlus, einsteinHilbertTTCoefficient4D_eq]
  norm_num

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

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 theorem does not prove that the framework fails to reproduce gravity. The theorem does not claim that the banked algebraic identities are sufficient for the full isotropy target. The theorem does not state that the gap action recovery is impossible, only that it is not currently achieved.

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: