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

coherenceAtRung

show as:
view Lean formalization →

The coherence level at decoherence rung k equals phi to the power minus k. Modelers of quantum decoherence in the Recognition Science framework cite this definition when establishing the phi-decay law across independent channels. It is introduced as a direct power expression that inverts the sign of the upstream superconducting-qubit version.

claimThe coherence remaining after k independent decoherence channels is given by $C(k) = phi^{-k}$, where $phi$ denotes the self-similar fixed point of the Recognition Composition Law.

background

In the Recognition Science treatment of quantum decoherence, coherence is lost through interaction with an environment according to a phi-decay law. Each decoherence channel reduces the coherence ratio by the factor 1/phi per characteristic time scaled by phi to the rung Z. The module identifies five canonical mechanisms (phonon scattering, photon emission, spin-environment coupling, charge noise, flux noise) whose count equals the configuration dimension D = 5.

proof idea

This is a direct definition that sets the coherence value at rung k to phi raised to the integer power minus k. It mirrors the upstream definition from the superconducting qubit module but flips the exponent sign to encode decay.

why it matters in Recognition Science

This definition supplies the decay factor used in the coherenceDecay theorem, which proves that the ratio between consecutive rungs equals phi inverse. It also populates the phi_decay field in the DecoherenceCert structure. The construction realizes the phi-decay law stated in the module documentation and connects to the self-similar fixed point phi of the Recognition Composition Law.

scope and limits

formal statement (Lean)

  32noncomputable def coherenceAtRung (k : ℕ) : ℝ := phi ^ (-(k : ℤ))

proof body

Definition body.

  33

used by (5)

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

depends on (1)

Lean names referenced from this declaration's body.