def
definition
def or abbrev
chain_activation
show as:
view Lean formalization →
formal statement (Lean)
54def chain_activation (η : ℝ) (d : ℕ) (t : ℕ) : ℝ :=
proof body
Definition body.
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. -/