Gravity Analysis Edge Ttdecomposition Closer4 D Decoy Gauge Not Transverse

The non-transverse decoy

In classical general relativity, a gauge choice (a way of fixing coordinate freedom) is often required to be transverse, meaning the gauge field's divergence vanishes. The declaration decoyGauge_not_transverse establishes the opposite for a specific constructed field: it shows that a particular decoy field, built from a longitudinal piece, is not transverse. This is not an accident; it is a deliberate construction. The theorem shows the decoy equals a longitudinal gauge vector, and then uses a prior result to conclude non-transversality.

The purpose sits in a larger proof. The framework's machine-checked library of formal theorems assembles a decomposition called edge_tt_decomposition, which splits a wave into transverse-traceless (TT) parts and a pure-gauge decoy. The non-transverse decoy is the fourth component of that decomposition. The theorem edge_tt_decomposition composes four ingredients: an algebraic TT decomposition, two normalized polarization witnesses, and this non-transverse decoy. The whole assembly inhabits a preflight proposition, meaning it is a preparatory algebraic layer, not the final physical recovery.

The declaration's scope is narrow. It does not claim that all gauge fields are non-transverse, nor that the decoy is physical. It establishes only that this specific constructed field fails the transversality condition. The framework's own docstring is explicit: this is the algebraic and attachment layer for a named closer. Full multi-orbit true-weight continuum recovery remains a separate gate, called S_RS_converges_EH_4d, and the declaration does not touch it.

What the theorem changes is the logical status of the decomposition. Without the non-transverse decoy, the four-part split would be incomplete. With it, the preflight proposition closes. A reader can now see that the framework's edge decomposition deliberately includes a gauge artifact that is not transverse, and that this inclusion is established, not assumed.

theorem decoyGauge_not_transverse :
    ¬ IsTransverse axisWave decoyGauge := by
  rw [decoyGauge_eq_decoyLongitudinal]
  exact decoyLongitudinal_not_transverse

theorem decoyGauge_eq_decoyLongitudinal : decoyGauge = decoyLongitudinal := by
  unfold decoyGauge decoyLongitudinal axisGaugeVector
  funext i j
  fin_cases i <;> fin_cases j <;> simp [gaugePart, axisWave]

/-- **THEOREM (named ledger closer, algebraic+attachment layer).** -/
theorem edge_tt_decomposition :
    Regge4DContinuumPreflight.edge_tt_decomposition := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro m H hH hm
    have hm' : momentumSq m ≠ 0 := by
      simpa [waveNormSq_eq_momentumSq] using hm
    exact exists_edgeTTDecomposition m H hH hm'
  · exact axisTTPlusNormalized_isTTPolarization
  · exact axisTTCrossNormalized_isTTPolarization
  · exact decoyGauge_not_transverse

What this page does not claim

The declaration does not claim that all gauge fields are non-transverse. The declaration does not claim the decoy field represents a physical gravitational mode. The declaration does not establish the full continuum recovery, which remains a separate gate.

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/EdgeTTDecompositionCloser4D.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: