DecoherenceMechanism
plain-language theorem explainer
The inductive definition enumerates the five canonical decoherence channels in the Recognition Science model of quantum coherence loss. Physicists modeling decoherence times via the phi-ladder would cite this enumeration to fix the dimension of the mechanism space at 5. The definition proceeds by explicit constructors with automatic derivation of decidability and finiteness.
Claim. The set of decoherence mechanisms consists of phonon scattering, photon emission, spin-environment coupling, charge noise, and flux noise.
background
In the Recognition Science framework, quantum decoherence is the loss of coherence through environmental interaction, with the coherence ratio r following the phi-decay law: each channel reduces coherence by 1/phi per characteristic time T_dec = tau_0 * phi^Z, where Z is the decoherence rung. The module sets configDim D = 5 for the five mechanisms and states that adjacent mechanisms differ in T_dec by phi. The local theoretical setting is B-tier quantum physics with zero axioms or sorries.
proof idea
This is a direct inductive definition listing the five constructors, followed by a deriving clause that installs DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This definition supplies the finite set required by the downstream DecoherenceCert structure, which asserts Fintype.card = 5 together with the phi-decay relation between coherenceAtRung values. It realizes the configDim D = 5 for decoherence channels and closes the enumeration needed to certify the phi-decay law in the RS model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.