blend_step

formal source

  45
  46/-- Activation of a node at tick t, given blend rate η and incoming signal.
  47    This models one step of `blended = (1-η)*my_psi + η*prop`. -/
  48def blend_step (current : ℝ) (incoming : ℝ) (η : ℝ) : ℝ :=
  49  (1 - η) * current + η * incoming
  50
  51/-- Activation at hop distance d from source after t ticks of pure blend,
  52    assuming the source has unit activation and directed chain topology.
  53    At distance d, signal arrives at tick d and decays as η^d per hop. -/
  54def chain_activation (η : ℝ) (d : ℕ) (t : ℕ) : ℝ :=
  55  if t < d then 0 else η ^ d * (1 - η) ^ (t - d)
  56
  57/-! ## Directed Chains: Ordering Preserved -/
  58
  59/-- On a directed chain, node at distance 1 activates before node at distance 2.
  60    The signal must traverse each hop sequentially; no shortcuts exist. -/
  61theorem hop_ordering_preserved (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1) :
  62    chain_activation η 1 1 > chain_activation η 2 1 := by
  63  simp [chain_activation]
  64  have h1 : η ^ 2 * (1 - η) ^ 0 = η ^ 2 := by ring
  65  have h2 : η ^ 1 * (1 - η) ^ 0 = η := by ring
  66  rw [h2]
  67  have : η ^ 2 = η * η := by ring
  68  linarith [mul_lt_of_lt_one_right hη_pos hη_lt]
  69
  70/-- At tick 1, only distance-1 nodes have nonzero activation.
  71    Distance-2 nodes have zero activation because signal hasn't reached them. -/
  72theorem distance_2_zero_at_tick_1 (η : ℝ) :
  73    chain_activation η 2 1 = 0 := by
  74  simp [chain_activation]
  75
  76/-- At tick 2, distance-2 nodes activate but with η² attenuation.
  77    Distance-1 nodes have η(1-η) activation (received at tick 1, decayed one tick). -/
  78theorem activation_at_tick_2 (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1) :