core-labs/core
1
0
Fork 0
Code Issues 12 Pull requests Projects Releases Packages Wiki Activity Actions

docs(ADR-0136.S.2): record ADR-0137 attempt + deferral (#206)

Browse source 
PR #204 (ADR-0137 retrospective binding, rescoped to subsumption-only)
was drafted then closed without merging. The deferral reason is
structural: the DeferredCandidate/BindingProof apparatus is the right
shape for true retrospective binding (first-pass candidate has open
slots awaiting later evidence), but re-examination showed neither S.1
nor S.2 short-circuit fits that definition — both join two fully
grounded candidates. With no kind that has open slots in the v2
ledger, the machinery would degenerate to a join everywhere, which is
speculative infrastructure ahead of a forcing function (CLAUDE.md
warns against this pattern).

Update appended to the post-rescan notes so the deferral lives in the
repo, not just in a closed PR thread. Includes a reopen criterion:
ADR-0137 (or successor) may return when a case appears whose first-pass
candidate has genuinely open slots only later-sentence evidence can
close. Until then the unlock vehicle is S.x.

The S.1/S.2 short-circuits remain as tactical bridges; the canonical
runner staleness is better fixed in the runner than in a binding
layer.
This commit is contained in:
Shay 2026-05-23 21:55:48 -07:00 committed by GitHub
parent 684481910b
commit 6e11145282
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
docs/decisions/ADR-0136.S2-post-rescan.md
View file

@ -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