DecoherenceFromBITCert

formal source

 159    3. `T₂(k)` is strictly decreasing in `k`.
 160    4. The cross-class ratio is `φ^(k_b - k_a)` for any `k_a ≤ k_b`.
 161    5. The transmon-fluxonium ratio is exactly `φ`. -/
 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. -/
 174def decoherenceFromBITCert : DecoherenceFromBITCert where
 175  omega_BIT_band := omega_BIT_band
 176  T2_pos := T2_substrate_pos
 177  T2_strictly_decreasing := T2_substrate_strictly_decreasing
 178  T2_ratio_phi_power := T2_ratio_is_phi_power
 179  transmon_fluxonium_ratio := T2_transmon_to_fluxonium_ratio
 180
 181/-! ## §6. One-statement summary -/
 182
 183/-- **DECOHERENCE FROM BIT ONE-STATEMENT THEOREM.**
 184
 185    Under the BIT-coupling decoherence model:
 186    (1) the canonical BIT carrier sits in the `(8.0, 8.1)` band;
 187    (2) substrate decoherence times follow `T₂(k) = T₂_0 / φ^k`;
 188    (3) cross-class ratios are exact `φ`-powers `φ^(k_b - k_a)`. -/
 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.