peak_activation

formal source

 125/-- Signal strength at hop distance d: η^d.
 126    This is the peak activation a node at distance d ever achieves
 127    (occurring at the tick when signal first arrives). -/
 128def peak_activation (η : ℝ) (d : ℕ) : ℝ := η ^ d
 129
 130/-- Peak activation decreases geometrically with distance. -/
 131theorem peak_decreases (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1) (d : ℕ) :
 132    peak_activation η (d + 1) < peak_activation η d := by
 133  unfold peak_activation
 134  rw [pow_succ]
 135  exact mul_lt_of_lt_one_left (pow_pos hη_pos d) hη_lt
 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)