shortcut_simultaneous_activation

formal source

 106/-- With a shortcut A→C, C receives signal at tick 1 (via shortcut) with weight w_AC,
 107    simultaneously with B receiving signal at tick 1 with weight w_AB.
 108    If w_AC ≥ w_AB, C activates at least as strongly as B at tick 1. -/
 109theorem shortcut_simultaneous_activation (g : ShortcutGraph) (η : ℝ)
 110    (hη_pos : 0 < η) (h_weights : g.weight_AC ≥ g.weight_AB) :
 111    η * g.weight_AC ≥ η * g.weight_AB := by
 112  exact mul_le_mul_of_nonneg_left h_weights (le_of_lt hη_pos)
 113
 114/-- Bidirectional edges (like SBERT kNN) create shortcuts for every typed bond.
 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)