shortcut_simultaneous_activation
In a shortcut graph with positive blend rate η, if the shortcut weight to C meets or exceeds the chain weight to B, then the scaled activation to C meets or exceeds that to B at the first tick. Modelers of SpMV propagation in graphs with bidirectional edges cite this to quantify how shortcuts equalize first-tick activations. The proof applies the monotonicity of positive scalar multiplication directly to the weight inequality.
claimLet $G$ be a shortcut graph with weights $w_{AB}$ and $w_{AC}$ for the direct and shortcut edges. For any blend rate $η > 0$, if $w_{AC} ≥ w_{AB}$ then $η · w_{AC} ≥ η · w_{AB}$.
background
The module examines whether sparse matrix-vector multiplication preserves causal ordering in directed graphs. ShortcutGraph models a structure with a direct edge A to B and a shortcut A to C, both at distance 1. The doc-comment notes that C receives signal at tick 1 via shortcut simultaneously with B. Upstream results include reversal maps on Fin 8 and spectral properties from asteroid spectroscopy, though the core relies on the graph definition itself. The local setting addresses whether 8-tick octaves suffice for multi-hop propagation and if shortcuts flatten causality.
proof idea
The proof is a one-line wrapper applying mul_le_mul_of_nonneg_left to the weight comparison under the positivity of η.
why it matters in Recognition Science
This result supports the module's demonstration that shortcuts destroy causal ordering, as seen in related statements like bidirectional_destroys_ordering. It fills the step showing simultaneous activation at tick 1 when weights satisfy the inequality. In the Recognition framework it connects to the eight-tick octave and causal propagation questions. No open questions are directly touched here.
scope and limits
- Does not establish ordering preservation without the weight condition.
- Does not address multi-tick propagation beyond the first tick.
- Does not apply to negative blend rates.
- Does not quantify the difference in activations.
formal statement (Lean)
109theorem shortcut_simultaneous_activation (g : ShortcutGraph) (η : ℝ)
110 (hη_pos : 0 < η) (h_weights : g.weight_AC ≥ g.weight_AB) :
111 η * g.weight_AC ≥ η * g.weight_AB := by
proof body
Term-mode proof.
112 exact mul_le_mul_of_nonneg_left h_weights (le_of_lt hη_pos)
113
114/-- Bidirectional edges (like SBERT kNN) create shortcuts for every typed bond.
115 If gravity→acceleration has weight w_cause and acceleration→gravity has weight w_back,
116 the reverse edge is a shortcut that allows "effect" to activate "cause" as fast as
117 "cause" activates "effect". Causal ordering is destroyed. -/