ShortcutGraph

formal source

  97/-- A graph where A connects to both B (distance 1) and C (distance 1 via shortcut).
  98    In the directed chain A→B→C, C is at distance 2. But with a shortcut A→C,
  99    C is also at distance 1. -/
 100structure ShortcutGraph where
 101  weight_AB : ℝ
 102  weight_AC : ℝ
 103  weight_AB_pos : 0 < weight_AB
 104  weight_AC_pos : 0 < weight_AC
 105
 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. -/