feat: binding-graph acyclicity invariant — circular_dependency guard (ADR-0203)

proof_chain phase 2.1: the acyclicity guard at the shared binding-graph
construction boundary, before phase 2.2 wiring can build a cyclic-capable structure.

- generate/binding_graph/acyclicity.py: pure find_cycle(adjacency) detector
  (deterministic three-colour DFS; isolated, no model import).
- model.py __post_init__: builds {lhs: deps} adjacency over equations and raises
  BindingGraphError(circular_dependency ...) on a cycle. Runs on every binding
  graph (math + future proof) — illegal states unrepresentable for all consumers.
- tests/test_binding_graph_acyclicity.py: 17 tests (pure checker + construction
  enforcement); mutation-verified non-vacuous.
- ADR-0203: new ADDITIVE invariant referencing ADR-0132 (not an amendment —
  preserves the why-added-later history).

Math-lane regression proof: the only producer (math adapter) is acyclic by
construction (fresh result symbol per op, deps point backward); full
binding-graph + admissibility surface 392 green; guard refuses no existing graph.

Honesty boundary (load-bearing): through phase 2.3, proof_chain is SOUND OVER
DECLARED ATOMS, not grounded in recognized input (grounding is phase 2.4).

full binding-graph/admissibility surface: 392 passed. smoke: 67 passed.

docs/decisions/ADR-0203-binding-graph-acyclicity-invariant.md

@@ -0,0 +1,107 @@
+# ADR-0203 — Binding-Graph Acyclicity Invariant (`circular_dependency` refusal)
+
+**Status:** Accepted (proof_chain phase 2.1 — the isolated guard; ADR-0201 §Deferred)
+**Date:** 2026-06-02
+**Relates to:** **ADR-0132** (binding-graph data model — this *adds* an invariant to
+its construction contract; see §amend-vs-additive), ADR-0201 (canonicalizer +
+phase plan), ADR-0202 (proposition representation contract).
+
+---
+
+## Context
+
+ADR-0132's `SemanticSymbolicBindingGraph.__post_init__` enforces **referential
+integrity** (every `BoundEquation` dependency names a known symbol) but **not
+acyclicity**. A cycle in the equation dependency structure — `x` defined from `y`,
+`y` defined from `x`, or a self-dependency `x ← x` — is **circular reasoning**:
+structurally well-formed, semantically invalid. It is the proof-domain analog of
+the `20/5 == 4` class the arithmetic gate refuses.
+
+`proof_chain` (ADR-0201) is the first consumer that can *build* such a structure:
+its phase 2.2 wiring constructs binding graphs from proofs, where a malformed proof
+could close a dependency loop. Per CORE's "build the defensive refusal NOW"
+discipline, the guard must exist **before** the structure where a cycle can exist —
+so this phase (2.1) lands it *before* any 2.2 wiring.
+
+## Decision
+
+Add an **acyclicity invariant** to binding-graph construction:
+
+- **`generate/binding_graph/acyclicity.py`** — a pure `find_cycle(adjacency)`
+  cycle detector (deterministic three-colour DFS; sorted traversal → byte-stable
+  reported cycle; self-edge → length-1 cycle). No model import — testable in
+  isolation against synthetic adjacency graphs.
+- **Enforcement at the shared construction boundary.** `__post_init__` builds a
+  `{lhs_symbol_id: ⋃ dependencies}` adjacency over its equations and calls
+  `find_cycle`; a non-`None` result raises
+  `BindingGraphError("circular_dependency: equation dependency cycle …")` naming
+  the cycle. This runs on **every** binding graph — math and (future) proof alike —
+  making a cyclic graph unrepresentable for all consumers.
+
+### Why the shared `__post_init__` (not a proof-only check)
+
+Putting it at the substrate boundary closes the gap universally and makes illegal
+states unrepresentable (the CLAUDE.md design principle), rather than leaving the
+math binding graph cycle-unchecked. The guard exists the instant the structure
+becomes constructible — strictly *before* the proof wiring that makes a cycle
+reachable.
+
+### Math-lane regression proof (the shared-constructor risk)
+
+Because the guard runs on the existing math/algebra path too, it must refuse no
+existing graph. Verified:
+
+- The **only** production producer is `generate/binding_graph/adapter.py`
+  (`bind_math_problem_graph`). It mints a **fresh** result symbol per operation
+  (`_op_result_symbol_id(idx)`) and depends only on symbols that already exist —
+  edges point strictly backward in construction order. It is therefore **acyclic
+  by construction** and cannot produce a graph this guard would refuse.
+- No existing test constructs a dependency cycle (the `sym_ghost` fixture is the
+  referential-integrity refusal, not a cycle).
+- The **full binding-graph + admissibility test surface — 392 tests — stays
+  green** with the guard in `__post_init__`. (Smoke: 67 passed.)
+
+A future/in-flight consumer that *did* build a cycle would now be refused at
+construction — which is the point.
+
+## amend-vs-additive (ADR-0203 vs amending ADR-0132)
+
+**Decision: a new additive ADR (this one) that references ADR-0132 — not an
+amendment of the closed record.**
+
+ADR-0132 is `Accepted`. The acyclicity invariant was not part of its original
+decision; it became necessary later, when `proof_chain` made cycles *reachable*.
+Recording it as a new invariant preserves that history — *why* the guard was added
+and *when it became load-bearing* — which an in-place edit of the closed record
+would erase. This mirrors the history-vs-current-state discipline used elsewhere
+(append the new fact; don't rewrite the settled one). The code lives beside
+ADR-0132's referential-integrity check in `__post_init__`; the *decision record* is
+additive.
+
+## Honesty boundary (load-bearing — carried by every phase-2 ADR, 0203–0205)
+
+Through phase 2.3, `proof_chain` is **sound over its declared atoms** — it does
+**not** reason over recognized input. Atoms are opaque/declared symbol ids
+(ADR-0202); grounding them to ADR-0144 `EpistemicNode`/`FeatureBundle` carriers is
+**phase 2.4** (fork B). This must **never** be softened to "reasons over input"
+before 2.4 lands. This ADR is structure-only and makes no grounding claim; it is
+named here so the boundary travels with the work, not just with the rule ADRs.
+
+## Evidence
+
+- `tests/test_binding_graph_acyclicity.py` — 17 tests: pure checker (acyclic→None;
+  self-loop/2-/3-cycle/cycle-with-tail detected; deterministic), construction
+  enforcement (cyclic + self-dependent refuse; acyclic + adapter-shape construct),
+  and referential-integrity-still-fires-first.
+- **Mutation-verified non-vacuous:** neutering `find_cycle` (→ always `None`) makes
+  a 2-cycle construct without refusal — `test_two_cycle_equation_set_refuses` would
+  fail. The guard is load-bearing, not decoration.
+- Full binding-graph/admissibility surface: **392 passed**. Smoke: **67 passed**.
+
+## Deferred (not in this phase)
+
+- **2.2** — proof-graph builder (proof → `BoundEquation`s; `canonical_key` →
+  `rhs_canonical`); the first construction that exercises this guard through the
+  real proof path (ADR-0204).
+- **2.3** — `modus_ponens` + the disagreement rule (ADR-0205).
+- **2.4** — atom→`EpistemicNode` carrier grounding (ADR-0206).

generate/binding_graph/__init__.py

@@ -21,6 +21,7 @@ Phase 5 (bounded-grammar / B3 integration) deferred.
 
 from __future__ import annotations
 
+from .acyclicity import CIRCULAR_DEPENDENCY, find_cycle
 from .adapter import (
     INTRODUCED_BY,
     REFUSED_UNIT_PROOF,
@@ -73,6 +74,7 @@ from .units import (
 __all__ = (
     "ADMISSIBILITY_REASONS",
     "ADMISSIBILITY_STATUSES",
+    "CIRCULAR_DEPENDENCY",
     "BASE_DIMENSIONS",
     "DIMENSIONLESS",
     "INTRODUCED_BY",
@@ -102,6 +104,7 @@ __all__ = (
     "bind_math_problem_graph",
     "bound_unknown_from_math_problem_graph",
     "check_admissibility",
+    "find_cycle",
     "infer_question_form",
     "parse_unit",
     "resolve_state_index",

generate/binding_graph/acyclicity.py

@@ -0,0 +1,91 @@
+"""ADR-0203 — Acyclicity invariant for the binding-graph dependency structure.
+
+Pure cycle detection over a ``{node: successors}`` adjacency, isolated from the
+binding-graph model so it is testable against synthetic graphs with no
+binding-graph construction. The model's ``__post_init__`` adapts its equations
+into an adjacency and calls :func:`find_cycle`; a non-``None`` result is refused
+with the typed reason :data:`CIRCULAR_DEPENDENCY`.
+
+Why this exists (additive to ADR-0132, which it references): the ADR-0132 data
+model enforces *referential integrity* (every dependency names a known symbol) but
+not *acyclicity*. A cycle in the equation dependency structure is **circular
+reasoning** — concluding ``P`` because ``Q`` because ``P`` — the proof-domain
+analog of the ``20/5 == 4`` class: structurally well-formed, semantically invalid.
+``proof_chain`` is the first consumer that can build such a structure, so the guard
+lands at the shared construction boundary *before* that wiring exists (ADR-0201
+phase 2.1).
+
+On main today the only producer of binding graphs is the math adapter
+(`generate/binding_graph/adapter.py`), which mints a fresh result symbol per
+operation and depends only on symbols that already exist — edges point strictly
+backward in construction order, so it is **acyclic by construction**. This guard
+therefore refuses no existing graph; it protects the structure the moment a future
+consumer could build a cycle.
+
+Honesty boundary (carried by every phase-2 ADR, 0203–0205): through phase 2.3,
+``proof_chain`` is **sound over its declared atoms**, not grounded in recognized
+input. Atom→carrier grounding is phase 2.4. This module is structure-only and makes
+no grounding claim.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Mapping
+from typing import Final
+
+CIRCULAR_DEPENDENCY: Final[str] = "circular_dependency"
+
+
+def find_cycle(adjacency: Mapping[str, frozenset[str]]) -> tuple[str, ...] | None:
+    """Return a directed cycle as an ordered tuple ``(n0, …, nk, n0)``, or
+    ``None`` if the graph is acyclic.
+
+    ``adjacency`` maps a node to the set of nodes it points to (an equation's
+    ``lhs_symbol_id`` → the symbols it reads). Nodes that appear only as
+    successors (leaf dependencies defined by no equation) have no out-edges and
+    cannot start a cycle.
+
+    Deterministic: roots and successors are visited in sorted order, so the
+    reported cycle is byte-stable across runs (the replay discipline). A node
+    listing itself as a successor is reported as a length-1 self-cycle
+    ``(n, n)``.
+    """
+    WHITE, GREY, BLACK = 0, 1, 2
+    color: dict[str, int] = {node: WHITE for node in adjacency}
+    for succs in adjacency.values():
+        for succ in succs:
+            color.setdefault(succ, WHITE)
+
+    def successors(node: str) -> list[str]:
+        return sorted(adjacency.get(node, frozenset()))
+
+    # Iterative three-colour DFS (iterative to avoid recursion limits on long
+    # dependency chains). GREY = on the current DFS path; a GREY successor is a
+    # back-edge, i.e. a cycle.
+    for root in sorted(color):
+        if color[root] != WHITE:
+            continue
+        path: list[str] = [root]
+        stack: list[tuple[str, list[str]]] = [(root, successors(root))]
+        color[root] = GREY
+        while stack:
+            node, succs = stack[-1]
+            descended = False
+            while succs:
+                nxt = succs.pop(0)
+                state = color[nxt]
+                if state == GREY:
+                    start = path.index(nxt)
+                    return tuple(path[start:] + [nxt])
+                if state == WHITE:
+                    color[nxt] = GREY
+                    path.append(nxt)
+                    stack.append((nxt, successors(nxt)))
+                    descended = True
+                    break
+                # BLACK: fully explored, no cycle through it — skip.
+            if not descended:
+                color[node] = BLACK
+                path.pop()
+                stack.pop()
+    return None

generate/binding_graph/model.py

@@ -19,6 +19,8 @@ from __future__ import annotations
 from dataclasses import dataclass, field
 from typing import Final, Literal, Union
 
+from generate.binding_graph.acyclicity import CIRCULAR_DEPENDENCY, find_cycle
+
 # ---------------------------------------------------------------------------
 # Public errors
 # ---------------------------------------------------------------------------
@@ -464,6 +466,24 @@ class SemanticSymbolicBindingGraph:
                         f"{dep!r} (lhs={eq.lhs_symbol_id!r})"
                     )
 
+        # ADR-0203 — acyclicity invariant. Referential integrity (above) proves
+        # every dependency names a known symbol; this proves the equation
+        # dependency structure has no cycle. A cycle is circular reasoning
+        # (conclude P because Q because P) — structurally well-formed, invalid.
+        # The math adapter is acyclic by construction, so this refuses no
+        # existing graph; it guards the structure before proof_chain (the first
+        # consumer that could build a cycle) wires in. Multiple equations sharing
+        # an lhs union their dependencies.
+        adjacency: dict[str, set[str]] = {}
+        for eq in self.equations:
+            adjacency.setdefault(eq.lhs_symbol_id, set()).update(eq.dependencies)
+        cycle = find_cycle({lhs: frozenset(deps) for lhs, deps in adjacency.items()})
+        if cycle is not None:
+            raise BindingGraphError(
+                f"{CIRCULAR_DEPENDENCY}: equation dependency cycle "
+                f"{' -> '.join(cycle)}"
+            )
+
         equation_count = len(self.equations)
         for unk in self.unknowns:
             if unk.symbol_id not in known_ids:

tests/test_binding_graph_acyclicity.py

@@ -0,0 +1,167 @@
+"""ADR-0203 — acyclicity guard for the binding-graph dependency structure.
+
+Two layers, both exercised here:
+
+1. The **pure checker** (`find_cycle`) in isolation against synthetic adjacency
+   graphs — no binding-graph construction. Cyclic graphs return the cycle;
+   acyclic graphs return None; fails-loud under mutation (the equivalent
+   cyclic/acyclic assertions are mutually constraining, so a neutered detector
+   fails the suite).
+2. The **construction-boundary enforcement** in
+   `SemanticSymbolicBindingGraph.__post_init__` — a cyclic equation set raises
+   `BindingGraphError(circular_dependency …)`; an acyclic set (including the
+   math-adapter shape: fresh result symbol per op, deps point backward)
+   constructs fine — the math-lane regression proof.
+"""
+
+from __future__ import annotations
+
+import pytest
+
+from generate.binding_graph import (
+    CIRCULAR_DEPENDENCY,
+    BindingGraphError,
+    BoundEquation,
+    SemanticSymbolicBindingGraph,
+    SourceSpanLink,
+    SymbolBinding,
+    find_cycle,
+)
+
+
+# ---------------------------------------------------------------------------
+# Layer 1 — pure checker, isolated
+# ---------------------------------------------------------------------------
+
+ACYCLIC_GRAPHS = [
+    {},                                                         # empty
+    {"a": frozenset()},                                         # single, no edges
+    {"a": frozenset({"b"}), "b": frozenset({"c"})},             # linear chain
+    {"a": frozenset({"b", "c"}), "b": frozenset({"d"}),
+     "c": frozenset({"d"}), "d": frozenset()},                  # diamond / shared dep
+    {"a": frozenset({"b", "c", "d"})},                          # leaves not defined by any eq
+]
+
+
+@pytest.mark.parametrize("graph", ACYCLIC_GRAPHS)
+def test_acyclic_graphs_return_none(graph) -> None:
+    assert find_cycle(graph) is None
+
+
+CYCLIC_GRAPHS = [
+    {"a": frozenset({"a"})},                                    # self-loop
+    {"a": frozenset({"b"}), "b": frozenset({"a"})},             # 2-cycle
+    {"a": frozenset({"b"}), "b": frozenset({"c"}),
+     "c": frozenset({"a"})},                                    # 3-cycle
+    {"t": frozenset({"a"}), "a": frozenset({"b"}),
+     "b": frozenset({"c"}), "c": frozenset({"b"})},             # cycle with a tail (t→a→b→c→b)
+]
+
+
+@pytest.mark.parametrize("graph", CYCLIC_GRAPHS)
+def test_cyclic_graphs_are_detected(graph) -> None:
+    cycle = find_cycle(graph)
+    assert cycle is not None
+    # A reported cycle closes on itself and every hop is a real edge.
+    assert cycle[0] == cycle[-1]
+    for src, dst in zip(cycle, cycle[1:]):
+        assert dst in graph[src], f"{src}->{dst} is not an edge"
+
+
+def test_self_loop_reported_as_length_one_cycle() -> None:
+    assert find_cycle({"x": frozenset({"x"})}) == ("x", "x")
+
+
+def test_reported_cycle_is_deterministic() -> None:
+    graph = {"a": frozenset({"b"}), "b": frozenset({"c"}), "c": frozenset({"a"})}
+    assert find_cycle(graph) == find_cycle(graph)
+
+
+# ---------------------------------------------------------------------------
+# Construction fixtures (mirror tests/test_binding_graph_model.py helpers)
+# ---------------------------------------------------------------------------
+
+
+def _span() -> SourceSpanLink:
+    return SourceSpanLink(source_id="src", start=0, end=3, text="xyz")
+
+
+def _sym(symbol_id: str) -> SymbolBinding:
+    return SymbolBinding(
+        symbol_id=symbol_id,
+        name=symbol_id,
+        semantic_role="quantity",
+        source_span=_span(),
+        introduced_by="test",
+    )
+
+
+def _eq(lhs: str, deps: set[str]) -> BoundEquation:
+    return BoundEquation(
+        lhs_symbol_id=lhs,
+        rhs_canonical=f"{lhs} := f({sorted(deps)})",
+        dependencies=frozenset(deps),
+        operation_kind="add",
+        unit_proof="pending",
+        admissibility_status="pending",
+        source_span=_span(),
+    )
+
+
+# ---------------------------------------------------------------------------
+# Layer 2 — enforcement at the shared construction boundary
+# ---------------------------------------------------------------------------
+
+
+def test_acyclic_equation_set_constructs() -> None:
+    # r1 := f(x);  r2 := f(r1, y)   — strict DAG, edges point backward.
+    syms = tuple(_sym(s) for s in ("x", "y", "r1", "r2"))
+    eqs = (_eq("r1", {"x"}), _eq("r2", {"r1", "y"}))
+    graph = SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert len(graph.equations) == 2
+
+
+def test_adapter_shape_is_acyclic_by_construction() -> None:
+    # Mirrors the math adapter: each op result depends only on prior symbols.
+    syms = tuple(_sym(s) for s in ("q0", "q1", "op_0", "op_1"))
+    eqs = (
+        _eq("op_0", {"q0", "q1"}),     # op_0 := q0 + q1
+        _eq("op_1", {"op_0", "q1"}),   # op_1 := op_0 + q1  (chains forward)
+    )
+    graph = SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert len(graph.equations) == 2
+
+
+def test_two_cycle_equation_set_refuses() -> None:
+    syms = (_sym("x"), _sym("y"))
+    eqs = (_eq("x", {"y"}), _eq("y", {"x"}))  # x↔y circular dependency
+    with pytest.raises(BindingGraphError) as exc:
+        SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert CIRCULAR_DEPENDENCY in str(exc.value)
+
+
+def test_self_dependent_equation_refuses() -> None:
+    syms = (_sym("x"),)
+    eqs = (_eq("x", {"x"}),)  # x defined in terms of itself
+    with pytest.raises(BindingGraphError) as exc:
+        SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert CIRCULAR_DEPENDENCY in str(exc.value)
+
+
+def test_longer_cycle_equation_set_refuses() -> None:
+    syms = tuple(_sym(s) for s in ("a", "b", "c"))
+    eqs = (_eq("a", {"b"}), _eq("b", {"c"}), _eq("c", {"a"}))
+    with pytest.raises(BindingGraphError) as exc:
+        SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert CIRCULAR_DEPENDENCY in str(exc.value)
+
+
+def test_referential_integrity_still_enforced_before_cycle_check() -> None:
+    # An unknown dependency is still the referential-integrity refusal, not a
+    # cycle — the existing ADR-0132 invariant is unchanged.
+    syms = (_sym("x"),)
+    eqs = (_eq("x", {"ghost"}),)
+    with pytest.raises(BindingGraphError) as exc:
+        SemanticSymbolicBindingGraph(symbols=syms, equations=eqs)
+    assert "unknown dependency" in str(exc.value)
+    assert CIRCULAR_DEPENDENCY not in str(exc.value)