peak_decreases
plain-language theorem explainer
Geometric decay of peak activation follows directly from the definition η^d for blend rates η in (0,1). Propagation analysts cite the result to confirm strict ordering of activation times by hop distance on directed chains. The term proof reduces the inequality via power successor and the multiplicative comparison lemma.
Claim. For all real η with 0 < η < 1 and all natural numbers d, η^{d+1} < η^d.
background
The Causal Propagation Ordering module investigates whether SpMV operations maintain causal ordering in directed graphs and whether the 8-tick octave supports multi-hop signals. Peak activation at distance d is the quantity η^d, the highest signal level reached at that hop, realized at the arrival tick. This definition appears in the same module and connects to the blend rate η = 1/φ² drawn from the self-similar fixed point in the Recognition framework.
proof idea
Unfolding peak_activation yields η^{d+1}. The successor power rule rewrites this as η · η^d. The exact application of mul_lt_of_lt_one_left then uses positivity of the d-th power together with η < 1 to conclude the strict inequality.
why it matters
The declaration supplies the second conjunct of diagnostic_q1_q2, which affirms that activation ordering holds on chains and that 8 ticks cover up to roughly 4 hops since η^4 exceeds the detection threshold while η^5 falls below it. This step closes the reach-bound calculation log(ε)/log(η) and ties directly to the 8-tick octave landmark (T7) and the Recognition Composition Law constraints on blend rates. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.