density_exceeds_threshold
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute an explicit numerical N.
- Does not apply when any input constant is non-positive.
- Does not treat volume growth of degree other than three.
- Does not incorporate physical units or constants beyond the pure inequality.
formal statement (Lean)
133theorem density_exceeds_threshold (K₀ : ℝ) (hK₀ : 0 < K₀)
134 (V₀ : ℝ) (hV₀ : 0 < V₀) (threshold : ℝ) (hT : 0 < threshold) :
135 ∃ N : ℕ, K₀ * phi ^ N / (V₀ * ((N : ℝ) + 1) ^ 3) > threshold := by
proof body
Tactic-mode proof.
136 -- Need phi^N > (threshold * V₀ / K₀) * (N+1)^3
137 have hC : 0 < threshold * V₀ / K₀ := by positivity
138 obtain ⟨N, hN⟩ := phi_exp_defeats_cubic_succ (threshold * V₀ / K₀) hC
139 refine ⟨N, ?_⟩
140 have hdenom_pos : 0 < V₀ * ((N : ℝ) + 1) ^ 3 := by positivity
141 rw [gt_iff_lt, lt_div_iff₀ hdenom_pos]
142 -- Goal: threshold * (V₀ * (N+1)^3) < K₀ * phi^N
143 -- From hN: phi^N > (threshold*V₀/K₀) * (N+1)^3
144 -- So K₀ * phi^N > K₀ * (threshold*V₀/K₀) * (N+1)^3 = threshold*V₀*(N+1)^3
145 have hphi_pos : 0 < phi ^ N := pow_pos phi_pos N
146 have hNN3 : 0 < ((N : ℝ) + 1) ^ 3 := by positivity
147 have hK0phi : K₀ * phi ^ N > K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 := by
148 have := mul_lt_mul_of_pos_left hN hK₀
149 simp only [mul_comm, mul_assoc] at this ⊢
150 linarith
151 have hsimp : K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 =
152 threshold * V₀ * ((N : ℝ) + 1) ^ 3 := by
153 have hK0ne : K₀ ≠ 0 := ne_of_gt hK₀
154 field_simp [hK0ne]
155 rw [hsimp] at hK0phi
156 linarith
157
158end GrowthBounds
159end Foundation
160end IndisputableMonolith