pith. machine review for the scientific record. sign in
structure definition def or abbrev

DecoherenceFromBITCert

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)

 162structure DecoherenceFromBITCert where
 163  omega_BIT_band : (7.5 : ℝ) < omega_BIT ∧ omega_BIT < 8.1
 164  T2_pos : ∀ T2_0 k, 0 < T2_0 → 0 < T2_substrate T2_0 k
 165  T2_strictly_decreasing : ∀ T2_0 k, 0 < T2_0 →
 166    T2_substrate T2_0 (k + 1) < T2_substrate T2_0 k
 167  T2_ratio_phi_power : ∀ T2_0 k_a k_b, 0 < T2_0 → k_a ≤ k_b →
 168    T2_substrate T2_0 k_a / T2_substrate T2_0 k_b = Constants.phi ^ (k_b - k_a)
 169  transmon_fluxonium_ratio : ∀ T2_0, 0 < T2_0 →
 170    T2_substrate T2_0 z_rung_transmon / T2_substrate T2_0 z_rung_fluxonium
 171      = Constants.phi ^ 1
 172
 173/-- The master certificate is inhabited. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.