gap45_crossover_range
plain-language theorem explainer
The declaration bounds the approximate mode count at the Gap-45 crossover strictly between 100 and 300. Physicists estimating decoherence timescales in quantum systems cite this interval to locate the transition from coherent superposition to environmental entanglement. The proof reduces the claim to numerical verification by unfolding the constant 210 and applying normalization tactics.
Claim. $100 < N < 300$, where $N$ is the rational approximation to the number of environmental modes at the Gap-45 threshold.
background
In the QFT.Decoherence module the Gap-45 threshold marks the boundary between quantum coherence and classical decoherence, defined as the ratio of roughly $10^{45}$ between Planck-scale and biological timescales. The upstream definition gap45CrossoverApprox computes the corresponding mode count via the logarithmic ratio $N = ln(τ_bio / τ_0) / ln(φ) ≈ 210$, with τ_0 the fundamental tick and φ the golden ratio. The module derives decoherence times from the scaling τ_decoherence ≈ τ_0 × φ^{-N}.
proof idea
The term proof unfolds the definition of gap45CrossoverApprox to substitute the constant 210, then applies constructor to split the conjunction followed by norm_num to confirm both sides of the numerical inequality.
why it matters
This bound anchors the Gap-45 mechanism in the Recognition Science framework, supporting decoherence timescale derivations that connect to the phi-ladder scaling and eight-tick octave for temporal hierarchies. It supplies a concrete numerical check for the crossover described in QF-009, enabling estimates for quantum error correction based on environmental mode coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.