pith. machine review for the scientific record. sign in
theorem proved term proof

T2_transmon_to_fluxonium_ratio

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 137theorem T2_transmon_to_fluxonium_ratio (T2_0 : ℝ) (hT : 0 < T2_0) :
 138    T2_substrate T2_0 z_rung_transmon / T2_substrate T2_0 z_rung_fluxonium
 139      = Constants.phi ^ 1 := by

proof body

Term-mode proof.

 140  have h := T2_ratio_is_phi_power T2_0 z_rung_transmon z_rung_fluxonium hT (by
 141    unfold z_rung_transmon z_rung_fluxonium; omega)
 142  simpa [z_rung_transmon, z_rung_fluxonium] using h
 143
 144/-- The transmon-trapped-ion ratio is exactly `φ³`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.