Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 D Exact Midpoint M2 Ttident

The exact midpoint identity

In the mathematics of gravity, one often studies small ripples in spacetime by looking at a quantity called the wave's squared norm, a sum of the squares of its four components. The declaration in question, exactMidpointM2TTIdentityProved_true, is a machine-checked proof that a specific, complicated expression, the exact midpoint Bloch m² term, equals exactly negative one eighth of the wave's squared norm times the squared norm of the gravitational field, but only when the field and wave satisfy a condition called being transverse and traceless.

This condition, IsTT, is a standard one in general relativity: it means the field has no components along the wave's direction of travel and its trace is zero. The theorem, exactMidpointBlochM2_eq_neg_eighth_frobenius_tt, states this equality. A companion result, exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT, divides both sides by the wave's squared norm, yielding the constant negative one eighth, a number that appears naturally in the framework's analysis of gravitational wave energy.

The proof is not a numerical approximation. It is a formal derivation in a machine-checked library of formal theorems, built from exact rational arithmetic. The coefficients in the expression are defined as rational numbers, and the proof verifies the identity by rewriting the expression step by step, using symmetries of the coefficients and the transverse-traceless condition. The declaration exactMidpointM2TTIdentityProved_true is a boolean flag set to true by this proof, a compact certificate that the identity has been established.

What this does not claim is broader physical significance. It does not say that this identity holds for all fields and waves, only for those that are transverse and traceless. It does not assert that this expression represents the actual energy of a gravitational wave in the framework, only that a particular mathematical expression simplifies under a specific condition. The identity is a lemma, not a physical law, and the framework's library does not use it to derive any further results in this file.

theorem exactMidpointM2TTIdentityProved_true :
    ExactMidpointM2TTIdentityProved = true := rfl

/-- **Typed blocker `exact_midpoint_m2_tt_identity`, closed.**  For TT pairs
the exact midpoint Bloch m^2 equals `-(1/8) |H|_F^2 |k|^2`. -/
theorem exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
    (H : Mat4) (k : Wave4) (hTT : IsTT k H) :
    exactMidpointBlochM2 H k =
      (-(1 / 8) : ℝ) * frobeniusNormSq H * waveNormSq k := by
  rw [exactMidpointBlochM2_eq_closedForm_of_symmetric H k hTT.1,
    closedForm_eq_neg_eighth_of_TT H k hTT]

/-- Unit-Frobenius TT Rayleigh face `-1/8`. -/
theorem exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT
    (H : Mat4) (k : Wave4) (hTT : IsTT k H)
    (hF : frobeniusNormSq H = 1) (hk : waveNormSq k ≠ 0) :
    exactMidpointBlochM2 H k / waveNormSq k = (-(1 / 8) : ℝ) := by
  rw [exactMidpointBlochM2_eq_neg_eighth_frobenius_tt H k hTT, hF]
  field_simp [hk]

What this page does not claim

The identity holds for all fields and waves, not just those that are transverse and traceless. The exact midpoint Bloch m² term is the actual energy of a gravitational wave in the framework. The framework's library uses this identity to derive further physical results.

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