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

decoherence_from_BIT_one_statement

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)

 189theorem decoherence_from_BIT_one_statement :
 190    -- (1) Carrier in band.
 191    ((7.5 : ℝ) < omega_BIT ∧ omega_BIT < 8.1) ∧
 192    -- (2) `T₂` strictly decreasing in Z-rung.
 193    (∀ T2_0 k, 0 < T2_0 →
 194      T2_substrate T2_0 (k + 1) < T2_substrate T2_0 k) ∧
 195    -- (3) Cross-class ratio is a φ-power.
 196    (∀ T2_0 k_a k_b, 0 < T2_0 → k_a ≤ k_b →
 197      T2_substrate T2_0 k_a / T2_substrate T2_0 k_b = Constants.phi ^ (k_b - k_a)) :=

proof body

Term-mode proof.

 198  ⟨omega_BIT_band, T2_substrate_strictly_decreasing, T2_ratio_is_phi_power⟩
 199
 200end
 201
 202end DecoherenceFromBIT
 203end QuantumComputing
 204end IndisputableMonolith

depends on (19)

Lean names referenced from this declaration's body.