phi12_gt_300
plain-language theorem explainer
φ¹² exceeds 300, supplying the lower bound needed to place biological coherence times at rung 12 of the Recognition Science φ-ladder into the microsecond regime. Modelers of avian cryptochrome decoherence cite the result to confirm the scaling from the femtosecond base time τ₀. The tactic proof substitutes the Fibonacci form for φ⁸, derives φ⁴ from the quadratic identity, multiplies the powers, and closes the inequality with nlinarith on the φ > 1.61 bound.
Claim. $φ^{12} > 300$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module develops coherence times from the J-cost functional under the BIT hypothesis. Coherence time at rung k is τ₀ × φ^k with τ₀ ≈ 7.3 fs; rung 12 corresponds to avian cryptochrome and requires φ^12 > 300 to reach the microsecond scale. Upstream lemmas supply the necessary algebraic identities: phi_sq_eq states φ² = φ + 1, phi8_fibonacci states φ^8 = 21φ + 13, and phi_gt_onePointSixOne states φ > 1.61.
proof idea
The proof obtains φ^8 = 21φ + 13 from phi8_fibonacci. It derives φ^4 = 3φ + 2 from phi_sq_eq by two applications of nlinarith. It records the multiplicative identity φ^12 = φ^8 · φ^4 via ring. The final nlinarith step combines these equalities with the numerical lower bound φ > 1.61 to conclude the strict inequality.
why it matters
The bound is packaged directly into coherenceTimeCert together with the φ-ratio, φ^8 value, and φ^8 > 46 to certify rung-12 coherence times. It completes the rung-12 step in the module claim that τ_bio lies in the femtosecond-to-microsecond range. Within the framework it anchors the phi-ladder scaling that follows from T6 (self-similar fixed point) and T7 (eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.