DecoherenceCert
plain-language theorem explainer
DecoherenceCert packages the two assertions that exactly five decoherence channels exist and that coherence ratios between consecutive rungs equal phi inverse. Modelers of qubit lifetimes or T_dec scaling in the Recognition Science framework cite this certificate when matching the phi-ladder to experimental decoherence data. The declaration is a bare structure definition that records the two field predicates with no further reduction or computation.
Claim. A certificate consisting of the statements that the set of decoherence channels (phonon scattering, photon emission, spin-environment coupling, charge noise, flux noise) has cardinality 5 and that the coherence function satisfies $C(k+1)/C(k)=phi^{-1}$ for every natural number $k$, where $C(k)=phi^{-k}$.
background
The module derives quantum decoherence from the J-cost functional equation via the Recognition Composition Law. DecoherenceMechanism enumerates the five canonical channels (phonon, photon, spinEnvironment, chargeNoise, fluxNoise) and carries a Fintype instance. coherenceAtRung(k) is defined as phi to the power of minus k, giving the ratio of quantum recognition capacity to the classical limit at rung k on the phi-ladder.
proof idea
Structure definition that directly encodes the two field assertions. The first field uses the Fintype.card instance on DecoherenceMechanism; the second field states the uniform ratio property of the coherenceAtRung definition.
why it matters
Supplies the type for the downstream decoherenceCert instance that is built from decoherenceMechanismCount and coherenceDecay. It formalizes the RS claim that five mechanisms equal configDim D=5 and that adjacent mechanisms differ in T_dec by the factor phi, completing the B-tier quantum physics section of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.