IndisputableMonolith.QFT.CasimirNumericalBounds

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Numerical Casimir Bounds
   6
   7This module gives an explicit pressure interval at unit RS separation.  It is
   8deliberately conservative: the upper bound uses only `π < 4`, `ℏ < 1`, and
   9`c = 1`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirNumericalBounds
  15
  16open CasimirPlateModes
  17open Constants
  18
  19noncomputable section
  20
  21/-- Unit RS-native plate separation. -/
  22def unitSeparation : PlateSeparation where
  23  value := 1
  24  pos := by norm_num
  25
  26/-- The positive magnitude of the ideal Casimir pressure at unit separation. -/
  27noncomputable def unitPressureMagnitude : ℝ :=
  28  -idealPressure unitSeparation
  29
  30/-- Unit-separation Casimir pressure magnitude is positive. -/
  31theorem unitPressureMagnitude_pos :
  32    0 < unitPressureMagnitude := by
  33  unfold unitPressureMagnitude
  34  exact neg_pos.mpr (idealPressure_negative unitSeparation)
  35
  36/-- Conservative explicit upper bound at unit RS separation. -/
  37theorem unitPressureMagnitude_lt_one :
  38    unitPressureMagnitude < 1 := by
  39  unfold unitPressureMagnitude idealPressure unitSeparation
  40  simp only
  41  have hpi2 : Real.pi ^ 2 < 16 := by
  42    nlinarith [Real.pi_pos, Real.pi_lt_four]
  43  have hh : hbar < 1 := hbar_lt_one
  44  have hc : c = 1 := rfl
  45  rw [hc]
  46  have hpos : 0 < Real.pi ^ 2 := sq_pos_of_pos Real.pi_pos
  47  have hmul : Real.pi ^ 2 * hbar < 16 := by
  48    nlinarith [hpi2, hbar_pos, hh, hpos]
  49  nlinarith
  50
  51/-- Pressure-interval falsifier at a chosen separation. -/
  52structure PressureIntervalFalsifier where
  53  separation : PlateSeparation
  54  lower : ℝ
  55  upper : ℝ
  56  measuredMagnitude : ℝ
  57  proved_interval : lower < -idealPressure separation ∧ -idealPressure separation < upper
  58  falsifies : Prop := measuredMagnitude ≤ lower ∨ upper ≤ measuredMagnitude
  59
  60/-- The unit-separation falsifier interval. -/
  61def unitPressureInterval (measuredMagnitude : ℝ) : PressureIntervalFalsifier where
  62  separation := unitSeparation
  63  lower := 0
  64  upper := 1
  65  measuredMagnitude := measuredMagnitude
  66  proved_interval := ⟨unitPressureMagnitude_pos, unitPressureMagnitude_lt_one⟩
  67
  68/-- Numerical-bound certificate. -/
  69structure NumericalBoundCert where
  70  unit_interval :
  71    0 < -idealPressure unitSeparation ∧ -idealPressure unitSeparation < 1
  72
  73/-- Certificate instance for the unit-pressure interval. -/
  74def numericalBoundCert : NumericalBoundCert where
  75  unit_interval := ⟨unitPressureMagnitude_pos, unitPressureMagnitude_lt_one⟩
  76
  77end
  78
  79end CasimirNumericalBounds
  80end QFT
  81end IndisputableMonolith
  82