ShortcutGraph
ShortcutGraph defines a three-node graph with positive-weight edges A to B and A to C, modeling a shortcut that places C at distance 1 alongside the chain distance 2. Researchers analyzing SpMV causal ordering in recognition graphs cite it when testing whether shortcuts allow simultaneous activation at the first tick. The definition is a direct record structure with four fields for the two weights and their strict positivity.
claimA structure on positive reals $w_{AB}>0$ and $w_{AC}>0$ that equips nodes A, B, C with edges A→B and A→C, allowing C to receive signal at tick 1 via the shortcut while B receives it via the direct edge.
background
The module studies whether SpMV propagation on directed graphs preserves causal ordering or flattens it under shortcuts. It contrasts ordinary chains A→B→C (where activation time of B is strictly before C) with shortcut cases. Upstream, tick supplies the fundamental time quantum τ₀ = 1, while A denotes the active edge count per tick (equal to 1). The structure is introduced to capture bidirectional SBERT-style edges that create distance-1 shortcuts.
proof idea
This is a structure definition with no proof body. It directly declares the four fields: two real weights and the two positivity hypotheses 0 < weight_AB, 0 < weight_AC.
why it matters in Recognition Science
ShortcutGraph supplies the hypothesis type for the downstream theorem shortcut_simultaneous_activation, which proves that when w_AC ≥ w_AB the shortcut node C activates at least as strongly as B at tick 1. It directly addresses the module question of whether shortcuts destroy causal ordering, a prerequisite for the effective-reach bound of roughly 4.8 hops under blend rate 1/φ² and the claim that the 8-tick octave suffices for chains up to five hops.
scope and limits
- Does not encode the full adjacency matrix or any other edges.
- Does not contain activation thresholds or blend-rate parameters.
- Does not assert any ordering or equality of activation times.
- Does not restrict the weights beyond positivity.
formal statement (Lean)
100structure ShortcutGraph where
101 weight_AB : ℝ
102 weight_AC : ℝ
103 weight_AB_pos : 0 < weight_AB
104 weight_AC_pos : 0 < weight_AC
105
106/-- With a shortcut A→C, C receives signal at tick 1 (via shortcut) with weight w_AC,
107 simultaneously with B receiving signal at tick 1 with weight w_AB.
108 If w_AC ≥ w_AB, C activates at least as strongly as B at tick 1. -/