decoherenceFromBITCert
plain-language theorem explainer
The master certificate for decoherence under the bosonic identity theorem carrier is inhabited by populating its five fields from sibling results. Quantum information researchers modeling qubit T2 times under BIT coupling would cite this when deriving phi-power ratios between substrate classes. The definition is a direct structure construction that wires the frequency band, positivity, monotonicity, and exact phi-power ratio lemmas into the certificate record.
Claim. The decoherence certificate asserts that the BIT carrier frequency satisfies $7.5 < ω_{BIT} < 8.1$, that the substrate decoherence time $T_2(k)$ is positive for positive $T_{2,0}$ and strictly decreasing in the rung index $k$, that cross-class ratios obey $T_2(k_a)/T_2(k_b) = φ^{k_b - k_a}$ for $k_a ≤ k_b$, and that the transmon-to-fluxonium ratio equals exactly $φ$.
background
The module establishes the algebraic structure of decoherence induced by coupling a qubit substrate to the bosonic identity theorem carrier at frequency $ω_{BIT} = 5φ$ in RS-native units. The central object is the structure DecoherenceFromBITCert whose five fields encode the band constraint on the carrier, positivity and strict decrease of $T_2(k)$, the exact phi-power ratio between any two rung indices, and the specific transmon-fluxonium ratio of $φ$. Upstream results supply the carrier frequency definition (5·φ) and the canonical arithmetic and cost-band operations used to construct the underlying rung ladder.
proof idea
The definition is a direct structure construction that assigns the five fields of DecoherenceFromBITCert to the sibling lemmas omega_BIT_band, T2_substrate_pos, T2_substrate_strictly_decreasing, T2_ratio_is_phi_power, and T2_transmon_to_fluxonium_ratio. No tactics or reductions are required beyond field projection.
why it matters
This definition inhabits the master certificate that closes the algebraic core of the Decoherence from BIT track. It supplies the structural theorem that any two substrate classes differ in T2 by an integer power of φ once their Z-rung difference is fixed, directly supporting the one-statement summary in the module. The result sits downstream of the carrier frequency definitions and upstream of any empirical calibration of specific qubit families to rungs; it touches the open question of whether measured cross-class T2 ratios remain inside the predicted phi-powers on larger data sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.