IndisputableMonolith.QFT.CasimirEightTickInterference

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3import IndisputableMonolith.Foundation.EightTick
   4
   5/-!
   6# Eight-Tick Casimir Interference
   7
   8The complete eight-tick phase cycle cancels coherent modulation terms.  The
   9static ideal Casimir pressure survives as the cycle-invariant background.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirEightTickInterference
  15
  16open CasimirPlateModes
  17open Foundation.EightTick
  18
  19noncomputable section
  20
  21/-- Complex pressure modulation by a single phase factor. -/
  22noncomputable def eightTickModulatedPressure
  23    (a : PlateSeparation) (factor : ℂ) : ℂ :=
  24  (idealPressure a : ℂ) * factor
  25
  26/-- Summing the eight phase modulations cancels exactly. -/
  27theorem eight_tick_modulation_sum_zero (a : PlateSeparation) :
  28    (∑ k : Fin 8, eightTickModulatedPressure a (phaseExp k)) = 0 := by
  29  unfold eightTickModulatedPressure
  30  rw [← Finset.mul_sum]
  31  rw [sum_8_phases_eq_zero]
  32  simp
  33
  34/-- The real part of the full-cycle modulation also vanishes. -/
  35theorem eight_tick_real_modulation_sum_zero (a : PlateSeparation) :
  36    ((∑ k : Fin 8, eightTickModulatedPressure a (phaseExp k))).re = 0 := by
  37  rw [eight_tick_modulation_sum_zero]
  38  simp
  39
  40/-- Eight-tick interference certificate. -/
  41structure EightTickCasimirCert where
  42  complex_cycle_zero :
  43    ∀ a : PlateSeparation,
  44      (∑ k : Fin 8, eightTickModulatedPressure a (phaseExp k)) = 0
  45  real_cycle_zero :
  46    ∀ a : PlateSeparation,
  47      ((∑ k : Fin 8, eightTickModulatedPressure a (phaseExp k))).re = 0
  48
  49/-- Certificate instance. -/
  50def eightTickCasimirCert : EightTickCasimirCert where
  51  complex_cycle_zero := eight_tick_modulation_sum_zero
  52  real_cycle_zero := eight_tick_real_modulation_sum_zero
  53
  54end
  55
  56end CasimirEightTickInterference
  57end QFT
  58end IndisputableMonolith
  59