IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochM2Rayleigh4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
   6import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   7
   8/-!
   9# Exact midpoint Bloch m² Rayleigh = algebraic faces (R3)
  10
  11Inhabits `TypedResidual_m2_rayleigh_eq_algebraic_face`:
  12
  13* unit-Frobenius TT: `exactMidpointBlochM2 H k / |k|² = -1/8`
  14* pure gauge: `exactMidpointBlochM2 (pureGaugeFamily m v) m / |m|² = 0`
  15
  16Certificate lives in `ReggeExactMidpointM2TTIdentity4D` (rational packed
  17biquadratic table + `native_decide` + closed-form transport).  This module
  18is the ledger-facing name matching SymbolZero4D / the handoff residual R3.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Gravity
  23namespace Analysis
  24namespace ReggeExactFlatHessianBlochM2Rayleigh4D
  25
  26open Regge4DContinuumPreflight
  27open ReggeExactFlatHessianSymbol4D
  28  (exactHessianM2UnitFrobeniusTTCoeff exactHessianM2GaugeCoeff)
  29open ReggeExactFlatHessianBlochSymbol4D
  30open EdgeTTDecomposition4D
  31open ReggeExactMidpointM2TTIdentity4D
  32  (exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT
  33    exactMidpointBlochM2_gauge_rayleigh_eq_zero)
  34
  35noncomputable section
  36
  37/-- Disambiguate shared aliases after multi-module opens. -/
  38abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  39abbrev Wave4 := Regge4DContinuumPreflight.Wave4
  40
  41private theorem frobeniusNormSq_preflight_eq_identity (H : Mat4) :
  42    Regge4DContinuumPreflight.frobeniusNormSq H =
  43      ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq H :=
  44  rfl
  45
  46private theorem waveNormSq_preflight_eq_identity (k : Wave4) :
  47    Regge4DContinuumPreflight.waveNormSq k =
  48      ReggeExactMidpointM2TTIdentity4D.waveNormSq k :=
  49  rfl
  50
  51/-- Unit-Frobenius TT Rayleigh equals the algebraic face `-1/8`. -/
  52theorem exactMidpointBlochM2_rayleigh_eq_unitFrobeniusTTCoeff
  53    (H : Mat4) (k : Wave4)
  54    (hTT : IsTT k H)
  55    (hF : frobeniusNormSq H = 1)
  56    (hk : waveNormSq k ≠ 0) :
  57    exactMidpointBlochM2 H k / waveNormSq k =
  58      exactHessianM2UnitFrobeniusTTCoeff := by
  59  have hF' : ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq H = 1 := by
  60    simpa [frobeniusNormSq_preflight_eq_identity] using hF
  61  have hk' : ReggeExactMidpointM2TTIdentity4D.waveNormSq k ≠ 0 := by
  62    simpa [waveNormSq_preflight_eq_identity] using hk
  63  have h :=
  64    exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT H k hTT hF' hk'
  65  simpa [exactHessianM2UnitFrobeniusTTCoeff, waveNormSq_preflight_eq_identity]
  66    using h
  67
  68/-- Pure-gauge Rayleigh equals the algebraic face `0`. -/
  69theorem exactMidpointBlochM2_rayleigh_eq_gaugeCoeff
  70    (m v : Wave4) (hm : waveNormSq m ≠ 0) :
  71    exactMidpointBlochM2 (pureGaugeFamily m v) m / waveNormSq m =
  72      exactHessianM2GaugeCoeff := by
  73  have hm' : ReggeExactMidpointM2TTIdentity4D.waveNormSq m ≠ 0 := by
  74    simpa [waveNormSq_preflight_eq_identity] using hm
  75  have h := exactMidpointBlochM2_gauge_rayleigh_eq_zero m v hm'
  76  simpa [pureGaugeFamily, exactHessianM2GaugeCoeff,
  77    waveNormSq_preflight_eq_identity] using h
  78
  79/-- Packaged algebraic faces matching residual R3. -/
  80theorem exactMidpointBlochM2_rayleigh_eq_algebraic_face :
  81    (∀ (H : Mat4) (k : Wave4),
  82        IsTT k H →
  83          frobeniusNormSq H = 1 →
  84            waveNormSq k ≠ 0 →
  85              exactMidpointBlochM2 H k / waveNormSq k =
  86                exactHessianM2UnitFrobeniusTTCoeff) ∧
  87      (∀ (m : Wave4) (v : Wave4),
  88        waveNormSq m ≠ 0 →
  89          exactMidpointBlochM2 (pureGaugeFamily m v) m / waveNormSq m =
  90            exactHessianM2GaugeCoeff) :=
  91  ⟨exactMidpointBlochM2_rayleigh_eq_unitFrobeniusTTCoeff,
  92    exactMidpointBlochM2_rayleigh_eq_gaugeCoeff⟩
  93
  94/-- Ledger-facing inhabit of R3 (same Prop shape as
  95`SRSConvergesEH4D.TypedResidual_m2_rayleigh_eq_algebraic_face`). -/
  96theorem typedResidual_m2_rayleigh_eq_algebraic_face :
  97    (∀ (H : Mat4) (k : Wave4),
  98        IsTT k H →
  99          frobeniusNormSq H = 1 →
 100            waveNormSq k ≠ 0 →
 101              exactMidpointBlochM2 H k / waveNormSq k =
 102                exactHessianM2UnitFrobeniusTTCoeff) ∧
 103      (∀ (m : Wave4) (v : Wave4),
 104        waveNormSq m ≠ 0 →
 105          exactMidpointBlochM2 (pureGaugeFamily m v) m / waveNormSq m =
 106            exactHessianM2GaugeCoeff) :=
 107  exactMidpointBlochM2_rayleigh_eq_algebraic_face
 108
 109end
 110
 111end ReggeExactFlatHessianBlochM2Rayleigh4D
 112end Analysis
 113end Gravity
 114end IndisputableMonolith
 115