Roel, Nicolás, all,

Your second question first, because it is a defect in what I proposed and
not an edge of it.

1. The zero-verdict run

You are right. Evidence completeness as I restated it in 0034 quantifies
over verdict records, and a run with no verdict records satisfies it by
having nothing to quantify over. An all-not-exercised run reads as
evidence-complete. A run with one pass and every other check excluded is
the same trick with the volume turned down.

The fix is your own rule from 0020 point 3, which I applied to the
aggregate and then failed to apply to my own claims: never emit the claim
without the denominator beside it. So each completeness claim publishes the
count of the population it quantifies over.

accounting completeness population: declared checks
execution completeness population: declared checks
evidence completeness population: verdict records

And a claim over an empty population is reported as not claimable, not as
satisfied. The zero-verdict run then has a name in the roll-up instead of a
silent pass, and the observations themselves are untouched, which is the
part I care about.

Note that execution completeness is vacuous in the same way at zero
declared checks. That is why I would rather state the rule once over
populations than patch evidence completeness alone. It also gives one
run-level rejection, which belongs in my section rather than in Nicolás's
table: a report asserting a completeness claim without the count of the
population it quantifies over.

2. Which evidence from 0013 qualifies

Your distinction cuts against my own wording, and the honest answer is that
most of 0013 does not qualify.

0013's method changes the checker: a rule's errors are dropped from the
validator's output and every vector is re-run. Both observations are real
and they come from two checkers. Under your condition, same checker,
constraints and domain, that is not a witness of the opposite verdict. It
is your Assay case in a different repository, and it establishes what your
Assay case establishes: the recorded verdict is attributable to the named
rule, so the control is not green for some other reason. Kenne's
rule-isolation point, in the message 0013 replies to, is the same claim. I
would call that attribution, keep it as its own thing, and keep it out of
discrimination.

What qualifies in 0013 is in the baseline, not in the mutation. The 89
vectors at f3295ca run under one pinned checker and contain both verdicts,
and at least one pair is related by a stated delta: Nicolás's Level A pair,
the same gap accepted with a lead's acceptance and rejected without it. Two
inputs, one delta, one checker, two verdicts, and that pair satisfies the
rows 8/9 implication. Guigui's accept and reject cases from 0006 are
candidates for the same shape, but I cannot tell from the thread whether
they are related by a stated delta or are an accept set beside a reject
set, and that is a question for Guigui rather than an assumption for me.

So the definition narrows, and it should:

discrimination demonstrated two observations from the same pinned checker,
under
the same constraints and domain, on two inputs related
by a stated delta, differing on the record's projection

Unrelated pass and fail records in one corpus must not qualify. If any pass
beside any fail counted, every mixed suite would be discrimination-complete
for free, which is the disease the field exists to prevent. The unit is the
delta-related pair, not the corpus.

3. exact-delta, and what it is not

It is the wrong home for this and I would not stretch it. exact-delta
answers one of your three questions, what changed. What is held fixed and
what is observed are different slots, and rows 8/9 have to read the second
and third, so they cannot live inside a free field describing the first.

changed which object varied: input | checker
fixed what is pinned: checker identity, constraint set, domain
projection what was compared: verdict, or verdict and fired-rule list
delta the concrete change, exact-delta, as the content of changed

The projection slot is not bookkeeping, and 0013 forces it. A vector flips
there when either the verdict or the fired-rule list changes. Three of the
64 MUST-FAIL vectors name two rules, because one violation trips two, and
relaxing R10 on those changes the fired-rule list while the test still
fails. Movement in the projection with the verdict fixed, already sitting
in the corpus. Without the slot, "flipped" cannot be read back and two
evidence objects asserting the same value assert different things. Your
Assay note that the handler decision and the test verdict are different
observations is the same requirement approached from the other side.

With those slots your scoping condition stops being prose. Rows 8/9 fire
only when changed = input and fixed includes the checker, the constraints
and the domain of the record. I would rather narrow the antecedent than
weaken the rows, which gives one more rejection: discrimination
demonstrated pointing at an evidence object whose changed object is the
checker. Attribution evidence in a discrimination cell.

4. Rows 10 and 11, and the order

Agreed, and the subcondition point is the sharper form of it. Each of those
rows bundles requirements, a record missing both references stays rejected
after one check is removed, and a vector that only demonstrates rejection
demonstrates nothing about which requirement is live. One vector per
requirement, accept controls retained, and the assertion on the rejection
reason rather than on the fact of rejection. That is Kenne's rule-isolation
applied to the rejection table, and Nicolás's test_vectors.py already works
this way, comparing the fired-rule list instead of pass or fail. A
rejection vector should name the row that rejected it.

Agreed on the order too, and your reason is better than the one I gave in
0034. I said the seventeen were premature because the row count would move.
The stronger reason is that 0013, your Assay case and Guigui's set are
three contrasts of different kinds, and a form that cannot classify all
three does not need vectors yet.

One citation I owed section 8 and missed. Guigui's reason for C01, in the
message 0013 forwards: fourteen MUST-FAIL vectors without it cannot
distinguish fail-closed from fail-shut. That is the saturated fail, named
on this list in early September as a defect worth a dedicated control, and
three suites carry the control already. The gap was never in the practice.
It was in the cell.

Evgenii Arsentev
ORCID 0000-0002-9120-7298
