coherenceTimeRatio
plain-language theorem explainer
The theorem establishes that coherence times on the phi-ladder scale exactly by the golden ratio at each successive rung. Researchers modeling biological quantum coherence, such as in avian cryptochrome at rung 12, would cite this scaling to extrapolate from femtosecond base times. The proof is a direct algebraic reduction that unfolds the power definition and simplifies the ratio via positivity and ring rewriting.
Claim. For every natural number $k$, the ratio of normalized coherence times satisfies $τ(k+1)/τ(k)=φ$, where $τ(k):=φ^k$ is the coherence time at rung $k$.
background
In this module, coherence times are assigned to rungs of the phi-ladder with the time at rung $k$ defined as $φ^k$ in units where the base time $τ_0$ equals 1. This construction follows from the J-cost minimum at the identity event (state equal to 1), which anchors the ladder. The module documentation ties the setup to the BIT hypothesis and DFT-8 harmonics, with the 8th harmonic near 5φ Hz and biological coherence times reaching the microsecond range at rung 12. Upstream, the definition coherenceTimeAtRung $k$ := $φ^k$ supplies the power-law form, while the identity event in ObserverForcing records the zero-cost base point.
proof idea
The term-mode proof unfolds coherenceTimeAtRung on both sides to obtain $φ^{k+1}/φ^k$. It applies pow_pos to establish positivity of $φ^k$, rewrites with pow_succ and div_eq_iff, then simplifies the resulting expression with the ring tactic.
why it matters
The result supplies the phi_ratio field inside coherenceTimeCert, which also records the phi^8 and phi^12 amplitude bounds via Fibonacci identities. It completes the scaling step in the quantum coherence time derivation from J-cost, consistent with the self-similar fixed point phi forced at T6 of the unified forcing chain. The certification supports the module's claim that coherence times at rung 12 enter the microsecond regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.