Design | Chapter 4 | Prerequisites: 3-Scoring-System | 24 min read | Home
4. Spreading Activation
Priority-queue Bellman-Ford from seed nodes, adapted from ModelAtlas.
4.1 Two Channels
Link channel (Layer 1): Traverse entity_links bidirectionally. Activation decays by link weight × hop decay (0.8 per hop). A depends_on link (weight 0.9) transmits 72% of activation per hop. A commonly_co_occurs link (weight 0.6) transmits 48%.
Anchor channel (Layer 2): Find entities sharing anchors with the current node. Activation weighted by fraction of shared anchors. A entity sharing 8/10 of the current node's anchors receives higher activation than one sharing 2/10.
4.2 Bank Scoping
If the current proof is about algebra (DOMAIN ≤ 0), only spread through DOMAIN-bank anchors. This prevents topology lemmas from activating during algebra proofs via shared generic anchors like equality.
4.3 Parameters
| Parameter | Value | Rationale |
max_depth | 3 | Beyond 3 hops, activation is too diluted to be meaningful |
decay | 0.8 | 20% loss per hop — aggressive enough to focus, gentle enough to explore |
neighbor_slice | 20 | Max link neighbors per node — prevents explosion |
anchor_slice | 30 | Max anchor co-occurrences per node |
4.4 Dynamic Seeds
Seeds change as the proof progresses:
- Initially: Just the theorem's goal state entity.
- After each successful tactic: Add the used lemmas and the new subgoal states as seeds.
- After each failure: Add the failed tactic/premise to an "avoid" set that dampens their activation.
This creates a feedback loop: successful proof steps refine the search space, making subsequent steps more likely to find relevant lemmas.
Sources: docs/WAYFINDER_DESIGN.md