z_rung_transmon
The definition assigns the transmon qubit class to Z-rung 5 on the Recognition Science phi-ladder. Researchers deriving T2 decoherence ratios under the Bosonic Identity Theorem cite this value to fix the exponent in phi-power relations between qubit families. The declaration is a direct constant assignment with no computation or lemmas.
claimThe Z-rung for the transmon qubit class is $5$.
background
The DecoherenceFromBIT module examines coupling between the BIT carrier at frequency $5φ$ and qubit substrates. Each substrate class receives a Z-rung hypothesis that locates it on the phi-ladder; the rung difference then sets the integer exponent $k$ in the T2 ratio $T_2(a)/T_2(b) = φ^k$. Upstream rung definitions in Anchor, RSBridge, and AnchorPolicy supply the integer map from class names to ladder positions, while the calibration definition converts external measurements into RS-native units.
proof idea
Direct definition that sets the value to the natural number 5. No lemmas or tactics are invoked; the declaration simply records the calibration target for transmon qubits.
why it matters in Recognition Science
This assignment supplies the integer input to DecoherenceFromBITCert and the ratio theorems T2_transmon_to_fluxonium_ratio and T2_transmon_to_trapped_ion_ratio. It fixes the rung difference that forces the transmon-fluxonium T2 ratio to equal $φ$ under the BIT model. The placement follows the phi-ladder mass formula extended to decoherence channels, where Z-rung gaps control the exponent in the ratio law.
scope and limits
- Does not derive the rung value from the Recognition Science axioms or forcing chain.
- Does not apply to qubit classes outside the transmon, fluxonium, NV, and trapped-ion families.
- Does not guarantee invariance of the assignment under new experimental calibration data.
Lean usage
theorem use_z_rung_transmon (T2_0 : ℝ) (hT : 0 < T2_0) : T2_substrate T2_0 z_rung_transmon / T2_substrate T2_0 z_rung_fluxonium = Constants.phi ^ 1 := T2_transmon_to_fluxonium_ratio T2_0 hTformal statement (Lean)
125def z_rung_transmon : ℕ := 5
proof body
Definition body.
126
127/-- Fluxonium qubit class — assigned Z-rung 6 (calibration target). -/