def
definition
decoherenceFromBITCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QuantumComputing.DecoherenceFromBIT on GitHub at line 174.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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.
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)) :=
198 ⟨omega_BIT_band, T2_substrate_strictly_decreasing, T2_ratio_is_phi_power⟩
199
200end
201
202end DecoherenceFromBIT
203end QuantumComputing
204end IndisputableMonolith