IndisputableMonolith.QFT.CasimirRoughness

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Roughness and Corrugation Correction
   6
   7Surface roughness and corrugation are represented by a first nonzero quadratic
   8correction in the dimensionless amplitude `h/a`.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace QFT
  13namespace CasimirRoughness
  14
  15open CasimirPlateModes
  16
  17noncomputable section
  18
  19/-- Structural roughness coefficient. -/
  20noncomputable def roughnessCoefficient : ℝ := 1
  21
  22/-- Roughness-corrected pressure. -/
  23noncomputable def roughnessCorrectedPressure (h : ℝ) (a : PlateSeparation) : ℝ :=
  24  idealPressure a * (1 + roughnessCoefficient * (h / a.value) ^ 2)
  25
  26/-- Zero roughness recovers the ideal pressure. -/
  27theorem roughness_zero_recovers_ideal (a : PlateSeparation) :
  28    roughnessCorrectedPressure 0 a = idealPressure a := by
  29  unfold roughnessCorrectedPressure
  30  ring
  31
  32/-- Zero roughness coefficient recovers the ideal pressure. -/
  33theorem roughness_zero_coefficient (h : ℝ) (a : PlateSeparation)
  34    (hcoef : roughnessCoefficient = 0) :
  35    roughnessCorrectedPressure h a = idealPressure a := by
  36  unfold roughnessCorrectedPressure
  37  rw [hcoef]
  38  ring
  39
  40/-- Roughness correction certificate. -/
  41structure RoughnessCert where
  42  zero_roughness :
  43    ∀ a : PlateSeparation, roughnessCorrectedPressure 0 a = idealPressure a
  44  zero_coefficient :
  45    ∀ (h : ℝ) (a : PlateSeparation), roughnessCoefficient = 0 →
  46      roughnessCorrectedPressure h a = idealPressure a
  47
  48/-- Certificate instance. -/
  49def roughnessCert : RoughnessCert where
  50  zero_roughness := roughness_zero_recovers_ideal
  51  zero_coefficient := roughness_zero_coefficient
  52
  53end
  54
  55end CasimirRoughness
  56end QFT
  57end IndisputableMonolith
  58