hop_ordering_preserved
plain-language theorem explainer
hop_ordering_preserved establishes that for blend rate η in (0,1), activation after one tick at distance 1 strictly exceeds activation at distance 2 on a directed chain. Researchers modeling causal signal flow in Recognition Science cite it to confirm that SpMV respects sequential hop ordering without flattening. The tactic proof unfolds the chain_activation definition, reduces the resulting powers via ring, and closes the inequality with linarith.
Claim. For $0 < η < 1$, let $a(d,t)$ be the activation at hop distance $d$ after $t$ ticks on a directed chain, given by $a(d,t) = η^d (1-η)^{t-d}$ if $t ≥ d$ and $0$ otherwise. Then $a(1,1) > a(2,1)$.
background
The module examines whether sparse matrix-vector multiplication preserves causal ordering on graphs. It introduces chain_activation as the activation at hop distance $d$ from a unit source after $t$ ticks of pure blend on a directed chain topology: the signal arrives exactly at tick $d$ and then decays by the factor η per additional hop. The fundamental time unit is the tick, defined as the RS-native time quantum τ₀ = 1. The local setting answers two diagnostic questions: whether SpMV flattens causality and whether the 8-tick octave suffices for multi-hop propagation.
proof idea
The tactic script begins with simp on chain_activation to expose the conditional definition. Two ring lemmas establish the concrete powers η² and η after substitution of t=1. A further ring step rewrites the left-hand side, after which linarith closes the strict inequality using the positivity and upper-bound hypotheses on η.
why it matters
Listed among the module's key results, the theorem confirms that SpMV preserves causal ordering on directed chains and thereby answers diagnostic question 1. It supports the claim that the 8-tick octave is long enough for chains up to roughly five hops, linking to the eight-tick octave (T7) and the absence of shortcuts in the underlying causal structure. No downstream uses are recorded yet; the result stands as a foundational ordering lemma for later reach-bound arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.