feat(missions): cross-campaign dependency edges, with an anti-cascade rule

telperion/docs/CROSS_CAMPAIGN_EDGES_2026-09-19.md

@@ -0,0 +1,97 @@
+# Cross-campaign dependency edges in the missions registry (2026-09-19)
+
+*`conjecture1_proved = False`. This is registry plumbing, not mathematics.*
+
+## The problem
+
+`load_campaign` rejected any `depends_on` target outside its own campaign. The
+corpus is emphatically cross-campaign: mirrormere's Route-D nodes consume rh's
+`E6Bridge*` results on the `rvm_bridge` island. With no way to say so, authors
+reached for the nearest same-campaign proxy while the node title named the real
+source, and the 2026-09-18 registry audit found **five nodes whose dependency
+edges the corpus does not support**. The audit also found that all 44 live proof
+links are `via = direct`: the `reduction` mechanism, the one that actually
+consumes dependency edges, had never been used once.
+
+So the registry has been recording a chain of reductions toward a conjecture
+while in fact holding a collection of independent direct proofs. The edges were
+decorative. This change makes them mean something, which is also what makes it
+dangerous, hence the emphasis below.
+
+## The mechanism
+
+A `depends_on` entry is now one of:
+
+| form | meaning |
+|---|---|
+| `RH_corridor_bound` | a node in the same campaign (unchanged, still the default) |
+| `rh:RH_corridor_bound` | the node `RH_corridor_bound` in the campaign whose **directory** is `rh` |
+
+The campaign part is the directory name, not `manifest.name`: the directory is
+what `--campaign` takes and what a reference must resolve against (`rh`, not
+`RH.conjecture`).
+
+Three layers, deliberately separated:
+
+1. **`load_campaign(root)`** validates internal references exactly as before. An
+   external reference is checked for *syntax* and *file existence* only
+   (`<root>/../<campaign>/nodes/<slug>.toml`). It does not load the other
+   campaign, so there is no recursion and no load-order coupling.
+2. **`load_universe(missions_root)`** loads every campaign, resolves every
+   external reference for real, and asserts **global** acyclicity. A cycle like
+   `rh:A -> mm:B -> rh:A` is invisible to any per-campaign check by
+   construction; this is the layer that sees it.
+3. **`compute_universe_closures(universe)`** runs one global closure fixpoint
+   keyed by `(campaign, slug)`.
+
+`verify_campaign` auto-loads the sibling universe when it can, and falls back to
+`None` when it cannot, which leaves every external edge dirty.
+
+## The anti-cascade rule
+
+A cross-campaign edge is a new path for an unverified premise to reach a
+`proved` node. The 2026-09-18 audit *demonstrated*, on a throwaway campaign,
+that the gate could mark a node proved from a stub. So the rule here is stated
+as a single invariant and tested from the negative side:
+
+> An edge counts toward a clean closure only when its target genuinely
+> resolves, has status `proved`, **and** is itself closure-clean under the
+> global fixpoint. Every other case is dirty. There is no code path that turns
+> an unresolved, unproved, or dirty edge clean.
+
+Two specific traps, both of which bit during implementation and are now tests:
+
+- **No universe, external edge.** Returns dirty. A caller who forgets to pass
+  the universe gets a conservative answer, never an optimistic one.
+- **Never trust the target's stored flag.** The first implementation fell back
+  to the external node's stored `closure_clean` when no global pass was
+  available. That is exactly how transitive dirt launders across a boundary: a
+  reduction node's stored flag can read `True` while its own chain is dirty.
+  `test_transitive_dirt_propagates_across_campaigns` caught it. The fallback is
+  gone; the global fixpoint is computed instead.
+
+Note that a **direct** proof is unaffected by its dependency edges, by design:
+it stands on its artifact and the gate that checked it. Edges constrain
+`reduction` proofs. That asymmetry is why the registry could accumulate
+unsupported edges without any node becoming falsely clean.
+
+## What this does not do
+
+- It does not fix the five unsupported edges. Only one of them
+  (`MM_weil_form_certified_height`, which needs `rh:RH_rvm_unconditional`) is a
+  genuine cross-campaign case, and it lives on an unmerged branch. The other
+  four are dependency-correctness questions the mechanism cannot settle: a node
+  whose title refutes its own edges needs an author's judgement, not a syntax.
+- It does not make anything proved, and no node's status changes here.
+- It does not retro-fit `via = reduction` anywhere. The reduction relation is
+  now usable across campaigns; whether a given proof is a reduction remains a
+  claim its author must make and the gate must check.
+
+## Tests
+
+`tests/test_missions_cross_campaign.py`, 19 tests, most of them negative:
+malformed references, missing target, missing campaign, internal validation
+unchanged, global cycle detection, and six closure cases covering unproved,
+proved-but-dirty, no-universe, transitive dirt, and the direct-proof asymmetry.
+The full mission subset stays green at 331 passed, and all four real campaigns
+load as a universe and verify OK.

telperion/src/telperion/missions/registry.py

@@ -45,6 +45,59 @@ class Campaign:
     manifest: MissionManifest
     nodes: Dict[str, Node]   # keyed by slug
 
+    @property
+    def cname(self) -> str:
+        """The campaign's on-disk directory name -- its identity in a dep ref.
+
+        Deliberately the directory name, not ``manifest.name``: the directory is
+        what the CLI's ``--campaign`` takes and what a cross-campaign reference
+        must resolve against (``rh``, not ``RH.conjecture``).
+        """
+        return self.root.name
+
+
+# ---------------------------------------------------------------------------
+# Cross-campaign dependency references
+#
+# A depends_on entry is either a bare slug (same campaign, unchanged) or a
+# qualified reference "<campaign-dir>:<NodeSlug>", e.g. "rh:RH_rvm_unconditional".
+# The qualified form exists because real dependencies cross campaigns: the
+# mirrormere D3 node genuinely needs the rh cumulative-RvM theorem.  Before this
+# existed, authors substituted a same-campaign proxy while the node title named
+# the real source, which put five unsupported edges in the registry.
+# ---------------------------------------------------------------------------
+
+DEP_SEP = ":"
+
+
+def parse_dep(dep: str, home: str) -> tuple:
+    """Split a depends_on entry into ``(campaign_dir, slug)``.
+
+    ``home`` is the referring campaign's directory name, used for bare slugs.
+    Raises SchemaError on a malformed reference.
+    """
+    if DEP_SEP not in dep:
+        if not dep:
+            raise SchemaError("empty depends_on entry")
+        return (home, dep)
+    camp, _, slug = dep.partition(DEP_SEP)
+    if not camp or not slug or DEP_SEP in slug:
+        raise SchemaError(
+            f"malformed cross-campaign reference {dep!r}; "
+            f"expected '<campaign>{DEP_SEP}<NodeSlug>'"
+        )
+    return (camp, slug)
+
+
+def is_external(dep: str, home: str) -> bool:
+    """True iff *dep* names a node in a campaign other than *home*."""
+    return parse_dep(dep, home)[0] != home
+
+
+def dep_ref(campaign: str, slug: str) -> str:
+    """Render a qualified reference."""
+    return f"{campaign}{DEP_SEP}{slug}"
+
 
 # ---------------------------------------------------------------------------
 # Load
@@ -75,13 +128,26 @@ def load_campaign(root: Path) -> Campaign:
                 )
             nodes[sl] = node
 
-    # Validate depends_on references
+    # Validate depends_on references.  Internal refs must be present in this
+    # campaign; external refs are checked by file existence only -- resolving
+    # them fully would recurse across campaigns, so full cross-campaign
+    # validation (including global acyclicity) lives in load_universe.
+    home = root.name
     for sl, node in nodes.items():
         for dep in node.depends_on:
-            if dep not in nodes:
-                raise SchemaError(
-                    f"Node {sl!r} depends_on {dep!r} which is not in the campaign."
-                )
+            camp, target = parse_dep(dep, home)
+            if camp == home:
+                if target not in nodes:
+                    raise SchemaError(
+                        f"Node {sl!r} depends_on {dep!r} which is not in the campaign."
+                    )
+            else:
+                ext = root.parent / camp / "nodes" / f"{target}.toml"
+                if not ext.is_file():
+                    raise SchemaError(
+                        f"Node {sl!r} depends_on external {dep!r}, but no such node "
+                        f"file exists at {ext}."
+                    )
 
     campaign = Campaign(root=root, manifest=manifest, nodes=nodes)
     assert_acyclic(campaign)
@@ -92,6 +158,17 @@ def load_campaign(root: Path) -> Campaign:
 # DAG invariants
 # ---------------------------------------------------------------------------
 
+def _internal_deps(campaign: Campaign, slug: str) -> List[str]:
+    """This node's same-campaign dependency slugs (external refs dropped)."""
+    home = campaign.cname
+    out = []
+    for dep in campaign.nodes[slug].depends_on:
+        camp, target = parse_dep(dep, home)
+        if camp == home:
+            out.append(target)
+    return out
+
+
 def assert_acyclic(campaign: Campaign) -> None:
     """Raise SchemaError naming a cycle if the dependency graph is cyclic."""
     # Iterative DFS with three-colour marking: 0=unvisited, 1=in-stack, 2=done
@@ -102,7 +179,7 @@ def assert_acyclic(campaign: Campaign) -> None:
         if color[start] != WHITE:
             continue
         # DFS stack holds (slug, iterator-over-its-deps)
-        stack: List[tuple] = [(start, iter(campaign.nodes[start].depends_on))]
+        stack: List[tuple] = [(start, iter(_internal_deps(campaign, start)))]
         color[start] = GREY
 
         while stack:
@@ -131,6 +208,102 @@ def assert_acyclic(campaign: Campaign) -> None:
 # Open-leaves query
 # ---------------------------------------------------------------------------
 
+
+# ---------------------------------------------------------------------------
+# Universe: every campaign under one missions root, with cross-campaign edges
+# ---------------------------------------------------------------------------
+
+@dataclass
+class Universe:
+    root: Path
+    campaigns: Dict[str, Campaign]   # keyed by directory name
+
+    def resolve(self, home: str, dep: str) -> Optional[Node]:
+        """The Node a depends_on entry names, or None if it does not resolve.
+
+        None is the conservative answer everywhere it is used: an edge that does
+        not resolve must never be treated as satisfied.
+        """
+        camp, target = parse_dep(dep, home)
+        c = self.campaigns.get(camp)
+        if c is None:
+            return None
+        return c.nodes.get(target)
+
+
+def load_universe(missions_root: Path) -> Universe:
+    """Load every campaign under *missions_root* and validate all edges.
+
+    A campaign directory is one containing ``mission.toml``.  Raises SchemaError
+    if any cross-campaign reference does not resolve, or if the GLOBAL graph
+    (internal and external edges together) contains a cycle.
+    """
+    missions_root = Path(missions_root)
+    campaigns: Dict[str, Campaign] = {}
+    for d in sorted(missions_root.iterdir()):
+        if d.is_dir() and (d / "mission.toml").is_file():
+            campaigns[d.name] = load_campaign(d)
+    uni = Universe(root=missions_root, campaigns=campaigns)
+
+    for cname, camp in campaigns.items():
+        for sl, node in camp.nodes.items():
+            for dep in node.depends_on:
+                if not is_external(dep, cname):
+                    continue
+                if uni.resolve(cname, dep) is None:
+                    raise SchemaError(
+                        f"Node {cname}:{sl} depends_on {dep!r}, which does not "
+                        f"resolve to a node in this missions root."
+                    )
+    assert_acyclic_universe(uni)
+    return uni
+
+
+def assert_acyclic_universe(uni: Universe) -> None:
+    """Raise SchemaError naming a cycle in the GLOBAL dependency graph.
+
+    Internal cycles are already rejected per campaign; this catches the ones a
+    per-campaign check structurally cannot see, e.g. rh:A -> mm:B -> rh:A.
+    """
+    WHITE, GREY, BLACK = 0, 1, 2
+    color: Dict[tuple, int] = {}
+    for cname, camp in uni.campaigns.items():
+        for sl in camp.nodes:
+            color[(cname, sl)] = WHITE
+
+    def deps_of(key: tuple) -> List[tuple]:
+        cname, sl = key
+        node = uni.campaigns[cname].nodes[sl]
+        out = []
+        for dep in node.depends_on:
+            camp, target = parse_dep(dep, cname)
+            if (camp, target) in color:
+                out.append((camp, target))
+        return out
+
+    for start in list(color):
+        if color[start] != WHITE:
+            continue
+        stack: List[tuple] = [(start, iter(deps_of(start)))]
+        color[start] = GREY
+        path: List[tuple] = [start]
+        while stack:
+            key, it = stack[-1]
+            try:
+                nxt = next(it)
+            except StopIteration:
+                color[key] = BLACK
+                stack.pop()
+                path.pop()
+                continue
+            if color.get(nxt) == GREY:
+                cyc = " -> ".join(f"{c}{DEP_SEP}{s}" for c, s in path + [nxt])
+                raise SchemaError(f"cross-campaign dependency cycle: {cyc}")
+            if color.get(nxt) == WHITE:
+                color[nxt] = GREY
+                path.append(nxt)
+                stack.append((nxt, iter(deps_of(nxt))))
+
 def open_leaves(
     campaign: Campaign,
     claims: Optional[Dict[str, Claim]] = None,