Gravity Analysis Regge Exact Flat Hessian Bloch M2 Rayleigh4 D Exact Midpoint Bl

A fixed ratio for a gravity residual

In numerical analysis, a residual is the amount by which an approximate solution fails to satisfy an exact equation. The declaration exactMidpointBlochM2_rayleigh_eq_unitFrobeniusTTCoeff is a theorem about one such residual in a 4D gravity model. It states that for any 4x4 matrix H (the Hessian) and any 4-vector k (a wave vector), if three conditions hold, then a specific ratio is exactly -1/8.

The three conditions are: k is a transverse-traceless (TT) mode with respect to H, the squared Frobenius norm of H equals 1 (it is unit-normalized), and the squared norm of k is nonzero. Under these, the theorem proves that the quantity exactMidpointBlochM2 H k divided by the squared wave norm equals -1/8. This is a fixed, algebraic number, not a variable that depends on the specific values of H or k.

The theorem is part of a larger framework called Recognition Science, which uses a machine-checked library of formal theorems to derive physical structure from a ledger of recognition events. In this context, the result is a 'ledger-facing' name for a residual value. The library's audit confirms the proof rests only on the standard axioms of the underlying type theory, with no framework-specific axioms added.

The statement does not claim that this ratio is universal for all possible Hessians and wave vectors. It requires the specific conditions of TT mode, unit Frobenius norm, and nonzero wave norm. It also does not claim that the value -1/8 has any physical meaning in conventional gravity; it is a mathematical property of the specific residual defined in this framework. The theorem is a precise algebraic identity, not a statement about the physical universe.

/-- Unit-Frobenius TT Rayleigh equals the algebraic face `-1/8`. -/
theorem exactMidpointBlochM2_rayleigh_eq_unitFrobeniusTTCoeff
    (H : Mat4) (k : Wave4)
    (hTT : IsTT k H)
    (hF : frobeniusNormSq H = 1)
    (hk : waveNormSq k ≠ 0) :
    exactMidpointBlochM2 H k / waveNormSq k =
      exactHessianM2UnitFrobeniusTTCoeff := by
  have hF' : ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq H = 1 := by
    simpa [frobeniusNormSq_preflight_eq_identity] using hF
  have hk' : ReggeExactMidpointM2TTIdentity4D.waveNormSq k ≠ 0 := by
    simpa [waveNormSq_preflight_eq_identity] using hk
  have h :=
    exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT H k hTT hF' hk'
  simpa [exactHessianM2UnitFrobeniusTTCoeff, waveNormSq_preflight_eq_identity]
    using h

What this page does not claim

This theorem does not claim the -1/8 ratio applies outside the specified conditions of TT mode, unit norm, and nonzero wave norm. This theorem does not claim that -1/8 is a measured or physically observed constant in conventional gravity. This theorem does not claim to derive the value of the fine-structure constant or any other fundamental coupling.

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