vectors: write the cases — 49 sketches become vectors, and the trichotomy is enforced - #78
vectors: write the cases — 49 sketches become vectors, and the trichotomy is enforced#78dhh1128 wants to merge 11 commits into
Conversation
Forty-nine vectors, one per discriminating record the ratified edition and the rulings assign, with the input shape and the expected result stated at the grade the law can currently carry. Section 17's five families, the record's eight station-bearing rulings, supplement 2's six, and supplement 3's five, plus the ordering discriminators finding Nicholas-Keystate#15 names - including the empty-subcode collision that survived a full gauntlet round and the census gate because nobody wrote it. Every expected value is semantic-grade under R5 as clarified by supplement 1 C-1, since the carriage encoding has not ratified. The ledger pins every source it derives from by digest, and tools/verify_vectors.py checks that the pins still match the bytes, that every assigned station obligation carries at least one vector, that held vectors name their hold, and that no entry claims byte grade before the encoding round lands. The coverage check is the point: a ruling that assigns a discriminating record and never gets one is how the canonical-selection contradiction survived 4.1. Two vectors are held - the two-track equivalence pair on R19, and the rotation-covenant families on the recovery-seam ruling supplement 3 names as owed. The verifier runs in CI alongside the kernel and census checks. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
…supplement 4 The edition of record changed under the ledger. The edition-owed family moves from 4.1's section 17 to 4.2's section 18, whose boundary family R15 extended with designation and membership; every ruling-owed entry gains the ratified site where its ruled text now lives, or the fact that the ratified edition does not yet carry it. Eight entries are in that second state, all from supplement 3, and the README says so rather than letting a reader assume the corpus binds to 4.2 throughout. Eleven vectors are new. Section 19's gate three had no predecessor site at all, so its equivalence, must-reject and vanilla-passthrough families enter as a compact-form family. Supplement 4's two errata owe three station vectors: the cardinality-3 circuit was already here as V-R10-01, while the duplicity-pair and circuit-shaped payload pair are new, and the empty-subcode boundary needed a new entry rather than the one already present - V-R03-02 tests two tied defeats, and the erratum's boundary is the sole defeat with an empty subcode, which is where the two readings part company. Sources now pin both editions and all four supplements. 60 vectors, 13 families, 25 obligations covered, verifier green. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
# Conflicts: # .github/workflows/verify.yml
The ledger said corpus and meant register. An entry recorded that a vector was owed and sketched the shape of the case; it did not state the case. That gap is now visible rather than papered over: entries carry a concrete case where one has been written, the README says what an entry without one is, and the verifier's closing line reports both counts. A case is concrete at the semantic layer, which is the only layer that exists before the carriage encoding ratifies. The fixture convention fixes the symbols - a law head, a position, a bundle given as its spans, a clause whose class names the defeater class - so two implementers building one case build the same case, and the symbols become self-addressing identifiers when the encoding lands with nothing else about the case changing. Supplement 5 ruled the recovery seam whole and named itself the release condition for the families S3-9 held. Its nine arrive as cases: the seam family of seven, from an ordinary event with its seal through a bridge whose horizon closes unregrounded, and the delegated pair. The supplement stated them as input-to-expected-value pairs already, which is the form the rest of the ledger is being moved toward. Nine older entries gain cases too, chosen because they decide live findings or carry supplement 4's errata. Fifty-one remain sketches, and the ratchet is forward-only: new obligations from supplement 4 onward must arrive as cases, and the older ones are worth writing deliberately against the ruling that assigned them rather than in one guessing pass. Also resolves the verify.yml conflict with main, keeping the 4.2 census gate and replay steps alongside the ledger check. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
Ten cases drafted by the ratifying authority on PR Nicholas-Keystate#72, mapped into the ledger's schema rather than pasted: status to the ledger's enum, the not-carried fact to ratified_site where it belongs, and each situation converted from prose into a case with its given and its then, substance preserved. They discharge the vector debts of supplement 3's eighth and ninth composition items - conditional seating, the watcher-invocation law, identifier-as-office, governed vacancy - plus one from the keripy vintage #1544 repaired. Each carries contributed_by. The fixture convention gains their symbols: a governed domain, a custodial quorum, a chartered watcher, an unchartered courier, an exhibit-grade conviction package, a caretaker's enumerated powers. The id pattern widens to admit a sub-series letter rather than renaming ids already cited in review. Two holds corrected. The delegated transfer pair is not specifiable: it designs against the shape xfr is expected to take, which is roadmap-only at the pinned checkout, so it is held on the substrate - a different hold from the recovery-seam hold supplement 5 released. And R19 is unruled rather than held: it fell between the sittings, so no ruling waits on feasibility to be applied. The ledger had implied otherwise. Family stays as filed, across three families for the three office-succession cases: owed_by records the ruling, so a family that repeated it would stop being useful for finding anything. 79 vectors, 28 with cases, 51 sketches. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
Twenty-three sketches become cases, written against the ruling that assigned each. The record's seven: position-indexed succession across a revocation, the species-collision pair that finding Nicholas-Keystate#27 executed, the citing-clause list comparisons, contested standing as a typed pending, both pin kinds, competitors at one coordinate, and a refusal two verifiers reach from one triple. Supplement 2's sixteen: the compound refusal that preserves its computed components, the two remaining bearing branches, the three reversal-condition cases, the three membership cases including the eloquent stranger and the two-team pair whose expected value is the refusal itself, the covenant seal's three layers, both blinding cases, and the two semantics-pin cases. Where a ruling determines structure rather than a value, the case says so in its note rather than inventing one - V-R01-01 fixes the second finding's value by giving the requirement space no other unexamined check, and says that the value follows from R2 rather than from R1. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
…ketch gap Twenty-eight more sketches become cases. Supplement 3's nine: the scoped-claim divergence, the aggregate-membership pair and the three presentation forms, the unseated warrantor, the charter floor and the authentication grade, the two typed observation reports. The ratified section 18's ten: confluence under permuted arrival, six boundary must-rejects, the refusal-boundary pair drawn at the grammar grain, the recognition case that presumes nothing external, and the proper-subset membership rule. Section 19's seven, which had no predecessor site at all: the equivalence pair, four must-rejects including both directions of the digest-preimage confusion, route isolation, and the vanilla-passthrough vector at gate grade. Two entries carry no case and both say why. V-S39-01 is a marker recording that S3-9's held families were released. V-S17-02 is underdetermined: it cannot state which two expressions of one governance act are compared until R19 is ruled, and R19 is unruled rather than held. The verifier now enforces the trichotomy - a case, a stated underdetermination, or a marker - so an entry can no longer sit unwritten and unexplained, and it prints the open questions by name on every run. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
The ratified text's 'route isolation, below' resolves: compact-form bytes SHALL NOT ride in streams consumed by parties that never committed the regime, and are refused at the genus boundary because a foreign-genus segment is mechanically fatal rather than merely unlawful. The case now states that mechanism instead of paraphrasing the gate. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
Writing V-R03-01 needed a comparison basis for the species component and the ratified text does not commit one. Section 8.3 names the third component's basis explicitly and leaves the fourth's unstated; wall 6's default ranges over self-addressing identifiers and a species is an enumerated label, so the default does not reach it. Two readings survive - enumerated position, or the bytes of the name - and they order window-open against expired/abandoned differently. V-R03-01's existing pair does not discriminate: absent against window-open orders the same way under both readings, which was luck. The new entry carries the pair that does discriminate and stays unwritten under the trichotomy, naming the basis as what is open rather than guessing it. Signed-off-by: Daniel Hardman <daniel.hardman@gmail.com>
|
Substance-gate review, run at the bytes on the branch ( Two findings, both corpus-internal; the spec's enumeration was checked first and is not the ambiguous party. F-1 (mechanical): the outcome field carries two names. 29 cases write F-2 (substantive — the convention's first firing, against the corpus): two cases use an outcome word outside the ratified codomain. The codomain enumerates four cells (4.2 L176): affirmed / defeated-with-citation / pending / self-convicted. V-S39-W01 and V-S39-O01 write Both findings land against the cases, not the expectations — the discriminations are right; two words are wrong. With F-1 and F-2 repaired this is merge-ready from the substance side, and the supplement-6 families (six, released at S6-9 of |
|
Board-state ping (2026-08-27) — what's yours, what's ours, so neither side waits on a misread. Yours, and the only thing between this PR and merge: the two findings in the review above — F-1 (one key for the outcome role; Sequencing note that dissolves a blocker: #72 is still open, and this PR's body says merge-that-first. Since this branch carries #72's history and the substance-gate review ran at these combined bytes, we read merging #78 as landing both — #72 closes as contained when this lands. If you'd rather #72 merge separately first, say so and it's done; otherwise no action is owed there. Also yours, on your own proposal in #87 (adopted today, comment of record there): the discharge two-senses finding filed separately at MAJOR, and any term-retirement filings in the test's form (which test failed, at how many sites). No urgency; the test executes at 4.3 regardless. Ours, queued — so you know none of your filings are dangling: #85, #86, #90, and #83 are ruling-grade findings on the 4.3 docket's plate; rulings land at the sitting (the #88 locator seed is already adopted as an input of record on #77, with the review of record on that PR). #92 stays held on the clean-root decision by its own design. #82 closed today with the five determinations you asked for — the code is yours whenever you want it. And the moment this PR lands, the supplement-6 vector families (six, S6-9) file as the follow-on PR in this ledger's convention, so your merge unblocks our next. |
Writes the cases the ledger was missing. Builds on #72 — merge that first, or this can rebase.
No ratified bytes are altered, and nothing here touches
spec/. Changes are confined tovectors/and one tool.What changed
#72 established that a ledger entry recording that a vector is owed is not itself a vector. 51 entries were in that state. This writes 49 of them as cases, and the remaining two say why they are not.
Every case states its
givenand itsthenin the fixture convention — fixed symbols, named spans, an expected finding to the depth the case discriminates. No bytes, because the carriage encoding has not ratified; the symbols become self-addressing identifiers when it does and nothing else about a case changes.The two that carry no case
V-S39-01is a marker: it records that S3-9's held families were released by supplement 5 and points at the entries that state them.V-S17-02carriesunderdetermined. It cannot state which two expressions of one governance act are compared until R19 is ruled — and R19 is unruled rather than held, per the correction on #36.The trichotomy is now enforced
verify_vectors.pyfails the build unless every entry either states a case, names what its ruling leaves underdetermined, or is a marker. An entry can no longer sit unwritten and unexplained, and the open questions print by name on every run.Where a ruling determines structure rather than a value, the case says so rather than inventing the remainder —
V-R01-01fixes its second value by construction and records that the value follows from R2 rather than from R1.What the exercise surfaced
Forcing every field to a value is what exposes a field no ruling fixes. Two items came out of it and are held for review before filing rather than posted overnight; the stronger one is a missing comparison basis in the canonical order, of the same class as E4-2 and found the same way.
verify_vectors15/15,verify_kernel7/7, census-42 green, replay green.