IndisputableMonolith.QFT.CasimirPhiCorrections

   1import Mathlib
   2import IndisputableMonolith.Physics.CasimirEffectCertV2
   3
   4/-!
   5# Phi-Ladder Corrections to Casimir Pressure
   6
   7This module defines the RS correction layer
   8
   9`P_RS(a) = P_Casimir(a) * (1 + δφ)`
  10
  11and proves the algebraic sanity facts.  Actual material response functions are
  12kept as hypotheses until a Lifshitz/dispersive boundary module exists.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace QFT
  17namespace CasimirPhiCorrections
  18
  19open CasimirPlateModes
  20
  21noncomputable section
  22
  23/-- Material boundary families for the correction model. -/
  24inductive MaterialBoundary where
  25  | idealConductor
  26  | finiteConductor
  27  | dielectric
  28  | graphene
  29  | superconductor
  30  | metamaterial
  31  | fluidSeparated
  32  | hydrationLayer
  33  deriving DecidableEq, Repr
  34
  35/-- Geometry families for correction bookkeeping. -/
  36inductive CasimirGeometry where
  37  | parallelPlates
  38  | spherePlate
  39  | cylinderPlate
  40  | corrugated
  41  | sphereSphere
  42  | layeredCavity
  43  deriving DecidableEq, Repr
  44
  45/-- Parameters on which an RS φ-ladder correction may depend. -/
  46structure PhiCorrectionInputs where
  47  separation : PlateSeparation
  48  material : MaterialBoundary
  49  geometry : CasimirGeometry
  50  coatingThickness : ℝ
  51  plasmaWavelength : ℝ
  52  phononBandCenter : ℝ
  53  coherenceLength : ℝ
  54  hydrationThickness : ℝ
  55
  56/-- A model for the φ-ladder correction factor. -/
  57structure PhiCorrectionModel where
  58  deltaPhi : PhiCorrectionInputs → ℝ
  59
  60/-- Corrected RS pressure. -/
  61noncomputable def correctedPressure
  62    (M : PhiCorrectionModel) (x : PhiCorrectionInputs) : ℝ :=
  63  idealPressure x.separation * (1 + M.deltaPhi x)
  64
  65/-- Zero correction recovers the standard ideal Casimir pressure. -/
  66theorem correctedPressure_eq_ideal_of_delta_zero
  67    (M : PhiCorrectionModel) (x : PhiCorrectionInputs)
  68    (hδ : M.deltaPhi x = 0) :
  69    correctedPressure M x = idealPressure x.separation := by
  70  unfold correctedPressure
  71  rw [hδ]
  72  ring
  73
  74/-- Positive `δφ` increases attractive magnitude: pressure becomes more
  75negative than the ideal attractive pressure. -/
  76theorem correctedPressure_more_attractive_of_delta_pos
  77    (M : PhiCorrectionModel) (x : PhiCorrectionInputs)
  78    (hδ : 0 < M.deltaPhi x) :
  79    correctedPressure M x < idealPressure x.separation := by
  80  unfold correctedPressure
  81  have hp : idealPressure x.separation < 0 :=
  82    idealPressure_negative x.separation
  83  have hmul : idealPressure x.separation * M.deltaPhi x < 0 :=
  84    mul_neg_of_neg_of_pos hp hδ
  85  linarith
  86
  87/-- If `-1 < δφ`, the corrected pressure remains attractive. -/
  88theorem correctedPressure_negative_of_delta_gt_neg_one
  89    (M : PhiCorrectionModel) (x : PhiCorrectionInputs)
  90    (hδ : -1 < M.deltaPhi x) :
  91    correctedPressure M x < 0 := by
  92  unfold correctedPressure
  93  have hp : idealPressure x.separation < 0 :=
  94    idealPressure_negative x.separation
  95  have hfactor : 0 < 1 + M.deltaPhi x := by linarith
  96  exact mul_neg_of_neg_of_pos hp hfactor
  97
  98/-- If `δφ < -1`, the correction reverses the sign and produces repulsive
  99pressure in this algebraic model. -/
 100theorem correctedPressure_repulsive_of_delta_lt_neg_one
 101    (M : PhiCorrectionModel) (x : PhiCorrectionInputs)
 102    (hδ : M.deltaPhi x < -1) :
 103    0 < correctedPressure M x := by
 104  unfold correctedPressure
 105  have hp : idealPressure x.separation < 0 :=
 106    idealPressure_negative x.separation
 107  have hfactor : 1 + M.deltaPhi x < 0 := by linarith
 108  exact mul_pos_of_neg_of_neg hp hfactor
 109
 110/-- Material-response hypotheses that must be supplied before claiming an
 111actual device-level correction. -/
 112structure MaterialPhiHypothesis where
 113  model : PhiCorrectionModel
 114  material : MaterialBoundary
 115  geometry : CasimirGeometry
 116  resonance_claim : Prop
 117  falsifier : Prop
 118
 119/-- Per-material ceiling hypothesis: material physics prevents the correction
 120from crossing the repulsive `δφ < -1` threshold. -/
 121structure MaterialCeilingHypothesis where
 122  model : PhiCorrectionModel
 123  epsilon : ℝ
 124  epsilon_pos : 0 < epsilon
 125  epsilon_le_one : epsilon ≤ 1
 126  delta_phi_above_minus_one :
 127    ∀ x : PhiCorrectionInputs, -1 + epsilon ≤ model.deltaPhi x
 128
 129/-- Under a material ceiling, the corrected pressure remains attractive. -/
 130theorem correctedPressure_negative_under_material_ceiling
 131    (H : MaterialCeilingHypothesis) (x : PhiCorrectionInputs) :
 132    correctedPressure H.model x < 0 := by
 133  apply correctedPressure_negative_of_delta_gt_neg_one
 134  have hceil := H.delta_phi_above_minus_one x
 135  linarith [H.epsilon_pos, hceil]
 136
 137/-- Certificate for the theorem-level algebra of φ-corrected pressure. -/
 138structure PhiCorrectionCert where
 139  recovery :
 140    ∀ (M : PhiCorrectionModel) (x : PhiCorrectionInputs),
 141      M.deltaPhi x = 0 →
 142        correctedPressure M x = idealPressure x.separation
 143  enhanced_attraction :
 144    ∀ (M : PhiCorrectionModel) (x : PhiCorrectionInputs),
 145      0 < M.deltaPhi x →
 146        correctedPressure M x < idealPressure x.separation
 147  remains_attractive :
 148    ∀ (M : PhiCorrectionModel) (x : PhiCorrectionInputs),
 149      -1 < M.deltaPhi x →
 150        correctedPressure M x < 0
 151  sign_reversal :
 152    ∀ (M : PhiCorrectionModel) (x : PhiCorrectionInputs),
 153      M.deltaPhi x < -1 →
 154        0 < correctedPressure M x
 155  ceiling_constrained_attraction :
 156    ∀ (H : MaterialCeilingHypothesis) (x : PhiCorrectionInputs),
 157      correctedPressure H.model x < 0
 158
 159/-- The φ-correction algebra certificate. -/
 160def phiCorrectionCert : PhiCorrectionCert where
 161  recovery := correctedPressure_eq_ideal_of_delta_zero
 162  enhanced_attraction := correctedPressure_more_attractive_of_delta_pos
 163  remains_attractive := correctedPressure_negative_of_delta_gt_neg_one
 164  sign_reversal := correctedPressure_repulsive_of_delta_lt_neg_one
 165  ceiling_constrained_attraction := correctedPressure_negative_under_material_ceiling
 166
 167end
 168
 169end CasimirPhiCorrections
 170end QFT
 171end IndisputableMonolith
 172