Gravity Analysis Regge4 Dalgebraic Closer Decoy One Orbit M2 Ne Eh Coefficient

A decoy check in the 4D gravity program

The declaration decoy_one_orbit_m2_ne_eh_coefficient is a deliberately constructed test within a larger program that aims to derive general relativity from a discrete structure. The program works with a lattice-like model where space-time is built from elementary units, and it seeks to show that, at large scales, the model reproduces the Einstein-Hilbert action, the classical starting point for general relativity. The specific declaration examines a simplified, one-orbit case and proves that this case produces a value of -3 for a particular quantity, the m² symbol, a measure of a mode's squared mass-like contribution. This is sharply different from the target Einstein-Hilbert coefficient of -1/4. The theorem, checked by a machine, states these two values are unequal, confirming that the simplified case does not accidentally match the desired continuum result.

The purpose of this decoy is to act as a negative control. In scientific testing, a decoy is a case designed to fail, to ensure that the methods are sensitive enough to detect a discrepancy. Here, the one-orbit case is not expected to reproduce the full theory; it is a stripped-down scenario used to verify that the algebraic machinery correctly identifies when a result is off-target. The theorem's proof is a direct computation, and the declaration also records that this failure does not by itself overturn the program's main goals. The status flags in the same module explicitly mark the full isotropy target, the pure-gauge vanishing target, and the plus-cross agreement target as still open, meaning they are not yet proved. The decoy result is a banked fact, a known negative that future work must account for, not a step toward the final derivation.

What the declaration does not claim is as important as what it proves. It does not prove that the full 4D model fails to converge to the Einstein-Hilbert action; that question, named S_RS_converges_EH_4d, remains open. It does not establish that the decoy case is physically relevant or that its failure indicates a problem with the overall approach. The decoy is one specific, simplified orbit, and its mismatch with the continuum target is a deliberate feature of the test, not a discovered flaw. The declaration also does not claim that the full isotropy of gravitational waves, the agreement between plus and cross polarizations, or the vanishing of pure-gauge modes has been achieved; all of these are explicitly listed as open targets with status false.

In plain terms, this declaration is a checkpoint in a long and unfinished derivation. It confirms that the algebraic tools can compute a value and compare it against a target, and it records a known failure in a controlled case. The work of bridging the gap between the discrete model and continuous general relativity remains incomplete, and this decoy is a documented marker of how far the program has yet to go.

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

def regge4DAlgebraicCloserStatus : Regge4DAlgebraicCloserStatus where
  decoyOneOrbitClosed := true
  plusCrossWitnessesClosed := true
  gaugeM2SymbolClosed := true
  fullMomentZeroMomClosed := true
  fullTTIsotropyClosed := false
  pureGaugeVanishesClosed := false
  plusCrossAgreeClosed := false
  srsConvergesEH4d := false
  gapActionRecovery := false

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 declaration does not prove that the full 4D model fails to converge to general relativity. This declaration does not establish that the one-orbit case is physically relevant. This declaration does not prove any of the open isotropy, gauge, 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: