CoherenceTimeCert
plain-language theorem explainer
CoherenceTimeCert packages the constant ratio phi between coherence times at consecutive phi-ladder rungs together with algebraic and inequality witnesses for phi^8 and phi^12. Quantum biologists modeling decoherence in cryptochrome or similar systems would reference this certificate to justify rung-12 timescales. The declaration is a structure definition that simply records these four properties without further computation.
Claim. The structure asserts that coherence time satisfies $τ(k+1)/τ(k)=φ$ for all natural $k$, where $τ(k):=φ^k$, together with the relations $φ^8=21φ+13$, $φ^8>46$, and $φ^{12}>300$.
background
The module models biological quantum coherence times as scaling geometrically with the golden ratio phi on the phi-ladder. coherenceTimeAtRung k is defined as phi^k, consistent with the J-cost functional and the self-similar fixed point. The base time is set near 7.3 femtoseconds, placing avian systems near rung 12 where times reach microseconds.
proof idea
As a structure definition, CoherenceTimeCert collects the four fields without executing any proof steps or applying lemmas. The properties are verified separately in sibling declarations such as coherenceTimeRatio and phi8_fibonacci, then assembled in the downstream coherenceTimeCert.
why it matters
CoherenceTimeCert provides the bundled certificate consumed by coherenceTimeCert to certify the scaling law for quantum coherence times. It fills the module's claim that tau(k) = tau_0 * phi^k, linking to the T6 phi fixed point and T7 octave in the unified forcing chain. This supports predictions in the femtosecond to microsecond range without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.