decoherenceMechanismCount
plain-language theorem explainer
The declaration fixes the number of decoherence channels at five in the Recognition Science model of quantum coherence loss. Modelers of J-cost driven decay would cite the count to set the configuration dimension when computing coherence ratios. The proof is a one-line decision procedure that evaluates the Fintype cardinality of the enumerated inductive type.
Claim. The finite set of decoherence mechanisms, consisting of phonon scattering, photon emission, spin-environment coupling, charge noise, and flux noise, satisfies $|D| = 5$.
background
The module treats quantum decoherence as reduction of the coherence ratio r by successive factors of 1/phi, with each channel acting over a characteristic time scaled by phi to the rung index. DecoherenceMechanism is the inductive type whose five constructors are phonon, photon, spinEnvironment, chargeNoise, and fluxNoise; the type derives DecidableEq, Repr, BEq, and Fintype instances directly from the constructors. The local setting states that these five channels realize configDim D = 5 and that adjacent mechanisms differ in decay time by exactly one power of phi.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card DecoherenceMechanism = 5. The tactic succeeds because the inductive definition supplies a computable Fintype instance whose cardinality is the number of listed constructors.
why it matters
The result supplies the five_mechanisms field of the downstream decoherenceCert definition, which pairs the count with the coherenceDecay law. It realizes the module claim that five mechanisms account for decoherence in RS-native units, consistent with the five-element configuration dimension stated in the module documentation. No open scaffolding questions are attached to this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.