coherenceDecay
plain-language theorem explainer
The ratio of coherence values at consecutive rungs on the phi-ladder equals the inverse golden ratio. Quantum physicists working with J-cost models of decoherence would cite this to obtain the exponential decay factor per channel. The proof is a direct algebraic reduction that unfolds the power definition and simplifies the resulting zpow expressions using field arithmetic.
Claim. For every natural number $k$, the ratio of coherence at rung $k+1$ to coherence at rung $k$ equals $phi^{-1}$, where coherence at rung $m$ is defined to be $phi^{-m}$.
background
The module models quantum decoherence as loss of recognition capacity through environmental channels. Coherence at rung $k$ is the real number $phi^{-k}$, so the ratio between adjacent rungs is forced to be the constant decay factor $phi^{-1}$. This encodes the statement that each independent decoherence channel multiplies coherence by $1/phi$ per characteristic time interval. The non-vanishing of $phi$ is supplied by the upstream lemma phi_ne_zero from Constants and from PhiLadderLattice, which guarantees that the division in the ratio is well-defined.
proof idea
Unfold the definition of coherenceAtRung on both sides to obtain the explicit powers $phi^{-(k+1)}$ and $phi^{-k}$. Invoke phi_ne_zero together with zpow_pos to obtain a positivity witness. Rewrite the integer exponents via push_cast and ring to isolate the additive shift, apply zpow_add₀, then finish with field_simp.
why it matters
The theorem supplies the phi_decay component inside the downstream decoherenceCert definition, which packages the five-mechanism count together with the decay law. It thereby realizes the RS prediction that adjacent decoherence mechanisms differ in their characteristic times by the factor phi. In the larger framework this step closes the link between the J-cost functional equation and the observed exponential loss of coherence, consistent with the self-similar fixed-point structure that forces the golden ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.