distance_2_zero_at_tick_1
plain-language theorem explainer
The theorem shows that activation at hop distance 2 vanishes after only one tick in a directed chain. Modelers of causal signal propagation in recognition networks cite it to verify that multi-hop signals require at least as many ticks as the hop count. The proof reduces immediately to the case distinction in the definition of chain activation.
Claim. For any real blend rate $η$, the activation of a node at hop distance 2 after exactly one tick is zero.
background
The module examines whether sparse matrix-vector multiplication preserves causal ordering on directed graphs. Its central definition states that chain activation at distance $d$ after $t$ ticks equals zero when $t < d$ and otherwise equals $η^d (1-η)^{t-d}$. The upstream tick constant supplies the discrete time unit $τ_0 = 1$. This theorem supplies the base case confirming that distance-2 nodes remain inactive at the first tick.
proof idea
One-line wrapper that applies the definition of chain activation, which returns zero whenever the tick count is strictly less than the hop distance.
why it matters
The result anchors the claim that activation times strictly increase with hop distance on directed chains, feeding the parent statement hop_ordering_preserved. It directly addresses the module's diagnostic question on whether propagation preserves causality and aligns with the eight-tick octave being long enough for chains up to roughly five hops.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.