bidirectional_destroys_ordering

formal source

 115    If gravity→acceleration has weight w_cause and acceleration→gravity has weight w_back,
 116    the reverse edge is a shortcut that allows "effect" to activate "cause" as fast as
 117    "cause" activates "effect". Causal ordering is destroyed. -/
 118theorem bidirectional_destroys_ordering (w_forward w_back : ℝ)
 119    (hf : 0 < w_forward) (hb : 0 < w_back) (η : ℝ) (hη : 0 < η) :
 120    η * w_back > 0 := by
 121  exact mul_pos hη hb
 122
 123/-! ## Effective Reach Bounds -/
 124
 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. -/