--protocol-check's A-7 gate fires only when required equals achieved on every factor:
✓ required differs from achieved somewhere 1 of 12 differ
One divergent row satisfies it, and the other eleven are never examined. So a sheet where eleven required levels were defaulted by the extractor and confirmed in a single sweep passes this gate, provided one row happens to differ.
This is not hypothetical — the shipped Nagaraja encoding has such a row
packs/vv40/examples/nagaraja/cou1 carries Test conditions at required 3 / achieved 1. Any workbook derived from that case has a divergent row by construction, which makes the clause unsatisfiable and the check permanently green regardless of what happened to the other twelve factors.
The Johnson pilot has the same shape (the recovered exceedance row at 3/1). Both of the project's worked examples defeat the check.
Why the all-or-nothing form is the wrong shape
A-7's own words are per-factor:
These are two different claims and they live in two different places in a source document. Confirm each against its own location.
The uniform-defaulting case the current check detects is real but is the easy case. The consequential one is partial defaulting, which is what an extractor actually produces, and which the current form cannot see.
Suggested per-row form
A factor owes work when either:
- its required level is still
defaulted — an extractor-supplied level is not a level the source stated; or
- required and achieved carry the same anchor — one passage offered as the source of two different claims, which is the citation form of copying one into the other.
A recorded waiver still clears it, as today.
Clause 2 is worth having on its own: it is mechanically checkable from the anchor column that A-5 already requires, and it catches the sweep that clause 1 alone would miss once an encoder anchors a defaulted level to whatever passage was nearest.
Context
Found while building Credenza against the published wheel. Credenza now implements the per-row form on its side (act-level refusal for the unanchored confirm, gate-level for the same-location rule), so it is not blocked — but the CLI check is the authority at A-11, and the two should agree.
Related: #93, #96. Same family — a gate that is correct on the ordinary case and vacuous on the important one.
Found against v0.12.0.
--protocol-check's A-7 gate fires only when required equals achieved on every factor:One divergent row satisfies it, and the other eleven are never examined. So a sheet where eleven required levels were defaulted by the extractor and confirmed in a single sweep passes this gate, provided one row happens to differ.
This is not hypothetical — the shipped Nagaraja encoding has such a row
packs/vv40/examples/nagaraja/cou1carriesTest conditionsat required 3 / achieved 1. Any workbook derived from that case has a divergent row by construction, which makes the clause unsatisfiable and the check permanently green regardless of what happened to the other twelve factors.The Johnson pilot has the same shape (the recovered exceedance row at 3/1). Both of the project's worked examples defeat the check.
Why the all-or-nothing form is the wrong shape
A-7's own words are per-factor:
The uniform-defaulting case the current check detects is real but is the easy case. The consequential one is partial defaulting, which is what an extractor actually produces, and which the current form cannot see.
Suggested per-row form
A factor owes work when either:
defaulted— an extractor-supplied level is not a level the source stated; orA recorded waiver still clears it, as today.
Clause 2 is worth having on its own: it is mechanically checkable from the anchor column that A-5 already requires, and it catches the sweep that clause 1 alone would miss once an encoder anchors a defaulted level to whatever passage was nearest.
Context
Found while building Credenza against the published wheel. Credenza now implements the per-row form on its side (act-level refusal for the unanchored confirm, gate-level for the same-location rule), so it is not blocked — but the CLI check is the authority at A-11, and the two should agree.
Related: #93, #96. Same family — a gate that is correct on the ordinary case and vacuous on the important one.
Found against
v0.12.0.