T2_ratio_is_phi_power
Under the BIT-coupling decoherence model the ratio of substrate decoherence times at Z-rungs k_a and k_b equals phi to the power of their difference when k_a is at most k_b. Researchers working on qubit decoherence channels in quantum hardware would invoke this identity to relate measured T2 values across device families. The proof unfolds the explicit form of the substrate decoherence function and reduces the ratio via field simplification and the power-subtraction identity for positive bases.
claimLet $T_{2,0}>0$ and let $k_a,k_b$ be natural numbers with $k_a≤k_b$. Then $T_2(k_a)/T_2(k_b)=φ^{k_b-k_a}$, where the substrate decoherence time is defined by $T_2(k):=T_{2,0}/φ^k$.
background
The module establishes decoherence channels arising from coupling to the bosonic identity theorem carrier at frequency 5φ. The key auxiliary definition is the substrate decoherence time T2_substrate(T2_0,k) which equals T2_0 divided by φ to the power k; higher rung strengthens the coupling and shortens the coherence time. Upstream results supply the positivity of φ and the rung maps used to assign integer labels to qubit classes such as transmon and fluxonium. The local setting is the algebraic structure of the φ-power ratio under the BIT model, with Z-rung assignments treated as empirical hypotheses.
proof idea
The tactic proof first unfolds the definition of T2_substrate on both sides. It then records positivity of φ and nonzeroness of the relevant powers together with the base T2_0. A field_simp step rewrites the left-hand side ratio into φ to the k_b over φ to the k_a. The final step invokes div_eq_mul_inv followed by the symmetric form of pow_sub_0 under the assumption k_a ≤ k_b.
why it matters in Recognition Science
This algebraic identity is invoked by the master certificate decoherenceFromBITCert and by the one-statement theorem decoherence_from_BIT_one_statement that packages the full BIT-decoherence claim. It supplies the exact φ-power ratios used in the concrete statements for transmon-to-fluxonium and transmon-to-trapped-ion ratios. Within the Recognition framework it closes the structural half of track F1, leaving only the rung assignments as open hypotheses.
scope and limits
- Does not derive the Z-rung assignments for specific qubit families from first principles.
- Does not apply when the base decoherence time is non-positive.
- Does not guarantee the ratio formula without the ordering k_a ≤ k_b.
- Does not address higher-order corrections beyond the leading BIT-coupling channel.
Lean usage
have h := T2_ratio_is_phi_power T2_0 z_rung_transmon z_rung_fluxonium hT (by unfold z_rung_transmon z_rung_fluxonium; omega); simpa [z_rung_transmon, z_rung_fluxonium] using hformal 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). -/