IndisputableMonolith.QFT.CasimirTorque

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Casimir Torque
   6
   7Anisotropic boundaries produce a torque from angularly dependent mode
   8admissibility.  This module formalizes the standard sinusoidal structural law.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace QFT
  13namespace CasimirTorque
  14
  15open CasimirPlateModes
  16
  17noncomputable section
  18
  19/-- Structural anisotropic Casimir torque law. -/
  20noncomputable def casimirTorque (beta : ℝ) (a : PlateSeparation) (theta : ℝ) : ℝ :=
  21  beta * idealEnergyDensity a * Real.sin (2 * theta)
  22
  23/-- Aligned anisotropic plates have zero torque. -/
  24theorem torque_zero_at_aligned (beta : ℝ) (a : PlateSeparation) :
  25    casimirTorque beta a 0 = 0 := by
  26  unfold casimirTorque
  27  simp
  28
  29/-- Orthogonal alignment also has zero torque in the `sin(2θ)` structural law. -/
  30theorem torque_zero_at_orthogonal (beta : ℝ) (a : PlateSeparation) :
  31    casimirTorque beta a (Real.pi / 2) = 0 := by
  32  unfold casimirTorque
  33  rw [show 2 * (Real.pi / 2) = Real.pi by ring]
  34  simp
  35
  36/-- Quarter-turn alignment evaluates to the full anisotropic amplitude. -/
  37theorem torque_at_quarter_turn (beta : ℝ) (a : PlateSeparation) :
  38    casimirTorque beta a (Real.pi / 4) = beta * idealEnergyDensity a := by
  39  unfold casimirTorque
  40  rw [show 2 * (Real.pi / 4) = Real.pi / 2 by ring]
  41  rw [Real.sin_pi_div_two]
  42  ring
  43
  44/-- Torque certificate. -/
  45structure CasimirTorqueCert where
  46  aligned_zero : ∀ beta a, casimirTorque beta a 0 = 0
  47  orthogonal_zero : ∀ beta a, casimirTorque beta a (Real.pi / 2) = 0
  48  quarter_turn_value :
  49    ∀ beta a, casimirTorque beta a (Real.pi / 4) = beta * idealEnergyDensity a
  50
  51/-- Certificate instance. -/
  52def casimirTorqueCert : CasimirTorqueCert where
  53  aligned_zero := torque_zero_at_aligned
  54  orthogonal_zero := torque_zero_at_orthogonal
  55  quarter_turn_value := torque_at_quarter_turn
  56
  57end
  58
  59end CasimirTorque
  60end QFT
  61end IndisputableMonolith
  62