module module

`IndisputableMonolith.Quantum.ClassicalEmergence`

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.Quantum.QMInterpretationStructure module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (21)

def jcostProduct L48
def jcostEntangled L53
theorem entangled_higher_cost L57
theorem cost_difference_scales_quadratically L71
structure PointerState L80
def positionPointer L88
def momentumPointer L94
theorem einselection_from_jcost L101
def decoherenceTime L113
theorem macro_decohere_instant L117
structure QuantumClassicalCrossover L127
theorem classical_from_coarse_graining L146
theorem classical_as_jcost_minimum L155
theorem classical_limit_is_continuum L162
structure NewtonianParticle L170
theorem newton_from_jcost L180
theorem ehrenfest_theorem L189
def predictions L200
def experiments L211
structure EmergenceFalsifier L225
def experimentalStatus L232