practical_reach_bound
plain-language theorem explainer
The declaration shows that if peak activation at hop distance d meets or exceeds a positive detection threshold ε then the activation value itself is strictly positive. Modelers of causal signal propagation in discrete spacetime would reference this to confirm that detectable multi-hop chains remain non-vanishing. The proof reduces directly to the positivity of real exponentiation under the given positivity hypothesis on the blend rate η.
Claim. Let $η,ε∈ℝ$ satisfy $0<η<1$ and $0<ε<1$, and let $d∈ℕ$. If the peak activation at distance $d$ satisfies $η^d≥ε$, then $η^d>0$.
background
In the Causal Propagation Ordering module, peak activation at hop distance d is defined as the geometric decay η^d, representing the maximum signal strength a node at that distance achieves upon first arrival. This sits inside the broader analysis of whether sparse matrix-vector multiplication preserves causal ordering on directed chains versus shortcut graphs. The module addresses whether the 8-tick octave suffices for multi-hop propagation, with related results showing that shortcuts can flatten ordering while pure chains preserve it.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of peak activation to η^d and then applies the lemma that a positive base raised to any natural power remains positive.
why it matters
This result supports the practical reach bound in causal chains, feeding into the claim that 8 ticks suffice for chains up to about 5 hops when η = 1/φ² ≈ 0.382 and ε = 0.01. It closes a small but necessary positivity check in the Recognition Science forcing chain analysis of propagation limits. The module's key results tie this to the question of whether the octave length accommodates detectable multi-hop causality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.