coherenceRatio
plain-language theorem explainer
Coherence times on the phi-ladder increase by exactly the factor phi at each successive rung. Quantum information researchers modeling superconducting qubit lifetimes under RS_PAT_043 predictions cite this scaling when deriving T2(k+1) = T2(k) * phi. The term proof unfolds the local power definition of coherenceAtRung, invokes positivity of phi^k, rewrites the successor and division, then simplifies algebraically with ring.
Claim. For each natural number $k$, the ratio of coherence at rung $k+1$ to coherence at rung $k$ equals the golden ratio $phi$, where coherence at rung $k$ is defined as $phi^k$.
background
In the SuperconductingQubitFromJCost module the function coherenceAtRung is defined by phi raised to the power k. This implements the RS_PAT_043 prediction that transmon T1 and T2 times follow phi^k scaling with optimal anharmonicity at ladder positions. The module also imports the related definition from QuantumDecoherenceFromJCost, where coherenceAtRung(k) equals phi to the power of minus k, providing the general decoherence baseline.
proof idea
The term proof unfolds coherenceAtRung to expose the powers of phi. It applies pow_pos to obtain positivity of phi^k, rewrites via pow_succ and div_eq_iff to eliminate the division, and finishes with the ring tactic for algebraic cancellation.
why it matters
This result supplies the phi_ratio field inside the scQubitCert structure that certifies the five canonical qubit types. It directly encodes the module claim that T2(k+1) equals T2(k) times phi. In the Recognition framework it instantiates the self-similar fixed point phi from the forcing chain (T6) and supports the eight-tick octave structure through the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.