module module

`IndisputableMonolith.QFT.VacuumFluctuations`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (19)

theorem energy_time_uncertainty L49
def minEnergyFluctuation L57
def zeroPointEnergy L65
theorem vacuum_has_energy L69
def casimirPressure L87
theorem casimir_is_attractive L90
theorem vacuum_fluctuations_from_discreteness L118
def vacuumEnergyScale L127
def virtualParticleLifetime L137
def virtualParticleInterpretation L144
theorem cosmological_constant_problem L158
theorem rs_resolves_cc_problem L168
def lambShift L182
theorem lamb_shift_from_jcost L187
theorem vacuum_8_tick_interference L199
theorem eight_tick_cancellation_from_foundation L211
theorem eight_tick_cancellation L219
def summary L249
structure VacuumFluctuationsFalsifier L264