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

born_normalization

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)

 100theorem born_normalization (theta : ℝ) :
 101    Real.sin theta ^ 2 + Real.cos theta ^ 2 = 1 :=

proof body

Term-mode proof.

 102  Real.sin_sq_add_cos_sq theta
 103
 104/-! ## Mesoscopic Threshold -/
 105
 106/-- The mesoscopic threshold: the mass at which A ≈ 1 (the transition
 107    between quantum coherence and classical behavior).
 108
 109    m_coh ≈ 0.2 ng = 2e-13 kg for τ ≈ 1 s.
 110
 111    Below m_coh: quantum superpositions survive (A << 1)
 112    Above m_coh: rapid decoherence (A >> 1) -/

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.