IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbolZero4DKernelCert

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   3
   4/-!
   5# Kernel Int certificate: midpoint Bloch symbolZero quartic coefficients vanish
   6
   7Reuses the banked `KernelCert.couplingZList` (Int-encoded coupling table).
   8Clears denominators by scale 16; the ℚ quartic coefficient is `qNum / 32`.
   9
  10Kernel `decide` only (no `native_decide`).
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Gravity
  15namespace Analysis
  16namespace ReggeExactFlatHessianBlochSymbolZero4D
  17namespace KernelCert
  18
  19open ReggeExactMidpointM2TTIdentity4D.KernelCert
  20  (CZ De Dep couplingZList)
  21
  22set_option maxRecDepth 100000
  23set_option maxHeartbeats 200000000
  24
  25/-- Every Int-encoded coupling denominator divides the fixed scale 16. -/
  26theorem couplingZ_den_dvd_16 : ∀ z ∈ couplingZList, z.den ∣ 16 := by
  27  decide
  28
  29/-- Integer contribution of one coupling to the cleared-denominator quartic
  30coefficient: `num · De_a · De_b · Dep_c · Dep_d · (16/den)`. -/
  31@[inline] def qContrib (z : CZ) (a b c d : Fin 4) : Int :=
  32  z.num * De z a * De z b * Dep z c * Dep z d * (↑(16 / z.den) : Int)
  33
  34/-- Cleared-denominator quartic numerator over the full coupling table. -/
  35def qNum (a b c d : Fin 4) : Int :=
  36  couplingZList.foldl (fun acc z => acc + qContrib z a b c d) 0
  37
  38/-- **THEOREM (kernel):** every cleared-denominator quartic numerator vanishes. -/
  39theorem qNum_eq_zero : ∀ (a b c d : Fin 4), qNum a b c d = 0 := by
  40  decide
  41
  42end KernelCert
  43end ReggeExactFlatHessianBlochSymbolZero4D
  44end Analysis
  45end Gravity
  46end IndisputableMonolith
  47