diff --git a/src/pacta/lean.py b/src/pacta/lean.py
index eca5936..882bef5 100644
--- a/src/pacta/lean.py
+++ b/src/pacta/lean.py
@@ -320,10 +320,22 @@ def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[s
     results: dict[str, list[str]] = {}
     lines = output.splitlines()
     for cert in certificates:
+        # Anchor on the exact quoted name Lean prints ('X' depends on … /
+        # 'X' does not depend on any axioms). A bare substring match would
+        # let 'Foo' hit the line for 'Foo_bar' first.
+        needle = f"'{cert}'"
         cert_results: list[str] | None = None
         for i, line in enumerate(lines):
-            if cert not in line:
+            if needle not in line:
                 continue
+            # Axiom-free certificates print a bracketless sentence. Decide
+            # on THIS line before opening any window: a window would reach
+            # into the NEXT certificate's bracket and steal its cone (found
+            # by the entry-13 rehearsal — the accumulator corpus is the
+            # first subject with axiom-free certificates).
+            if _mentions_no_axioms(line):
+                cert_results = []
+                break
             # Lean wraps long axiom lists (the apex tiers carry 11 axioms)
             # across many lines; take a window wide enough for the largest
             # documented boundary and flatten it before matching, the same
@@ -333,9 +345,6 @@ def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[s
             if bracket:
                 cert_results = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
                 break
-            if _mentions_no_axioms(window):
-                cert_results = []
-                break
         if cert_results is not None:
             results[cert] = cert_results
     return results
diff --git a/tests/test_lean.py b/tests/test_lean.py
index c075fd9..126590e 100644
--- a/tests/test_lean.py
+++ b/tests/test_lean.py
@@ -24,6 +24,34 @@ def test_parse_axiom_output_no_axioms_wording():
     assert parsed["CurveFieldProofs.fieldImplementation"] == []
 
 
+def test_parse_axiom_output_axiom_free_cert_does_not_steal_next_cone():
+    # Regression (found by the entry-13 rehearsal, 2026-07-16): an
+    # axiom-free certificate is followed by a cone-carrying one. The old
+    # windowed search reached past the bracketless "does not depend"
+    # sentence and attributed the NEXT certificate's cone. The
+    # accumulator corpus is the first subject with axiom-free
+    # certificates (domsep, Hash, instDecidableEqHash, take_append_drop),
+    # so no fork attestation ever exercised this path.
+    output = (
+        "'LTLAcc.domsep' does not depend on any axioms\n"
+        "'LTLAcc.eq_dropLast_append_of_getLast?' depends on axioms: [propext]\n"
+    )
+    parsed = parse_axiom_output(output, ["LTLAcc.domsep", "LTLAcc.eq_dropLast_append_of_getLast?"])
+    assert parsed["LTLAcc.domsep"] == []
+    assert parsed["LTLAcc.eq_dropLast_append_of_getLast?"] == ["propext"]
+
+
+def test_parse_axiom_output_exact_name_not_prefix():
+    # 'LTLAcc.MTH' must not match the line for 'LTLAcc.MTH_single' even
+    # when the latter comes first in the output.
+    output = (
+        "'LTLAcc.MTH_single' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+        "'LTLAcc.MTH' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+    )
+    parsed = parse_axiom_output(output, ["LTLAcc.MTH"])
+    assert parsed["LTLAcc.MTH"] == ["propext", "LTLAcc.sha256", "Quot.sound"]
+
+
 def test_mac_safe_lean_command_is_argument_list():
     tools = LeanTools(lean="/usr/local/bin/lean", lake=None)
     cmd = build_lean_invocation(Path("Proofs/A.lean"), tools, output_path=Path("Proofs/A.olean"), root_path=Path("."))