diff --git a/docs/decisions/ADR-0136.S2-post-rescan.md b/docs/decisions/ADR-0136.S2-post-rescan.md index 96aa63da..1d4439cf 100644 --- a/docs/decisions/ADR-0136.S2-post-rescan.md +++ b/docs/decisions/ADR-0136.S2-post-rescan.md @@ -103,6 +103,38 @@ next structural barrier. Only 3 `context_filler` cases remain blocking (0022, > (DeferredCandidate, evidence, BindingProof) triple. Short-circuits are kept > only as regression fixtures. +### Update 2026-05-23: ADR-0137 attempted and deferred + +ADR-0137 was drafted and rescoped against this ledger (PR #204), then **closed +without merging** on self-review. The reason is structural, not procedural: + +The DeferredCandidate / BindingProof apparatus is the right shape for *true* +retrospective binding — where a first-pass candidate has open slots that only +later-sentence evidence can fill. Re-examining S.1/S.2 against that definition +showed neither short-circuit fits it: + +- **0014**: `CandidateCapacity` (sentence 1) and `CandidateCapacityQuestion` + (sentence 2) are both fully grounded. What's needed is a **join rule** + pairing them into a derived `InitialPossession`, not a deferred-binding pass. +- **0042**: `CandidateInitial` (sentence 1) and `CandidateConditionalOpQuestion` + (sentence 2) are both fully grounded — same shape, same join. + +With no kind that has genuinely open slots in the v2 ledger, the binding +machinery would degenerate to a join everywhere it ran. Building it now would +be speculative infrastructure ahead of a forcing function — explicitly the +pattern CLAUDE.md warns against. + +**What stays.** The S.1/S.2 short-circuits in `parse_and_solve` remain as +tactical bridges. `wrong == 0` is preserved. The canonical +`evals/gsm8k_math/runner.py` staleness on short-circuit admissions (it asserts +`selected_graph is not None`) is a real annoyance but better fixed in the +runner — teach it to score short-circuit admissions — than by inventing a +binding layer to give every admission a graph. + +**Reopen criterion.** ADR-0137 (or its successor) may be revisited when a +case appears whose first-pass candidate has genuinely open slots that only +later-sentence evidence can close. Until then, the unlock vehicle is S.x. + ## ADR-0137 Probe Cases The following cases are required in the ADR-0137 probe to verify subsumption