density_exceeds_threshold
plain-language theorem explainer
The theorem proves that for any positive K₀, V₀ and threshold the ratio K₀ φ^N over V₀(N+1)^3 eventually exceeds the threshold. Analysts closing the Fermi chain in Recognition Science growth bounds cite it to confirm phi-ladder scaling overtakes cubic volume. The proof rescales the constant in the upstream phi-exp-defeats-cubic-succ lemma and rearranges the target inequality via positivity and linear arithmetic.
Claim. For all real numbers $K_0>0$, $V_0>0$ and threshold$>0$, there exists a natural number $N$ such that $K_0$ φ$^N$ / ($V_0$ $(N+1)^3$) exceeds threshold.
background
The module supplies pure real-analysis facts that exponential growth dominates any polynomial, with specific instances for the φ-ladder versus cubic volume growth that close the Fermi chain. The upstream result states: for any C>0 there exists N such that φ^N > C·(N+1)^3. The present theorem adapts that bound by setting C equal to threshold·V₀/K₀ so the target density expression exceeds the given threshold.
proof idea
The proof computes C = threshold·V₀/K₀ and obtains N from phi_exp_defeats_cubic_succ. It then rewrites the target inequality using lt_div_iff₀, positivity of the denominator, mul_lt_mul_of_pos_left, field_simp to cancel K₀, and linarith to finish.
why it matters
This supplies the final density-exceeds-threshold step that closes the Fermi chain in the Recognition framework. It directly instantiates the exponential-versus-cubic comparison required by the phi-ladder mass formula and the T6 self-similar fixed point. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.