T2_ratio_is_phi_power

formal source

 100    when `k_b ≥ k_a`).
 101
 102    Stated here with `k_b ≥ k_a` for non-negativity. -/
 103theorem T2_ratio_is_phi_power
 104    (T2_0 : ℝ) (k_a k_b : ℕ) (hT : 0 < T2_0) (h_le : k_a ≤ k_b) :
 105    T2_substrate T2_0 k_a / T2_substrate T2_0 k_b
 106      = Constants.phi ^ (k_b - k_a) := by
 107  unfold T2_substrate
 108  have h_phi_pos := Constants.phi_pos
 109  have h_phi_ne_zero : Constants.phi ≠ 0 := ne_of_gt h_phi_pos
 110  have h_pow_a_ne : Constants.phi ^ k_a ≠ 0 := pow_ne_zero k_a h_phi_ne_zero
 111  have h_pow_b_ne : Constants.phi ^ k_b ≠ 0 := pow_ne_zero k_b h_phi_ne_zero
 112  have hT_ne : T2_0 ≠ 0 := ne_of_gt hT
 113  -- Step 1: rewrite the LHS as φ^k_b / φ^k_a.
 114  have h_lhs : T2_0 / Constants.phi ^ k_a / (T2_0 / Constants.phi ^ k_b)
 115                = Constants.phi ^ k_b / Constants.phi ^ k_a := by
 116    field_simp
 117  rw [h_lhs]
 118  -- Step 2: φ^k_b / φ^k_a = φ^(k_b - k_a) when k_a ≤ k_b.
 119  rw [div_eq_mul_inv]
 120  exact (pow_sub₀ Constants.phi h_phi_ne_zero h_le).symm
 121
 122/-! ## §4. Pre-defined qubit-class Z-rungs (HYPOTHESIS-grade calibration) -/
 123
 124/-- Transmon qubit class — assigned Z-rung 5 (calibration target). -/
 125def z_rung_transmon : ℕ := 5
 126
 127/-- Fluxonium qubit class — assigned Z-rung 6 (calibration target). -/
 128def z_rung_fluxonium : ℕ := 6
 129
 130/-- NV-center qubit class — assigned Z-rung 7 (calibration target). -/
 131def z_rung_NV : ℕ := 7
 132
 133/-- Trapped-ion qubit class — assigned Z-rung 8 (calibration target). -/