practical_reach_bound
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 η.
claimLet $η,ε∈ℝ$ 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit hop bound d < log(ε)/log(η).
- Does not incorporate the specific Recognition Science value η = 1/φ².
- Does not address ordering preservation or shortcut effects.
- Does not quantify detection in the presence of noise or multiple paths.
formal statement (Lean)
139theorem practical_reach_bound (η ε : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1)
140 (hε_pos : 0 < ε) (hε_lt : ε < 1) (d : ℕ)
141 (h_exceeds : peak_activation η d ≥ ε) :
142 peak_activation η d > 0 := by
proof body
Term-mode proof.
143 unfold peak_activation
144 exact pow_pos hη_pos d
145
146/-- With η = 1/φ² ≈ 0.382, activation at hop 5 is η^5 ≈ 0.008.
147 This means 5-hop causal chains are detectable but weak.
148 For ε = 0.01, practical reach is ~4.8 hops. -/