Gravity Analysis Regge4 Dalgebraic Closer Full Moment Orbit Contribution Decoy G

The decoy gauge test

The declaration fullMomentOrbitContribution_decoyGauge is a theorem in the framework's machine-checked library of formal theorems. It concerns a specific test configuration called the decoy gauge, one of several trial states used in a four-dimensional gravitational analysis. The theorem states that for every orbit type in a discrete classification of hinge orbits, the contribution of the decoy gauge to a particular quadratic moment is exactly zero.

This moment, called the full-moment orbit contribution, is a bookkeeping device: it sums a certain squared quantity over the orbit types to measure how much a configuration resembles a physical gravitational wave. The theorem proves that the decoy gauge, despite being a candidate, contributes nothing to this sum. The proof works by showing the decoy gauge lies in the kernel of the relevant bilinear form, so its contribution vanishes identically.

The result is a banked witness, not a physical conclusion. It confirms that the decoy gauge is algebraically inert for this particular moment, but it does not establish that the decoy gauge is physical, nor that it matches the Einstein-Hilbert coefficient of -1/4. The library explicitly marks the full isotropy target, the pure-gauge vanishing target, and the plus-cross agreement target as open propositions with status flag false. The theorem also does not prove convergence of the recognition-science action to the Einstein-Hilbert action in four dimensions, and it does not flip the gap action recovery flag.

What the declaration does is narrow the search: among the candidate configurations, the decoy gauge is excluded from contributing to this moment, leaving the physically relevant candidates to be identified by further work. The machine-checked status record confirms that the decoy one-orbit symbol equals -3, not the continuum target of -1/4, so the decoy is a deliberate mismatch used to test the algebraic machinery.

The theorem is one of several closed results in a module that also proves the plus and cross normalized witnesses are transverse-traceless polarizations, and that the gauge m2 symbol vanishes on the decoy. These are algebraic facts about the test configurations, not statements about physical spacetime.

theorem fullMomentOrbitContribution_decoyGauge (ty : HingeOrbitType) :
    fullMomentOrbitContribution ty decoyGauge = 0 :=
  fullMomentOrbitContribution_of_deficit_zero ty _
    (orbitDeficit_dot_decoyGauge ty)

/-- Per-orbit deficit annihilation implies per-orbit contribution zero. -/
theorem fullMomentOrbitContribution_of_deficit_zero
    (ty : HingeOrbitType) (H : Mat4)
    (h : classDot (orbitDeficitKernel ty) H = 0) :
    fullMomentOrbitContribution ty H = 0 := by
  unfold fullMomentOrbitContribution orbitZeroMomQuadratic
  rw [h, mul_zero]

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

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

What this page does not claim

The decoy gauge is a physical gravitational configuration. The full-moment sum over all orbit types equals the Einstein-Hilbert coefficient for any direction. The recognition-science action converges to the Einstein-Hilbert action in four dimensions.

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: