pith. machine review for the scientific record. sign in
structure definition def or abbrev high

DecoherenceCert

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  44structure DecoherenceCert where
  45  five_mechanisms : Fintype.card DecoherenceMechanism = 5
  46  phi_decay : ∀ k, coherenceAtRung (k + 1) / coherenceAtRung k = phi⁻¹
  47

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.