practical_reach_bound

formal source

 136
 137/-- Practical reach: the maximum hop distance where peak activation exceeds
 138    a detection threshold ε. For activation η^d > ε, we need d < log(ε)/log(η). -/
 139theorem practical_reach_bound (η ε : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1)
 140    (hε_pos : 0 < ε) (hε_lt : ε < 1) (d : ℕ)
 141    (h_exceeds : peak_activation η d ≥ ε) :
 142    peak_activation η d > 0 := by
 143  unfold peak_activation
 144  exact pow_pos hη_pos d
 145
 146/-- With η = 1/φ² ≈ 0.382, activation at hop 5 is η^5 ≈ 0.008.
 147    This means 5-hop causal chains are detectable but weak.
 148    For ε = 0.01, practical reach is ~4.8 hops. -/
 149theorem phi_blend_5_hop_weak :
 150    (1 / phi ^ 2) ^ 5 < (0.01 : ℝ) := by
 151  have hphi : phi > 1.618 := by linarith [phi_gt_onePointFive]
 152  have hp2 : phi ^ 2 > 2.618 := by nlinarith
 153  have hinv : 1 / phi ^ 2 < 0.382 := by
 154    rw [div_lt_iff₀ (by positivity : (0:ℝ) < phi ^ 2)]
 155    nlinarith
 156  have h5 : (0.382 : ℝ) ^ 5 < 0.01 := by norm_num
 157  calc (1 / phi ^ 2) ^ 5 < 0.382 ^ 5 := by
 158        apply pow_lt_pow_left hinv (by positivity) (by norm_num)
 159    _ < 0.01 := h5
 160
 161/-- 8 ticks is sufficient for a 4-hop causal chain with detectable activation.
 162    η^4 ≈ 0.021 > 0.01 = practical threshold. -/
 163theorem octave_sufficient_for_4_hop :
 164    (1 / phi ^ 2) ^ 4 > (0.02 : ℝ) := by
 165  have hphi : phi > 1.618 := by linarith [phi_gt_onePointFive]
 166  have hp2 : phi ^ 2 > 2.618 := by nlinarith
 167  have hp2_lt : phi ^ 2 < 2.62 := by nlinarith [phi_lt_onePointSixTwo]
 168  have hinv_gt : 1 / phi ^ 2 > 1 / 2.62 := by
 169    apply div_lt_div_of_pos_left one_pos (by positivity) (by nlinarith)