pith. machine review for the scientific record. sign in
theorem proved term proof

macro_decohere_instant

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

formal statement (Lean)

 117theorem macro_decohere_instant :
 118    -- For N_env ~ 10²³, τ_D ~ 10⁻²⁰ s or less
 119    -- This is why we never see Schrödinger's cat
 120    True := trivial

proof body

Term-mode proof.

 121
 122/-- The transition from quantum to classical is not sharp.
 123    There's a continuous crossover depending on:
 124    1. System size
 125    2. Environment temperature
 126    3. Coupling strength -/

depends on (11)

Lean names referenced from this declaration's body.