module module

`IndisputableMonolith.QFT.Decoherence`

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

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

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Flight.GravityBridge module_import

declarations in this module (25)

def tau0_seconds L55
def phi L58
def gap45 L61
def tau_planck L64
def tau_bio L67
def timescale_gap_log10 L73
theorem gap_range L76
structure EnvironmentCoupling L83
def decoherenceTime L93
theorem decoherence_decreases_with_modes L97
theorem decoherence_decreases_with_coupling L117
def isQuantum L141
def isClassical L145
theorem quantum_classical_dichotomy L149
def criticalModes L159
theorem critical_modes_specification L167
structure QubitParams L177
def typicalSCQubit L188
def predictedQubitDecoherence L196
def gap45CrossoverModes L204
def gap45CrossoverApprox L215
theorem gap45_crossover_range L218
inductive DecoherenceStrategy L226
def strategyImprovement L234
structure DecoherenceFalsifier L247