module module

`IndisputableMonolith.Physics.CasimirEffectCertV2`

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 (2)

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

IndisputableMonolith.Gravity.RunningG module_import
IndisputableMonolith.QFT.CasimirPhiCorrections module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.CasimirEffectFromRS module_import
IndisputableMonolith.QFT.CasimirPlateModes module_import
IndisputableMonolith.QFT.CasimirRecognitionBoundary module_import

declarations in this module (14)

inductive ClaimStatus L29
structure PressureLawFalsifier L38
structure SignFalsifier L47
def geometryStatus L54
theorem geometry_count_retained L63
theorem factor_720_as_8tick_times_fermion_dof L69
theorem parallel_plate_status L74
theorem corrugated_status L80
structure CasimirV2Cert L85
def cert L98
theorem cert_inhabited L107
theorem cert_recovers_attraction L110
theorem cert_recovers_boundary_cost_nonneg L115
theorem cert_recovers_phi_hbar_pressure L120