diagnostic_q1_q2
plain-language theorem explainer
The theorem establishes that on directed chains, activation after d ticks strictly exceeds activation at distance d+1 for any blend rate η in (0,1), and that peak signal strength at 4 hops exceeds the peak at 5 hops. Graph theorists and causal inference modelers would cite it to confirm SpMV ordering preservation when edges are unidirectional. The proof is a direct pairing of the general hop-ordering lemma with the geometric peak-decrease result evaluated at distance 4.
Claim. For every blend rate η satisfying 0 < η < 1 and every natural number d, the chain activation at distance d after exactly d ticks exceeds the chain activation at distance d+1 after d ticks; moreover, the peak activation at distance 4 exceeds the peak activation at distance 5.
background
Chain activation at distance d after t ticks on a directed chain is defined as 0 when t < d and η^d (1-η)^{t-d} otherwise; it models pure geometric decay after the signal first arrives. Peak activation at distance d is simply η^d, the maximum value attained precisely when the signal reaches that node. The module answers two diagnostic questions on SpMV propagation: whether it preserves strict causal ordering on directed chains and whether the 8-tick octave suffices for multi-hop causality up to roughly 4 hops.
proof idea
The proof is a one-line wrapper that supplies the pair consisting of the general_hop_ordering theorem (applied to arbitrary d) and the peak_decreases theorem (applied at d=4). No additional tactics or reductions are required beyond the supplied lemmas.
why it matters
This diagnostic result directly answers the module's two questions, confirming that SpMV preserves ordering on unidirectional chains (Q1) and that 4-hop peaks remain detectable while 5-hop peaks fall below practical thresholds (Q2). It supports the eight-tick octave (T7) and the requirement that CAUSES bonds remain directed. No downstream theorems depend on it yet, but it grounds the engine correspondence to typed_bond_builder.py.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.