Evgenii, all,

This is the handover you asked for: the record and slot
definitions as they stand, the consolidated rejection table with each
row's provenance, and the 42 evidence objects with what the shape could
not express. New thread so the archive holds it under its own subject.

I put the definitions first and the table second, which is the reverse
of the order you listed them, because the table reads the record and
restating the record inside it would give you two sources for one
thing.

The definitions exist across five messages sent between 1 and 16
September, and three of those rename or withdraw something an earlier
one established. Part 1 section 7 records every rename, so you can
check that nothing changed without being named.

And the three things I said the shape could not express are no longer
three. All three moved this week. One became a decision you recorded.
The other two are one question, the open item Kenne proposed. Part 3
is that material against today's state. The original list would give you
something the thread has already passed.


=====================================================================
PART 1. The record and its slots
=====================================================================

Every definition below is someone's and the attribution is named.

1.1 The per-check record

Four fields per check.

state pass | fail | not-exercised | inconclusive | void
cause required on the three non-verdict states, absent on
the two verdict states
other-verdict unknown | possible-not-demonstrated |
demonstrated(<ref>) |
foreclosed(<constraint set>, <domain>)
discrimination unknown | demonstrated(<evidence ref>)

The five states are Roel's. The state is what a consumer may conclude
and the only field an aggregate counts.

other-verdict is read against the record's own state: the other verdict
of a pass is a fail, of a fail is a pass. The two qualifiers are
Evgenii's, with his default: unknown on both, and no value assertable
without the artifact that carries it.

What each field answers:

state what may a consumer conclude
cause why is there no verdict
other-verdict could this check have produced the other verdict, and
on what constraint set and input domain
discrimination did this checker distinguish a changed input from the
original, and where is the run that shows it

The last two are separate fields for Roel's reason: evidence
establishing foreclosure and evidence demonstrating discrimination
establish different things.

1.2 The cause vocabulary

CAP-1's eight closed dispositions, with three changes this thread made:

- a value for void, because every CAP-1 disposition describes a unit
that was not examined or not disclosed, and void is a unit that was
examined and whose evidence does not hold up. Roel's gap.
- integrity-failure kept separate from availability-failure. A
signature that will not verify is a corruption signal; a key set
that cannot be fetched is an operations signal. Kenne's seam,
crediting Isaac.
- precondition-unsatisfiable, which no surveyed format has: the check
cannot run because the condition it tests cannot exist in any
artifact the emitter is allowed to produce.

Free text is refused in place of a disposition, for CAP-1's reason:
free text does not aggregate.

precondition-unsatisfiable is narrow and is not foreclosure:

not-exercised + precondition-unsatisfiable
the runner never invoked the check
pass + foreclosed(...)
the check ran on every artifact and could not have failed

1.3 The evidence object

Five slots.

changed input artifact | checker rule | constraint
fixed named, not implied: checker identity, constraint set,
domain
compared what was read on both sides
moved the subset of compared that differs
delta the concrete change

compared and moved are the split of a single earlier slot, projection.
The split is in 1.7.

moved is recomputed, not declared. It is recomputed over what the
referenced observations actually contain, and an object whose moved is
not contained in its declared compared set is rejected. Defining it
that way also makes a new inconsistency visible: moved holding
something compared does not, which is an emitter reporting a difference
in something it says it did not look at.

The domain is declared once at run level. foreclosed and the fixed slot
reference it by identifier and no slot restates it. That removed a
rejection row instead of adding one.

Arity is not a slot. A declared arity is forgeable the same way a
declared moved is, so arity is recomputed from the delta.

1.4 Carry or reference, and how a reader reads it

The format permits both and requires one. An object that stays with its
corpus can reference; an object that leaves it, handed to someone who
does not have the suite, has no resolvable reference and has to carry.

Form is decidable from the object alone, and is a rejection row (row 14
in part 2):

moved asserted on an evidence object that neither carries both
observations nor references them with digests

Reading a well formed object is a table, not a row, because
resolvability is a property of the reader and not of the object:

resolves, digests match moved and arity recompute, rows read them
resolves, digests differ integrity failure
does not resolve unchecked, the rows reading moved degrade

The middle state is separate for the reason the cause vocabulary
separates integrity from availability: an unresolvable reference needs
someone to supply an artifact, a mismatch needs someone to find out
which side moved.

A reader who cannot resolve the reference cannot recompute moved. The
digest only tells them whether what they did resolve is what the object
was written against, which is weaker than carrying.

One line is being added to this table by the editor, from the Merkle
case. Nicholas narrowed it after that message was written and the
narrowing matters: binding the count is necessary and is not a general
membership proof, and domain separation added while duplicate-last
padding is retained does not remove the ambiguity, since RFC 6962 also
uses a different tree shape. The text should not present either as the
fix on its own.

1.5 The per-slot sort

A slot is one of four kinds:

declared written by the emitter
recomputed derived by re-running a pinned checker
resolved fetched through a reference and checked
recomputed, opaque re-runnable, not machine comparable

The fourth came out of the emission in part 3.

1.6 The two classes of row

Consistency rows read declared slots against each other and catch a
contradiction. Evidence rows read a declared slot against a recomputed
or resolved one and catch a falsehood. Form rows are decidable from the
object alone. The per-slot sort governs the evidence class only.

Which row is which is in part 2, and five of them are unclassified.

1.7 What was renamed or withdrawn, so the diff is readable

constructibility became other-verdict, and became symmetric. The
earlier field applied to pass alone and could not report a gate that
rejects everything, which my own outline listed as the case the
design could not express. The symmetric field names the verdict the
record did not produce, which makes "a fail is its own demonstration"
true by construction.

constructible-not-demonstrated became possible-not-demonstrated.

Four verdict causes were withdrawn with their column. An earlier
message required cause on all five states with a second disjoint
vocabulary: counterexample-in-suite, counterexample-absent,
counterexample-impossible, not-established. The qualifier field
replaced them and the column went back to the three non-verdict
states.

projection became compared and moved. The single slot was defined as
what was compared, and a row then read it as what moved. In all 42
one-field pairs the verdict and the fired-rule list move together, so
the row as written excluded every real pair including the one named
as qualifying. Splitting the slot lets the row read a field instead
of an agreement.

Declared arity was proposed and dropped, for the reason above.

One rejection row was removed rather than added: foreclosed over a
domain that is not the run's domain became unwritable once the domain
is a declared object referenced by identifier.


=====================================================================
PART 2. The rejection table
=====================================================================

This is the table I published on 15 September with the changes since
applied. Rows 1 to 12 keep their numbers, because the thread has been
citing them and renumbering would cost more than it is worth. Two rows
that were open and lettered are resolved and proposed as 13 and 14.
Nobody has numbered them yet, so that part is a proposal and not a
record of agreement.

1 a non-verdict state with no cause 0020, unchanged
2 void with not_applicable, out_of_scope or withheld 0025, unchanged
3 not-exercised with integrity-failure 0025, unchanged
4 a confinement control that failed while the check
ran, with any state but void 0020, unchanged
5 a declared exclusion with any state but
not-exercised 0020, unchanged
6 a non-verdict state carrying either qualifier narrowed in 0038
7 a verdict state carrying a cause widened in 0038
8 other-verdict foreclosed with discrimination
demonstrated now on both verdict states
9 discrimination demonstrated with other-verdict
unknown or possible-not-demonstrated 0033, reworded
10 foreclosed without a constraint set and a domain
now on both verdict states
11 an asserted value without its evidence reference,
on either field, foreclosed included extended, 0038
12 discrimination demonstrated citing an evidence
object whose changed slot is the checker new, 0036

Proposed numbering for the two that were open:

13 other-verdict demonstrated citing an evidence object whose moved
does not contain the verdict was A, now resolved
14 moved asserted on an evidence object that neither carries both
observations nor references them with digests was C, now resolved

2.1 Row classes

consistency 1, 2, 3, 5, 6, 7, 8, 9
form 14
not classified 4, 10, 11, 12, 13

I am not classifying the five. Rows 12 and 13 read a slot of a
referenced object and are probably evidence rows, and rows 10 and 11
are presence checks over declared values and are probably consistency
rows, but probably is not a classification. These five are unfinished.

2.2 What changed since the 15 September consolidation

Row A is resolved and is proposed as row 13. A was "other-verdict
demonstrated citing an evidence object whose projection is not the
verdict". It was contested because projection was defined as what was
compared and the row read it as what moved, so read literally it
excluded every real pair in my corpus, including the one named as
qualifying. Splitting projection into compared and moved and having the
row read moved fixes it. Sankalp proposed the same split today and you
have said you will write it that way, so A is settled.

Row C is resolved and is proposed as row 14. C originally said
"resolvably references", which made the rejection depend on whether the
reader had the repository. Resolvability is a property of the reader,
not of the object, so C repeated the defect it was written to catch.
Removing "resolvably" makes it decidable from the object alone, and the
reading of a well formed object is the table in 1.4 rather than a row.

Rows 8 and 9 were mislabelled by me and Kenne corrected it. I had
attributed the contested reading to rows 8 and 9; the contested one was
A. Rows 8 and 9 read two declared qualifiers against each other and
survive on that ground, which is what puts them in the consistency
class.

The two classes of row are new since the consolidation and are not an
amendment to any row. They are a property of the table that the
per-slot sort made visible, and rows 1 to 12 survive the split
unchanged.

2.3 Still open

B whether a stated delta is bounded to one field

At one field, MUST-FAIL pairs with different fired-rule lists number 0
in my corpus at 1e36257. At two fields they number 132. Sankalp reports
252 reject vectors at agent-evidence-vectors v0.11.1 naming exactly one
condition, and in Guigui's corpus at 6b10485 the count of one-field
pairs is 0 across all 66 pairs under three scopes.

One asymmetry that should be on the record. The 42 one-field pairs
are reproducible, by tools/emitir-42.py in the disensor repository. The
0 and the 132 come from a second script that measures pairs without
running the checker, and that one is not published, so those two
figures are still my assertion. I would rather the text say so than
carry them as if they had the same standing.

The measurements do not contradict each other. One field turns out to
be a property of how a corpus was built rather than something the
format can assume. Row 9 guards an empty set or a large one
depending on the answer.

2.4 What is not a change to this table, so it is not filed here twice

The roll-up rule that inconclusive and void cannot improve an aggregate
is Roel's and belongs to the roll-up, not to the rejection rows.

The two decisions you recorded, that the recompute-opaque slot is a
fourth kind no row reads, and that a digest over the error list was
considered and declined, are properties of the per-slot sort. The first
bears on this table only in the sense that no row reads that slot kind.

The count binding line from the Merkle case belongs to the reading
table in 1.4, not to a rejection row.


=====================================================================
PART 3. The 42 evidence objects, and what the shape could not express
=====================================================================

Emission: commit 1e36257, 42 pairs, v0.2 4, v0.3 16, v0.4 22. The
emitter runs the pinned checker over every vector and uses its output
as the observation. It is a script, not hand assembly.

The script is now public, so anyone can repeat the counts:

git clone
https://www.google.com/url?q=https://github.com/NicolasRocchia/disensor&source=gmail&ust=1789829664851000&sa=E
cd disensor && pip install -e .
python tools/emitir-42.py

It refuses to present a number as clean when the working tree carries
modified tracked content, and it prints the commit and the jsonschema
version it ran under.

The emission is stable across the sixteen commits between 1e36257 and
3950067: same 42 pairs with the same suite split, same 0 carried
against 84 referenced, same 42 moving something beyond the verdict and
rule labels, same 69 errors serialised as strings, same 0 vectors
disagreeing with their declared expectation, and the 42 objects and the
list of what could not be expressed come out identical byte for byte
once line endings and the embedded commit are normalised.

3.1 The shape has no name for the observation

Status: still unexpressed. This is the substance of the open item.

The checker returns a list of errors. The verdict is whether that list
is empty, and the rule labels are derived from it. Two projections of
one primitive.

The vocabulary for what was compared enumerates verdict, and verdict
with rule list. Both are projections. There is no value for the list
itself, which is what the checker actually produced. All 42 objects
report moving something other than verdict and rule labels, and all 42
move the same three together: the primitive and its two projections.

In v0.1 terms this is the output side of who declares what is counted:
an emitter can name only projections of its observation, so what the
record composes is settled by the emitter and not by the format.

3.2 Recomputable but opaque

Status: a decision, not a gap. The residue is what the decision costs.

All 69 errors in the corpus serialise as strings, with no structure.
The primitive can be recomputed by re-running the checker and still
cannot be read by a rejection row. You can establish that the message
changed, not what about it changed. That 69 is reproducible: the
emitter prints the serialisation path it took for every error it saw.

You have recorded this as a fourth kind of slot that no row reads, and
recorded that a digest over the error list was considered and declined
because it gives equality and nothing else. Both are right.

What it costs. The observation primitive is carried and recomputable,
and no row in the table reads it. Every row that fires on these 42
objects fires on a projection.

3.3 Whether a stated delta is bounded to one field

Status: open, with measurements on both sides that disagree. The
disagreement is the finding, which Kenne conceded and I concede.

Against Guigui's corpus at 6b10485 I counted one-field pairs under
three scopes. C01 against S01 differs in 3 fields inside tool_call, 14
over the whole file, and 0 with identity fields stripped. Across all 66
pairs, under all three scopes, the count of one-field pairs is zero.
And the repair that looks obvious, ignoring identity metadata, erases
the test case: S01's own README describes it as an envelope missing the
required field tool_call_id. Sankalp's 252 sit on the other side.

They are two corpora built for different purposes and neither is wrong.
One field is a property of how a corpus was constructed, not one the
format can assume. My own earlier claim that three corpora shared one
construction does not survive the measurement and I withdraw it.

3.4 What I would ask the text to do with these

3.1 and 3.3 are the same open item, one from the output side and one
from the input side, so publish them as one. Publish 3.2 as a decision
with its cost stated.

Three things this handover does not settle: what composes the
observation record, what counts as one field, and the classification of
rows 4, 10, 11, 12 and 13.

Nicolás
