DecoherenceFromBITCert
plain-language theorem explainer
The structure DecoherenceFromBITCert bundles five properties for the BIT-coupled decoherence model: the carrier frequency lies in (7.5, 8.1), T2 times remain positive and strictly decrease with rung index k, and T2 ratios between any two classes equal phi to the integer rung difference. Quantum information researchers modeling substrate-dependent decoherence would cite it when calibrating phi-power scaling from a single T2_0 measurement. It is introduced as a structure definition that directly encodes the algebraic consequences of the closed T2
Claim. Let $T_2(k) := T_{2,0}/phi^k$ for rung index $k$. The certificate asserts $7.5 < omega_{BIT} < 8.1$, positivity $T_2(k) > 0$ whenever $T_{2,0} > 0$, strict decrease $T_2(k+1) < T_2(k)$, the ratio identity $T_2(k_a)/T_2(k_b) = phi^{k_b - k_a}$ for $k_a leq k_b$, and the transmon-to-fluxonium ratio equaling $phi$.
background
In the Decoherence from BIT module the Bosonic Identity Theorem supplies the carrier frequency omega_BIT = 5 phi in RS-native units. The substrate decoherence time is defined by T2_substrate T2_0 k = T2_0 / phi^k, where higher Z-rung produces stronger BIT coupling and faster decoherence. This structure packages the resulting positivity, monotonicity, and phi-power ratio properties that follow immediately from the definition.
proof idea
As a structure definition with empty proof body, DecoherenceFromBITCert simply assembles the five listed properties. The ratio and monotonicity claims follow directly from the closed-form expression of T2_substrate once positivity of phi is granted by the Constants structure.
why it matters
This certificate serves as the master record for Track F1, feeding the inhabited instance decoherenceFromBITCert. It encodes the phi-power scaling forced by BIT coupling, consistent with the self-similar fixed point phi. The module notes that specific rung assignments remain hypotheses, with a falsifier given by cross-pair T2 ratios deviating more than 5% from any integer power of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.