docs(framing): align A3 with the D0b contingency

Revision 10 retires D0b only as a precondition: a demonstrated D1/D2
mechanism may account directly for the subset/full difference, while a
mechanism that does not account for it triggers D0b before closure.

A3 still stated the old unconditional rule that D0 must recreate the
comparison in every case. Make the acceptance criterion match the
diagnostic decision: record the direct explanation when it exists;
otherwise run D0b under captured provenance and explain or explicitly
leave its result unexplained. Either path remains mandatory before the
lane can close.
This commit is contained in:
Levi Neuwirth 2026-08-19 13:57:39 +02:00
parent e82bff71fe
commit 4fba9f6b44
No known key found for this signature in database
1 changed files with 7 additions and 5 deletions

View File

@ -519,11 +519,13 @@ Written now so the fix cannot quietly become "make the test pass".
confirmation on `main` is a follow-up, not a gate on the fix.
- **A3.** There is no established "R9 paradox" to explain — R9 ran
different Cargo compilations, so the comparison it appeared to make
was never made. What A3 requires instead: **D0 recreates the subset/full
comparison under captured provenance**, and whatever it then shows is
either explained by the fix or explicitly recorded as unexplained. A
fix that greens the sweep without that comparison having been made
properly leaves the gap stated, not hidden.
was never made. What A3 requires instead: **the demonstrated D1/D2
mechanism accounts for the subset/full difference, or D0b recreates
that comparison under captured provenance before this lane closes.**
In the first case, record the mechanism's explanation. In the second,
whatever D0b shows is either explained by the fix or explicitly
recorded as unexplained. A fix that greens the sweep without either
path leaves the gap stated, not hidden.
- **A4.** No deadline raised, no test skipped, retried, or serialised
to obtain green.
- **A5.** **Conditional on D4.** If bet 1 holds, this is unconditional: