general_hop_ordering
plain-language theorem explainer
General hop ordering asserts that activation at distance d exceeds activation at distance d+1 when evaluated at tick d, for any positive blend rate η. Researchers verifying causality in recognition-based propagation models would cite this result when establishing that directed chains maintain strict temporal separation. The proof proceeds by direct simplification of the chain activation formula followed by an appeal to positivity of powers.
Claim. For real number $η > 0$ and natural number $d$, let $A(η, k, t)$ denote activation at hop distance $k$ after $t$ ticks, defined as $0$ if $t < k$ and $η^k (1-η)^{t-k}$ otherwise. Then $A(η, d, d) > A(η, d+1, d)$.
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 before tick d and η^d (1-η)^{t-d} thereafter, modeling exponential decay along a pure chain. This sits inside the foundation layer that derives the eight-tick octave from the forcing chain T0-T8. Upstream results include the definition of chain_activation itself together with IntegrationGap.A and related structures that fix the active edge count per tick.
proof idea
The proof is a short tactic sequence. It first simplifies both chain_activation expressions at the two distances. A ring identity reduces the second term to η^d, after which the inequality becomes η^d > 0. This follows immediately from the hypothesis that η is positive and the fact that positive reals raised to natural powers remain positive.
why it matters
This lemma supplies the strict inequality needed for diagnostic_q1_q2, which affirms that SpMV preserves causal ordering on directed chains and that the eight-tick octave suffices for chains up to roughly five hops. It directly addresses the module's question on whether propagation flattens causality. In the broader framework it supports the claim that the phi-ladder and eight-tick structure maintain distinguishable hop distances before shortcuts are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.