module module

`IndisputableMonolith.Physics.CasimirTechnologyCertificates`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.QFT.CasimirPhiCorrections module_import

declarations in this module (19)

inductive CasimirTechnology L23
theorem technologyFamilyCount L35
def technologyStatus L41
structure TechnologyFalsifier L45
structure TechnologyClaim L51
def WellTaggedTechnologyClaim L61
theorem default_status_well_tagged L65
def RepulsiveBearingCondition L81
theorem repulsive_bearing_pressure_positive L86
def MemsAntiStictionCondition L94
theorem mems_antistiction_remains_attractive L100
structure DynamicCasimirCondition L107
structure QubitShieldCondition L114
structure BoundaryCatalysisCondition L123
structure ThermalDiodeCondition L132
structure MetrologyCondition L139
structure MicroActuatorCondition L146
structure TechnologyCert L152
def technologyCert L173