theorem
proved
tactic proof
T2_ratio_is_phi_power
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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). -/