module module

`IndisputableMonolith.QFT.CasimirPlateModes`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.CasimirEffectCertV2 module_import
IndisputableMonolith.QFT.CasimirEightTickInterference module_import
IndisputableMonolith.QFT.CasimirLifshitz module_import
IndisputableMonolith.QFT.CasimirNumericalBounds module_import
IndisputableMonolith.QFT.CasimirPolderAtomSurface module_import
IndisputableMonolith.QFT.CasimirRecognitionBoundary module_import
IndisputableMonolith.QFT.CasimirRoughness module_import
IndisputableMonolith.QFT.CasimirStabilityBound module_import
IndisputableMonolith.QFT.CasimirThermal module_import
IndisputableMonolith.QFT.CasimirTorque module_import
IndisputableMonolith.QFT.CasimirZetaRegularization module_import
IndisputableMonolith.QFT.VacuumFluctuations module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (18)

structure PlateSeparation L22
def transverseWaveNumber L29
def modeFrequency L35
def zeroPointModeEnergy L39
def idealEnergyCoefficient L44
def idealEnergyDensity L49
def idealEnergyDerivative L54
def idealPressure L58
theorem idealEnergyCoefficient_pos L62
theorem idealEnergyDerivative_pos L69
theorem idealPressure_eq_neg_energyDerivative L77
theorem idealPressure_negative L83
theorem neg_idealPressure_eq_derivative L89
theorem idealPressure_fourth_power_scaling L96
theorem idealPressure_hbar_phi_form L106
theorem idealPressure_ne_zero L113
structure IdealPlateCert L118
def idealPlateCert L132