chain_activation
plain-language theorem explainer
The chain_activation function specifies the activation level reached at distance d after exactly t ticks of blend propagation with rate η on a directed chain. It is cited in verifications that SpMV respects causal order on acyclic graphs and that the eight-tick octave supports chains of length up to five. The definition implements a thresholded geometric decay that is zero before arrival and η^d times (1-η) to the remaining power afterward.
Claim. For blend rate $η$, hop distance $d$, and tick count $t$, the activation is $0$ if $t < d$, and $η^d (1-η)^{t-d}$ otherwise. This assumes unit source activation on a directed chain topology.
background
The module examines whether sparse matrix-vector multiplication preserves causal ordering in propagation. The upstream before predicate from TimeEmergence states that snapshot A precedes B precisely when the tick index of A is smaller than that of B. Blend rate η is the transmission probability per hop, conventionally 1/φ² ≈ 0.382 in the engine.
proof idea
The definition is a direct conditional: zero when t is below d, otherwise the product of η raised to d and (1-η) raised to (t-d). It serves as the base case without invoking additional lemmas.
why it matters
It supplies the explicit formula used by hop_ordering_preserved and diagnostic_q1_q2 to confirm that activation times increase strictly with distance on directed chains. This supports the module's conclusion that the eight-tick octave (T7) is sufficient for causal chains up to roughly five hops, and that shortcuts would violate ordering. It addresses diagnostic questions 1 and 2 on causality preservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.