typicalSCQubit
plain-language theorem explainer
typicalSCQubit supplies a concrete record of parameters for a typical superconducting qubit in Recognition Science decoherence modeling. It sets T1 relaxation at 50 μs, T2 dephasing at 70 μs, temperature at 15 mK, and 10 environmental modes. Researchers computing predicted decoherence times from the Gap-45 threshold cite this instance. The definition is a direct record literal that instantiates the QubitParams structure with these values.
Claim. A typical superconducting qubit is specified by relaxation time $t_1 = 50$ μs, dephasing time $t_2 = 70$ μs, operating temperature $T = 0.015$ K, and coupling to 10 environmental modes.
background
QubitParams is the structure holding T1 relaxation time (seconds), T2 dephasing time (seconds), operating temperature (Kelvin), and the natural number of coupled environmental modes. The module derives decoherence timescales from the Gap-45 threshold, the boundary separating quantum coherence (information preserved below the threshold) from classical entanglement with the environment (above the threshold). Gap-45 ≈ 10^45 is the ratio between Planck and biological timescales. Upstream, temperature is the inverse of the Lagrange multiplier β, obtained as the derivative of average energy with respect to entropy in the Boltzmann distribution.
proof idea
This is a direct record definition that populates the four fields of QubitParams with the literal values t1 := 50e-6, t2 := 70e-6, temperature := 0.015, env_modes := 10. No lemmas or tactics are invoked; the construction is a one-line record literal.
why it matters
The definition supplies the concrete instance consumed by predictedQubitDecoherence to evaluate the decoherence time via τ_decoherence ≈ τ_0 × φ^(-N). It anchors the Gap-45 mechanism in the module's core insight, connecting to the phi scaling and eight-tick octave of the Recognition Science forcing chain (T5-T7). It provides a practical calibration point for the quantum-to-classical transition without deriving the numerical values from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.