activation_at_tick_2
plain-language theorem explainer
The theorem computes explicit activation levels at tick 2 for distance-1 and distance-2 nodes in a directed chain under blend rate η between 0 and 1. Modelers of causal signal flow in Recognition Science graphs cite it when verifying that SpMV respects hop ordering before shortcuts appear. The proof splits the conjunction and reduces each side by direct substitution into the chain_activation definition followed by algebraic simplification.
Claim. For blend rate $0 < η < 1$, the activation of a distance-1 node after two ticks equals $η(1-η)$ while the activation of a distance-2 node equals $η^2$.
background
The module examines whether sparse matrix-vector multiplication preserves causal ordering on directed graphs. The central definition is chain_activation(η, d, t) which returns zero when t < d and otherwise η^d (1-η)^{t-d}; this encodes a signal that arrives exactly at tick d and then decays by factor (1-η) each subsequent tick. The upstream tick constant supplies the discrete time unit τ₀ = 1. The surrounding results establish that on a pure directed chain the activation time of a node at distance d is strictly less than that at distance d+1, while the presence of a shortcut edge can equalize those times.
proof idea
The term-mode proof opens the conjunction with constructor. Each conjunct is discharged by rewriting with the definition of chain_activation and invoking ring to confirm the resulting polynomial identity.
why it matters
The result supplies the concrete values needed to prove hop_ordering_preserved and to confirm that the eight-tick octave (T7) suffices for chains up to roughly five hops. It directly supports the module claim that SpMV on directed chains respects the arrow of time before bidirectional edges flatten causality. No downstream theorems yet invoke it, leaving open whether the same ordering survives in the full Recognition Composition Law setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.