gap_range
plain-language theorem explainer
The theorem establishes that the base-10 logarithm of the decoherence timescale gap lies between 43 and 45. Researchers modeling quantum-to-classical transitions via the Gap-45 threshold in Recognition Science would cite this numerical bound when fixing environmental coupling. The proof is a one-line wrapper that unfolds the definition of timescale_gap_log10 and discharges the resulting inequalities with norm_num.
Claim. $43 ≤ log_{10}(τ_gap) ∧ log_{10}(τ_gap) < 45$, where τ_gap denotes the ratio of Planck time to biological coherence time in the Gap-45 mechanism.
background
In the QFT.Decoherence module the Gap-45 threshold separates the quantum regime (coherent superposition preserved) from the classical regime (entanglement with the environment). The decoherence time is expressed as τ_decoherence ≈ τ_0 × φ^{-N}, with N the number of coupled environmental modes and φ the golden-ratio scaling factor. timescale_gap_log10 is the base-10 logarithm of the ratio between Planck-scale and biological-scale times, yielding the order-of-magnitude separation that defines the threshold.
proof idea
The proof is a one-line wrapper. It unfolds the definition of timescale_gap_log10, splits the conjunction with constructor, and verifies the numerical bounds 43 ≤ x < 45 by norm_num.
why it matters
The bound calibrates the Gap-45 mechanism that anchors decoherence calculations in the Recognition Science framework. It supplies the concrete numerical separation required by the decoherence formula and aligns with the phi-ladder scaling and the eight-tick octave structure. No downstream theorems are listed, but the result closes the numerical foundation for QF-009.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.