Design | Chapter 7 | Prerequisites: 6-Ternary-Navigation | 24 min read | Home
7. Connection to Mutation Theory
The Mutation Theory corpus provides formal guarantees applicable to Wayfinder's navigational search. These connections are structural correspondences, not loose analogies — theorem proving is the ML application domain most naturally aligned with formal learning theory (exact verification oracle, well-defined state space, decomposable structure). See WAYFINDER_RESEARCH.md Section 2.7-2.8 for the full argument.
7.1 Convergence Guarantees
Theorem (Trajectory Monotonicity, T7.0): Killed sets grow monotonically along well-structured trajectories.
Application: In ModelAtlas terms: as you add constraints (require/prefer/avoid anchors), the candidate set monotonically shrinks. In proof search terms: each successful tactic application monotonically reduces the survivor set (remaining open goals). The Lyapunov monotonicity theorem (T7.5) guarantees convergence when the progress head's estimate (remaining steps) decreases at each step. This connects progress prediction → Lyapunov estimate → T7.5 → formal convergence guarantee.
Research direction: Existing work on proof complexity measures (proof tree depth, cut-rank, quantifier depth) may provide better Lyapunov function candidates than raw step count. See Phase 2.0 literature review.
7.2 Phase Transition
Theorem (Phase Transition, T7.3): Greedy kill trajectories exhibit a structural transition step: initial rapid progress followed by a harder regime.
Application: The first 1-3 tactics in most proofs are easy (intro, unfold, basic rewrites — near the origin in proof space). The hard part is finding the right deep lemma (far from origin, requiring specific anchors). The phase transition is precisely where navigational retrieval matters most — after the easy tactics, the model must navigate to specific, rare anchors in specialized regions of the semantic network.
7.3 Fixed-Point Partition
Theorem (fixedPointPartition, T4): The mutant space partitions into Killed × Equivalent × DistinguishableSurvivors.
Application: The proof space partitions identically:
| Mutation Theory Partition | Scoring Signal | Role |
| Killed vs. Survivor | bank_alignment | Right region of proof space? |
| Equivalent detection | anchor_relevance | Semantic labels match? (IDF-weighted) |
| Distinguishable → navigate to known | seed_similarity | Similar to already-solved patterns? |
The three-signal multiplicative scoring structure mirrors this three-way partition.
7.4 Decomposition Optimality
Theorem (Separable Independent Testing, T3): When a system decomposes into independent components, each can be tested independently with additive (not multiplicative) cost.
Application: The SubgoalDecomposer's decision to create have subgoals is formally justified when the subgoals are independent. Independent subgoals can be solved with separate navigational queries, and the total compute is Σ solve_cost(subgoal_i), not Π. Independence can be verified by checking whether subgoals share anchors — shared anchors suggest dependency.
7.5 Teaching Dimension
Theorem (TD = κ, T5.17): Teaching dimension equals specification complexity.
Application: The minimum number of premises needed to uniquely determine a proof is bounded by the specification complexity of the theorem. This provides a formal lower bound on the premise_candidates parameter: if a theorem's specification complexity is 4, retrieving 3 premises is provably insufficient. The proof network's anchor count per theorem approximates specification complexity.
Sources: docs/WAYFINDER_DESIGN.md