Repository navigation
Complete the floor's per-identity terminal evidence in the seed, and derive passed from it - #8896
Conversation
…ntity join THE OBLIGATION, WHICH IS WHY THIS EXISTS -- not the size of anything. The v2 self-host program claims candidate-bound witnesses executed and matched their expectations. The seed is the only producer that simultaneously holds a witness identity and its terminal Pass, and it destroys the identity at accumulation: `ClaimOutcome::Pass => outcome.passed += 1`. So a run reporting `passed=10132` cannot say WHICH. The v2 obligation is not realizable without a seam there. This commit is the v2 half: the schema and the completeness law. It touches no seed and no Rust. A PASS LIST IS THE WRONG ARTIFACT AND THIS IS DELIBERATELY NOT ONE. A roster of passing identities reproduces one layer up the ambiguity it was built to remove: an identity ABSENT from a pass list is failed, interrupted, unrouted, never executed, or lost to truncation -- five states behind one silence. The ledger carries ONE ROW PER PLANNED IDENTITY and every row is terminal, so absence is not a value it can express. `Pass` IS A PROJECTION, NOT A STORED FIELD. There is no `passed: Bool` in the row, so a row cannot disagree with its own disposition -- the disagreement has no constructor. `claim_disposition` derives from (expectation x observation) over the Returned / DiagnosedStop / Interrupted grain, and `Interrupted` carries the existing `ClaimSafetyOutcome` rather than a second spelling of it. An attempt that RETURNED may still have observed nothing, so `ClaimObservation` separates `ObservedVerdict` from `ObservationUnrepresentable`. Collapsing the second into `holds: False` would report a failing witness where the truth is a witness whose answer was never in a readable shape. COMPLETENESS IS AN IDENTITY JOIN, AND HERE IS THE CASE THAT FORCES IT. One planned identity never reaches the ledger; another is written twice. Row count equals planned count. Every aggregate in the run summary is IDENTICAL to a correct run. A count-based check is green and the missing witness -- possibly the one just added -- reports as covered. `LedgerReconciliation` is therefore a RECORD of three independently-joined sets, not a coproduct: a coproduct would report the first defect and hide the second, and this failure mode is exactly the one where two defects appear together and cancel. Measured, same test, two trees: identity join returned `true` count comparison the swap satisfies (control) returned `false` GREEN ADMISSION IS A TYPED OUTCOME, NOT A Bool. `LedgerGreenAdmission` has four arms -- EvidenceComplete, EvidenceUnfinalized, EvidenceReconciliationFailed, EvidenceFooterCountDisagrees -- because a Bool cannot say WHY evidence was refused and the three refusals have three different remedies. THE FIRST DRAFT RETURNED A Bool AND IT MADE A PARTIAL LEDGER READ GREEN. The arm was `LedgerPartial => bool_boolean_algebra.bottom`, which typechecked, ran, and answered the opposite of what it says -- the exact "instrumentation optional precisely when it fails" arm this schema exists to forbid. It was caught by a test written to fail in both directions, not by review. The substrate defect underneath it (v2 has two non-interoperating representations of Bool) is filed separately against v2.std.logic and is NOT fixed here: it is std's, and bundling a substrate repair into a self-host evidence vertical makes both harder to review. The footer count is checked against the PLANNED population, never against the rows the reader parsed -- a truncation that dropped rows and rewrote the footer to match would agree with itself. Five tests, all green, each with the discriminating arm named in its own carrier. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ete the field nothing read
Four review findings, all correct, all measured rather than argued.
1. THERE WAS NO CANDIDATE BINDING, and this module's own header claimed
CANDIDATE-BOUND witnesses. There was no `Ledger` type at all -- only rows,
reconciliation and publication -- so a ledger from run A was structurally
indistinguishable from evidence for run B, and the obligation's completed claim
("identity W appears exactly once in candidate C's terminal population") had no C
to name. That is the difference between a ledger and evidence.
`TerminalLedger { binding, rows, publication }` with `LedgerBinding
{ repository_snapshot, prepared_subject, roster_identity }`. The binding is a
FIELD, not a sibling artifact, so an unbound ledger is unrepresentable rather
than merely unusual, and `ledger_green_admission` now takes the ledger.
2. `DiagnosedStop { reason: Symbol }` COLLAPSED ARMS THE SEED ALREADY HOLDS
TYPED, and the seed's own comment argues against it: "A collapsed `failed` would
make a budget refusal, a runtime error and a witness that answered false read
alike, and those three have different remedies." A Symbol reason is a RENDERING
of the terminal fact, not the fact -- and the boundary is "v1 preserves the raw
terminal fact it already holds". Stringing it during transport would make the
ledger strictly less informative than its producer, which inverts the obligation.
Now RuntimeErrored { message } | BudgetRefused { safety } | HostToolUnresolved
{ name, probed } | RouteGap { route }, mirroring ClaimOutcome one for one.
3. `digest: String` was a hollow carrier -- it admits any text and cannot be
compared against anything else in the corpus that hashes. Now
`std.content_hash` `Fnv1a64Structural`, the structural family member DESIGN
names.
4. `ordinal: Int` WAS CARRIED AND NEVER READ, while this comment claimed it made
a missing row visible as a gap. Nothing in the schema touched it. That is
rung inflation at carrier grain: the guarantee existed only in the prose.
The repair is not a contiguity check -- it is DELETING THE FIELD. Position in a
list is dense and unique by construction, so a duplicated or gapped ordinal has
no spelling rather than being caught by a validator. Truncation is still caught,
by the footer count against the planned population, which is implemented and
tested.
A stale import of the renamed variant was caught by the resolver, not by me.
Five tests, all green after the rework.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lapsing what the row un-collapsed A. `Symbol` WAS USED THREE TIMES WITH NO IMPORT LINE. It typechecked and every test passed because v2 resolves bare symbols against the whole pool, so the module carried a real dependency that no import recorded -- the exact class of invisible edge the census lane measures, authored fresh in a module whose purpose is making evidence inspectable. The gap was mine: a `sed` removing the line when `DiagnosedStop` was replaced. Worth recording because it shaped my confidence: the resolver DID catch a stale import of a renamed variant one commit ago, so I read it as covering imports. It covers WRONG imports, not MISSING ones. A passing test suite established nothing here. B. THE DISPOSITION RE-COLLAPSED THE ARMS THE ROW HAD JUST SEPARATED. Four terminal shapes -- RuntimeErrored, HostToolUnresolved, RouteGap and ObservationUnrepresentable -- all projected onto one `RefusedBeforeVerdict`, one step after the row was un-collapsed for precisely the reason that a budget refusal, a runtime error and a witness answering false have different remedies. It is not cosmetic. The floor reports these as SEPARATE COUNTERS today -- `host_tool_unresolved`, `route_gap_unenrolled`, `route_gap_held`, `stale_route_gap`, `interrupted_before_verdict` -- and the obligation requires the counters to be DERIVED from finalized rows so a counter disagreeing with the ledger has no constructor. A projection that has already merged two counters can derive neither, so they would have had to be computed independently: the dual authority the derivation exists to dissolve, reintroduced by the projection meant to replace it. `ClaimDisposition` now has one arm per terminal shape -- BudgetRefused, HostToolUnresolved, RouteGap, RuntimeErrored and ObservationUnreadable, each `BeforeVerdict` -- so every counter the floor reports stays derivable. Losslessness was chosen over a declared coarseness because coarse-but-declared would still have forced the counters to a second authority. Five tests green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…derive `passed` from it The v2 self-host program declares a per-identity completed-evidence obligation over the required floor. This process is the only producer that holds a witness identity and its terminal outcome at the same moment, and it destroys the pairing at accumulation -- `ClaimOutcome::Pass => outcome.passed += 1` keeps the count and drops the name -- so the obligation is not realizable without a bridge here. Collection and consumer land together. Every planned identity mints exactly one `ClaimTerminalRow` before the branching, `reconcile_terminal_ledger` joins that population against the planned one by identity, and a mismatch is a typed `TerminalLedgerIncomplete` refusal naming the three sets. `passed` is then derived from the rows and the old increment is DELETED, not kept beside it: two authorities over one fact is what this removes. Completeness is an identity join, not a count equality. A ledger that omits one identity and duplicates another has the same row count, the same `passed`, and the same planned/executed/receipted triple as a healthy run -- the preceding `ClaimIdentityCountsDisagree` check is green over it. The discriminating RED is `a_duplicate_replacing_an_omission_is_caught_while_every_count_stays_equal`, which asserts the counts equal before asserting the join refuses; replacing the join with `planned.len() == rows.len()` turns it and its sibling red, measured. The seed stays narrow: it preserves raw terminal facts it already holds. No candidate digest, no expectation join, no artifact verification, no general evidence API. The binding -- which candidate this evidence is for -- is v2's to compute and mean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…r, and close the test's missing import Two carrier findings from review, and one from the automated pass. DISSOLUTION CONDITION. The ruling admitted this bridge on conditions and one of them had no representation in the diff: nothing named what retires the seam. It is named now, on both carriers, and it is ONE event for both findings -- the self-emitted v2 claim executor. Once v2 drives the floor's execution, the producer holding identity-and-outcome together IS v2, so `ClaimTerminalRow`, `claim_disposition`, `reconcile_terminal_ledger` and the refusal are deleted whole. THE MIRROR IS A SECOND AUTHORITY AND NOTHING CHECKS IT. `cli_run.rs` is HAND_MAINTAINED, so the Rust types are authored beside the `.dag` schema, not derived from it. Regen does not compare them -- the file is not generated. The witnesses do not compare them -- each side is exercised alone. So the two share only names, which is exactly the seam this change repaired one grain down when it extracted `reconcile_terminal_ledger` so its test could not be a control sharing only a name with its subject. That rule condemns this seam too; here it is declared debt at *mitigatable* with a named terminal rather than silently repaired. No lens is built: the cheapest honest check reads the seed's emitted ledger, which cannot exist before serialization does. Also corrected: both headers claimed the seed SERIALIZES the ledger. It does not yet -- the rows are consumed in-process by the reconciliation refusal and the `passed` derivation, and binding, footer and atomic publish land with the artifact. MISSING IMPORT. `LedgerPublication` was used as a parameter type and never imported; whole-pool resolution accepted it and every test passed. Imported now. The same sweep found `BudgetRefused` / `BudgetRefusedBeforeVerdict` imported and unexercised, so the arm gets the test it was missing rather than losing the import: a budget refusal is a pre-verdict disposition, not a failure, and collapsing the two would leave `budget_refused` underivable from the rows. Calibrated -- mutating that arm to `Failed` turns the new test red and leaves its sibling green, which is why the arm needed its own test. 6/6 PASS on the .dag roster; 3 passed on the Rust law. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Both findings taken, plus the automated pass's import nit. Pushed as Dissolution condition — was absent, now named on both carriers. One event retires the seam and the mirror together: the self-emitted v2 claim executor. Once v2 drives the floor's execution, the producer holding identity-and-outcome together is v2, so The mirror is a second authority and nothing checks it — declared rather than silent. Both headers were also inaccurate and are corrected: they said the seed serializes the ledger. It does not yet — the rows are consumed in-process by the reconciliation refusal and the Missing import (review 54697) — confirmed and fixed. Calibrated, not asserted: mutating Verification on this head: 6/6 PASS counted against the roster of 6 on the — sent from fierce-lynx-647 |
…nsus, and it refused #8896 landed src/v2/workflow/floor_terminal_ledger.dag on main while this branch was open. It imports WitnessIdentity and witness_identity_qualified_name from v2.workflow.floor2_prepared_subject by name, and its test does the same. This branch deletes that module. THE TWO BRANCHES TOUCH DISJOINT FILES, SO GIT MERGED THEM CLEAN. No textual conflict, no marker, no driver refusal -- and the merged tree does not compile. A three-way textual merge answers "did the same bytes change twice"; the question that decides this case is "does the merged tree still resolve", which is not a question about bytes. A merge preserves bytes, not measurements: every count in the disposition record is a statement about a tree, and the merge produced a tree none of them were measured against. The measurement was not wrong. The module was STILL-UNCONSUMED at base 90986d1 on every decoded surface and still is at that commit; it acquired a consumer afterwards. This is the census's second blind spot and it is not fixable by improving the instrument: a static census reads a tree, and the part that had not been written yet is as invisible as the part it decoded wrongly. Found by re-scoring the deleted set against the MERGED tree rather than against main -- a deliberately over-generous token match that flagged nine, of which eight were prose, annotation, or substring collisions (`Binding` inside CapabilityBinding prose, `YamlBool` whose live declarer is a coproduct VARIANT -- defect 7's own shape, in the triage regex this time -- `grade` and `readme` in citation text) and one was real. §4l's rule was followed rather than the count adjusted: the restore's imports were checked for in-population consumers, the fixed point closed at one restore, no cascade followed. 56 deleted becomes 55. The near-miss ledger reads 2, both found by execution and neither by the census: gunbc.pr_digests and this one. §4m records it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-first, batched, refusals reported as the census (#8862) * B1 — the RESIDUE-EMPTY control batch: 6 modules with no content to strand The census's control batch, run first for the reason it was chosen as one: a module that declares no symbol cannot be bare-referenced, so RESIDUE-EMPTY scored 0-of-8 consumed on the defect-6 re-score and is the batch that proves the deletion mechanics without risking working code. Every file here is a module line plus at most an import or a single unread String; none declares a symbol, none is named by any .dag, .rs, .yml or .toml in the tree. v2.bin.main's main_rs_trampoline_authority is the one row carrying content, and it is dead data in DESIGN 4c's sense: the only other occurrence of that text in the tree is a parse specimen in gap4_parse_tokens_remain_test.dag, which embeds the literal as a fixture rather than referencing this module. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * B2 — 66 modules unreachable from every root and named bare by nothing The remainder of the residue that carries no obligation to anything outside itself: not reachable from any discovery path, entry row or v1 seed mirror; no uniquely-owned symbol named bare by any .dag file in the corpus; and no mention in any .dag, .rs, .yml, .yaml, .toml or .sh source. Their only occurrences tree-wide are in .md prose, repaired in the next commit. None of the 66 declares a test fn, so no assertion stops executing with them, and none has a src/v1/stage0/src mirror, so the seed population is unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore gunbc.scm.commit_closure_store: the census deferred it by name, and it is not residue The census's finding on this row is that it is a replacement-migration leftover, not residue: gunbc.scm.repository_envelope took its grain one day later and left the Filesystem save/load half unattached. Which way that resolves -- the envelope grows save/load, or this module is the persistence layer the envelope should consume -- turns on the #8820 author's intent, and the census explicitly declined to disposition it for that reason. Sweeping it here on an unreachability score would answer that question by deletion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the two doc citations the deletion would have stranded Both rows describe a deleted module as a live subject: model-grounding-lens-extract names gunbc.tools.grounding_confirm as the CONFIRM judge, and review-surface-subject-map weighs gunbc.pr_digests.MergeReadinessVerdict as a second required aggregate. The analysis in each stands; only its premise about what exists in the tree does not, so the row is marked rather than rewritten. Three further mentions are deliberately left untouched. floor-cut-replacement-plan names dag/gunbc/floor_resolve_realization.dag on a 'delete as reachability confirms' list, so this deletion DISCHARGES that row rather than stranding it. Two receipts embed the literal git-status line 'A src/v2/workflow/host_discovered_owned_data_manifest.dag' inside a transcript; editing a transcript to match a later tree would falsify the receipt. algebra-grounding-unification-design names std.list as a road not taken, not as an authority it cites -- and the stub's deletion corroborates it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the disposition: 71 deleted, 68 held with a typed reason each The census answers what is unconsumed; this records what was done to it. Every held row carries the reason it survived, because a refusal is the deliverable here as much as a deletion is. Three results worth the document rather than the commit message. The instrument was re-derived rather than inherited, and it reproduces the census within four days of drift (131 residue -> 139), which is what makes the deletion auditable against the tree it ran on rather than against a row list. Re-scoring AFTER the cut is the discriminating evidence: reachable and CONSUMED-DECISIVE are both unchanged, so nothing with a live caller moved, while population fell by exactly the file count. And seven modules moved from DEAD-CONSUMER-ONLY to STILL-UNCONSUMED as their island neighbours went -- the census predicted the mechanic and this measures it, so the residue list is a fixed point reached by iteration, not a set reached in one pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Point the census at its execution record One line, at the top, because the two documents answer different questions and a reader who finds the census must not conclude the population is untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keep the instrument beside the census, drop the working blobs The script is what makes the numbers checkable; the JSON it emitted is derived data with no consumer, so it is ignored rather than committed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Specify the instrument in prose: the repository excludes *.py, so the method ships instead Committing the script was the first attempt and .gitignore refused it tree-wide. Rather than route around that, the method is written out to the grain a reader can re-implement, and the section-2 counters are noted as checkable without it at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The deletion's one real strand: two pinned exclude lists named a file that no longer exists Found by widening the mention scan past the source extensions to .txt/.json, which is where it was hiding: docs/probes/census_extra_excludes.txt and its seeds file both listed dag/examples/gunbhub_serve_program/gunbhub_serve_program.dag, and census_exclude_derive.rs loads both -- the seeds drive the derived closure and the oracle is its drift witness, so a row naming a deleted path skews the symmetric diff between them in the direction that reads as drift rather than as staleness. The row is removed from both rather than the file being restored: the exclusion existed to keep a module out of a resolve walk, and a module that is gone needs no exclusion. The two count literals that pin those files (83 -> 82, 27 -> 26) move with them; they are not oracles in DESIGN 5's sense either before or after, and this change does not make them one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the .txt strand in the disposition, and what it says about the precondition A source-extension mention scan is not a complete consumption surface. The finding is small -- one row in two pinned lists -- but the lesson is the reusable part, so it goes in the document rather than only in the commit that fixed it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record what the manifest deletion actually removed, and why its exclusion rows stay Review cleared two surviving references to a deleted filename as harmless string patterns, which is right. Checking why turned up two things worth the row. The deleted module was a committed instance of an artifact the generator that produces it stamps DO NOT COMMIT -- a second module path holding an all-zero copy -- so the deletion has a better justification than unreachability. And the exclusion rows are LIVE, not dead: path_excluded is a substring match over the full path, so the pattern still matches the ephemeral file the generator writes. Tidying them away, which 'a pattern matching nothing' invites, would re-admit a generated transport into discovery. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore gunbc.pr_digests and the deficit filing: one instrument defect, one KEEP disposition TWO RESTORES, DIFFERENT CAUSES, AND ONLY THE FIRST IS A DEFECT IN THE MEASUREMENT. gunbc.pr_digests is instrument defect 7, and the floor found it: "unresolved type MergeReadinessVerdict" plus eight "undefined variable Ready" in gunbc.code_change_workflow and its witness. The re-score's declared-symbol extraction read fn/data/type/const declarations and NOT COPRODUCT VARIANT CONSTRUCTORS, so the variants of type MergeReadinessVerdict = Ready | NotReady {...} contributed no owned symbols. code_change_workflow names Ready bare with no import -- exactly the whole-pool resolution the re-score exists to see -- and the instrument was blind to the constructor half of it. Counting variants moves CONSUMED-DECISIVE from 89 to 94 at this branch's base and reclassifies pr_digests as consumed. Same class as the census's own defect 6, one level down: a surface decoded for declarations and not for their variants. gunbc.generic_binder_field_projection_deficit is NOT a measurement error -- it scores STILL-UNCONSUMED correctly. It is dispositioned KEEP-WITH-REASON in #8851 as a DESIGN 4b deficit filing: declared rung, ceiling, next-rung trigger. An unconsumed deficit row is 4b(2) working as specified, since a class below its ceiling is REQUIRED to name its trigger and nothing consumes that filing by design. Deleting it would have removed a safety-ledger row and lowered a rung with none of the declaration 4b(3) demands. Unreachability is simply the wrong predicate for this class of row, and the census said so before I ran. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record instrument defect 7 and the deficit-filing restore in the disposition The floor's refusal is the section that matters: the two counters I offered as discriminating evidence were computed by the instrument that had the defect, so they could not see the case they were blind to. A control derived from the measurement it controls does not discriminate that measurement's blind spot. The floor did. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File defect 7 in the census, and the count-literal finding beside the v1 edit Defect 7 goes in the census document rather than only here, because it is a defect in that document's METHOD -- an extractor that reads fn/data/type/const and not variant constructors cannot answer the bare-symbol question defect 6 poses. Its scope is stated precisely: measured in this lane's re-implementation, unmeasured in the census's own, so the 91 and 96 are to be checked rather than assumed either way. The lesson is carried verbatim, because it generalizes past this row: a control derived from the measurement it controls does not discriminate that measurement's blind spot. Both counters this lane offered as safety evidence came from the instrument carrying the defect, and they read as reassurance precisely because they were consistent. The count literals moved for the pin are filed as a change detector with a receipt -- one row moved for an unrelated reason and both literals had to be hand-followed -- and deliberately not fixed, since the pin has its own lane and its own declared dissolution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore 13 more: the corrected extractor moves them to AMBIGUOUS, and the src/v1 edit dissolves with them silent-deer-368 sent four discriminating cases for the declared-symbol extractor. Mine passed three and FAILED the fourth: a same-line coproduct, type X = A | B, where the variants sit on the type line itself and a start-of-line variant scan never sees them. That is a fourth under-extraction bug in the same family as defect 7, and under-extraction creates FALSE UNIQUENESS, which is the delete-a-live-module direction rather than the keep-a-dead-one direction. Adopted their region-based extractor, which fixes all four at the root instead of patching a regex per bug: a type's region runs to the next TOP-LEVEL declaration (so a multi-line variant record cannot truncate it), a leading generic <...> is stripped before testing for =, and operation/service/resource are counted as declarations in the flat service namespace. All four discriminators now pass, and the (c) tell passes too: extdeps.transports.sql is AMBIGUOUS rather than consumed-by-filesystem_io, which linked only through operation Delete. THE RE-DERIVATION IS NOT A NULL RESULT. 13 of the 69 leave the residue, and every one lands in AMBIGUOUS-SHARED-ONLY -- no longer provably unconsumed, and NOT proven consumed. That bucket needs a per-row read, so none of them may be deleted on this evidence: nine formatters, the language_model rust root, generic_instantiation, roadmap_dispatch, and gunbhub_serve_program. Restored. 56 remain, still a strict subset of the corrected 114-row residue, still zero island violations. The src/v1 edit dissolves rather than being justified. It existed only because a deleted path left a dangling row in census_extra_excludes; gunbhub_serve_program is back, so the row is correct again and the two count literals go back to 83 and 27. This PR no longer touches the frozen seed at all. The change-detector finding about those literals stands on its own and stays filed -- it was always a property of the pin, not of this deletion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the island: rust_leaf_model_claim's consumer came back with the 13 Restoring v2.test.language_model.rust re-created an in-population consumer for v2.std.rust_leaf_model_claim, so deleting the latter would split the island the restore had just re-formed. This is the island constraint behaving exactly as the census describes it -- eligibility is a property of the SET, so changing the set changes who is eligible, and a restore can create a violation as readily as a deletion can. Computed as a fixed point rather than a single pass: repeatedly drop from the deletion set any module with a surviving in-population consumer, until nothing drops. One iteration, one module. 55 deletions, zero island violations, still a strict subset of the corrected residue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete commit_closure_store on its author's answer, with the cause they gave gentle-eagle-360 (#8820's author) answered the arm the census deferred, and corrected the premise of BOTH arms it offered. The correction is the part worth the row: the envelope did NOT supersede this module -- it holds zero Filesystem operations and not one func, it is a pure codec -- and it should NOT consume it either, because a commit-closure carrier demands a root and a repository's init has none, so wiring them would force init to invent a phantom commit. A census that records a false cause for a true deletion still carries a false row. Cause: STAGED ORPHAN AT THE WRONG GRAIN. Deleted rather than held for the repository-grain layer because a surviving X is an attractor -- every nearby persistence question keeps getting answered in vocabulary already scheduled to die. That is an author volunteering their own module on the doctrine. They also volunteered a defect that strengthens it: the header claims persistence is verified by direct execution in Wet mode, and the probe it names is enrolled nowhere and executes nothing. Unconsumed AND overclaiming its own evidence is a stronger warrant than unreachable. Island check re-run with it in the set, since eligibility is a property of the set: 56 deletions, fixed point, zero violations, still a strict subset of the corrected residue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bring the record's headline numbers and deleted table in line with the final 56 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rewrite the record's stale sections against the final set Four sections described a tree this branch no longer produces. Rewritten rather than annotated, because two accounts of one fact is the defect this document polices elsewhere: section 2's counters are re-measured on the corrected instrument and DEMOTED to necessary- but-not-sufficient with the reason; 4b records the .txt strand as a surface finding whose repair dissolved when its module came back; 4d grows from one defect to four with the mechanism they share and the 13 rows re-deriving cost; 4g makes the island fixed point its own section, since it fired in both directions and is the reason this is one PR. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the held table against the final set, and name the ambiguous 97 beside it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Section 7: state the limits against the final set, including the ones this lane created Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the discriminator roster, the count/set rule, and the two-population skew The reusable result from the cross-lane exchange is that a discriminator travels and a description does not: three relayed bug descriptions found one bug in this extractor, and the four test cases that came with them found a second nobody had named. (e) is contributed back with a specimen whose declared set is EMPTY under an unfixed extractor rather than merely incomplete, which puts it directly on the delete-a-live-module precondition. silent-deer-368's count/set rule is recorded verbatim because it resolves what looked like a discrepancy between two implementations into a property worth stating: a residue COUNT from the precise implementation, a deletion SET from the conservative one. And the skew is stated as a finding rather than bookkeeping, because the natural summary of it is wrong in the dangerous direction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record (f) and its second half: a generic parameter is a binder on both sides of the instrument The sixth case from silent-deer-368 still failed here after implementing (f) exactly as described, because the construct produces TWO independent false references: the parameter list in the header, and uses of the bound name in the declaration's body on the next line. Only region-scoped shadowing moved v2.std.projection to AMBIGUOUS. Scoping is the safety-critical part and the obvious implementation is wrong in the dangerous direction: dropping a bound name file-wide REMOVES references, which moves live modules into the residue. Shadow is scoped to the binding declaration's region. Also withdrew the service short-name credit -- my pattern never matched dotted forms but did match undotted ones, which is exactly the class that produced a false consumption claim on the other lane. Both defects inflate consumption, so neither could have caused a wrong deletion; the deletion set is unchanged at 56 with all six discriminators passing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct this document's own reason for dropping the service credit The reason given was a false-consumption claim measured on the other lane's instrument, and it was never true on this one -- their specimen is a DOTTED service name that this lane's pattern never matched. Restored and re-run with (f) fixed, the credit moves nothing here, so the honest reason is 'no measured effect on this population'. And the evidence points the other way: artifact_store_fs bare-resolves Filesystem.Write with no import, and Filesystem is declared undotted by two modules. A consumer DOES name a service short name bare, so a wholesale withdrawal stops filesystem_io owning a symbol it visibly declares -- the own-nothing direction (e) exists to catch. Recorded as the seventh discriminator. Adopting a peer's conclusion is not the same as reproducing their measurement, and writing their reason into this document as though it were mine was the same error this lane already filed once: a claim carried rather than checked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore the service credit on correctness of ownership, the basis that actually settles it Third and final revision of this reason, and the churn is the point: 'it causes false consumption' was another lane's measurement I had not reproduced; 'no measured effect' is true but settles nothing, since nil effect argues for either choice. Correctness of ownership does settle it -- filesystem_io declares service Filesystem, so an instrument denying it is wrong whether or not a row moves. And withholding the credit was worse than a missing fact: Filesystem is declared twice, service in filesystem_io and resource in std.resources, so dropping the service side handed std.resources FALSE SOLE OWNERSHIP -- manufactured uniqueness, the mechanism behind every wrong attribution in this chain, created by the fix meant to avoid it. Dotted forms now credited by last segment too. Zero exposure in this corpus, same basis. Deletion set unchanged at 56, subset, zero islands, counts identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Roster OwnedDataDiscoveryReceipt: the floor's second refusal, and it is correct Deleting the committed copy of the DO-NOT-COMMIT manifest (4c) removed the only non-test reference to this carrier, so it became inert and unrostered and the inert-carrier lens refused. Verified directly on the symbol's references before and after, not through the re-implementation I first reached for -- that re-implementation shared ZERO names with the live roster under two different readings, so its stable delta was suggestive and not evidence. Rostered rather than restoring the module. The carrier's real consumer is generated at runtime and stamped DO NOT COMMIT, so in the committed tree it is inert BY CONSTRUCTION and no corpus scan can see otherwise; re-committing a file its own generator forbids committing, in order to green a hygiene lens, would be the tail wagging the dog. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the OccurrenceId-keyed reproduction hazard as a class finding Not a claim about this change, which fixed nothing, and not about the original defect, which was root-caused at the declaration with a caller census and is green on main by that repair. The claim is about the CLASS: a defect keyed on a specific OccurrenceId value stops reproducing under any change that perturbs allocation, so a bisect across trees of different module counts measures luck rather than the defect. This branch is the specimen precisely because it contains no fix -- 16 identities red at the base, the same 16 green on a tree differing only by 56 deletions, planned identical at 10425 so roster change is ruled out and corpus size is the isolated variable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record what the static instrument was worth, and the rule for editing the set Two findings the lane owes its next reader. First, measured rather than asserted: across seven instrument defects and four extractor corrections, the static census never identified a live module -- it identified unknowns, correctly, and the one true positive came from one execution. DESIGN 3 as a measurement against a static alternative that had four rounds of sharpening. Second, the zero-near-miss reading carried verbatim, because it is the antidote to a later reader relaxing at a zero: AMBIGUOUS means unresolved, a live module would present exactly as those 13 do, so the honest statement is thirteen rows of unknown status I would have deleted. The same standard is turned on the 56 being deleted -- LowerBoundOnly, best-evidenced, not proof -- which is the argument FOR landing and reading refusals. And the editing rule: 69-13+1 reconciles by the wrong route, since 13 left evidentially and one left structurally. Anyone editing this set re-runs the fixed point rather than adjusting the count; the failure mode is silent because the arithmetic keeps agreeing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Downgrade the hazard-(b) control: a matching count does not rule out roster change An earlier revision claimed 'planned is identical at 10425, which rules out roster change'. It does not -- identical counts are consistent with an unchanged roster and do not establish one. And the caveat is not theoretical: on the next run offered moved 11798 -> 11812 and routed 10425 -> 10439 across two commits changing only a markdown file and one inert_row data row, declines unchanged. Fourteen witnesses entered discovery with no corpus change, cause not yet attributed, so the discovered roster is not a pure function of the committed tree. The comparison survives as corroboration -- the two runs agree on every reported discovery figure and differ by exactly the 56 deletions -- but the isolated-variable claim is downgraded. This is the failure the document records elsewhere, committed in its own write-up: a count treated as a check. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Remove .census/s.json: session scratch with no consumer, and the .gitignore hand-edit it caused .census/s.json is the disposition instrument's raw output, swept into 19d6301 by a broad `git add` rather than authored as a repository fact. Nothing in the tree cites it -- not the census, not the disposition record, not a lens. That is DESIGN.md's experimental-residue tell exactly: a new artifact with no final consumer, in a PR whose whole subject is removing artifacts with no consumers. The accident had a second half. To stop the directory reappearing I had hand-added `.census/` to `.gitignore` -- which is a GENERATED artifact, emitted from gunbc.gitignore_authority. That is manual application committed as source (DESIGN.md §6): the line survives until the next regen and then vanishes without anyone editing it, so the rule it states is not a fact the authority holds. The merge with origin/main surfaced it as a driver refusal on that path, which is the driver working as specified. Both halves are dropped rather than legislated. The scratch directory is session-local and belongs in the session scratchpad, not the repo, so the authority has nothing to say about it and no row is added to it. .gitignore is taken at origin/main's regenerated bytes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore v2.workflow.floor2_prepared_subject: the merge was a third census, and it refused #8896 landed src/v2/workflow/floor_terminal_ledger.dag on main while this branch was open. It imports WitnessIdentity and witness_identity_qualified_name from v2.workflow.floor2_prepared_subject by name, and its test does the same. This branch deletes that module. THE TWO BRANCHES TOUCH DISJOINT FILES, SO GIT MERGED THEM CLEAN. No textual conflict, no marker, no driver refusal -- and the merged tree does not compile. A three-way textual merge answers "did the same bytes change twice"; the question that decides this case is "does the merged tree still resolve", which is not a question about bytes. A merge preserves bytes, not measurements: every count in the disposition record is a statement about a tree, and the merge produced a tree none of them were measured against. The measurement was not wrong. The module was STILL-UNCONSUMED at base 90986d1 on every decoded surface and still is at that commit; it acquired a consumer afterwards. This is the census's second blind spot and it is not fixable by improving the instrument: a static census reads a tree, and the part that had not been written yet is as invisible as the part it decoded wrongly. Found by re-scoring the deleted set against the MERGED tree rather than against main -- a deliberately over-generous token match that flagged nine, of which eight were prose, annotation, or substring collisions (`Binding` inside CapabilityBinding prose, `YamlBool` whose live declarer is a coproduct VARIANT -- defect 7's own shape, in the triage regex this time -- `grade` and `readme` in citation text) and one was real. §4l's rule was followed rather than the count adjusted: the restore's imports were checked for in-population consumers, the fixed point closed at one restore, no cascade followed. 56 deleted becomes 55. The near-miss ledger reads 2, both found by execution and neither by the census: gunbc.pr_digests and this one. §4m records it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct §4m's rule: the adder is the exposed side, and the intersection is unilateral The consequence I published from §4m was "a deletion PR that merges main cleanly is not verified by that merge, so deleters owe a resolve pass". True, and it told a sibling lane it was clear when it was not. bright-ferret-335 checked its subtree against that rule, found no deletion lanes (#8877, #8909, #8882 are purely additive) and concluded it had nothing to check. #8909 adds three files that all import v2.workflow.floor2_prepared_subject -- the module §4m restores. THE HAZARD IS SYMMETRIC AND THE ADDER IS THE WORSE SIDE. A deleter that merges main discovers an added consumer in its own resolve. An adder is already green when the deletion lands later and breaks it, and an additive PR feels safe by construction, so its author has no reason to ask whether anything it imports is scheduled for deletion in someone else's open branch. The party in danger is the party without a prompt. The proposed repair was an intersection requiring one side to publish a list, premised on neither side being able to run it alone. THE DELETER-CANNOT-SEE HALF IS FALSE, and I falsified it by running it: open PR heads are on the remote, so the intersection went against all three sibling PRs from this side with no list. Zero real exposure -- no qualified import of any of the 55, and of the 664 symbols declared solely by the 55 with no surviving declarer, one token hit: render_footer in #8909, which declares its own and never depended on the deleted tools.readme. Deleting it REMOVES a two-declarer whole-pool ambiguity rather than creating a break. So the obligation is unilateral, which is the point of restating it: a rule requiring publication is a rule requiring coordination, and coordination fails silently when a lane is busy, blocked or archived. A rule one party can execute alone has no such failure mode. The deleter owes the intersection against every open PR head at merge time; the adder owes nothing but pushing. An adder who cannot be expected to look cannot be expected to publish either. Residue, strictly smaller than the coordinated version: this reaches PUSHED work only. Never-pushed worktree state is unreachable by any mechanism, and that alone is what publication would buy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the sign-reversed token hit as its own class: a deletion can improve resolution safety From bright-ferret-335, reading the intersection result rather than the rule. The render_footer hit read as a hazard -- a name declared by a module being deleted and used in an open PR -- and inverted on inspection: #8909's consumer declares its own, and while tools.readme stands the name has TWO whole-pool declarers. It is AMBIGUOUS, and the deletion REMOVES the ambiguity. So the same intersection that finds breaks also finds improvements, and a reviewer who reads any token hit as danger will misclassify this direction. It matters beyond one row because it is the ambient-pool defect in miniature: a name resolving by whole-pool uniqueness is one deletion away from binding differently, so its meaning is a function of the corpus denominator rather than of anything written at the declaration or the use. This deletion moves that name from two declarers to one. NOTHING STRUCTURAL GUARANTEES THE NEXT ONE MOVES THAT WAY -- the mechanism that disambiguates here can elsewhere silently rebind a use from one surviving declarer to another. Not created by this change, not closed by it, and visible from here only because an intersection over deletions is one of the few operations that looks straight at it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
The obligation
The v2 self-host program declares a per-identity completed-evidence obligation over
the required floor: for each planned witness identity, the run must be able to say what
terminally happened to that identity. The floor cannot say it today. The accumulation
step destroys the pairing at the exact moment it holds it:
The count survives; the name does not. This process is the only producer that holds a
witness identity and its terminal outcome at the same moment, so the obligation is not
realizable anywhere else, and it is not realizable at all without a bridge here.
What lands
Collection and its consumer, in one change. A collection with no consumer would not
clear the purpose test no matter how cheap it were.
ClaimTerminalRow— one row per planned identity, minted before the branching, soneither the expected-red arms (each of which
continues) nor the ordinary match cansilently omit its population.
reconcile_terminal_ledger— the completeness law as one authority: an identityjoin producing three sets (planned-without-terminal, terminal-without-planned,
terminal-duplicated). Three rather than a first-failure verdict, because an omission and
a duplicate arrive together and a report of only the first hides the half that explains it.
TerminalLedgerIncompleterefusal naming all three sets.claim_disposition— a lossless projection, one arm per terminal shape.outcome.passedis now derived from the rows, and the increment above is deleted,not kept as a cross-check. A cross-check would preserve exactly the disagreement the
derivation makes unrepresentable.
The discriminating RED
A ledger that omits one identity and duplicates another has the same row count, the
same
passed, and the same planned/executed/receipted triple as a healthy run. The checkimmediately preceding this one compares three counts and is green over it.
a_duplicate_replacing_an_omission_is_caught_while_every_count_stays_equalasserts thecounts equal first, then asserts the join names
m.cmissing andm.aduplicated.Calibrated by mutation — the identity join replaced with
planned.len() == rows.len():Reverted, 3 passed. The test calls production
reconcile_terminal_ledger; an earlierdraft carried its own copy of the loop, which would have kept passing while production
drifted arbitrarily far from it.
Standing, honestly
The v2 schema (
v2.workflow.floor_terminal_ledger, merged earlier on this branch) iscapable of deriving every counter; this bridge derives one —
passed— and therest still come from the seed's own accumulators. That is a declared coarseness, not a
claim of completion.
The ledger is consumed in-process (reconciliation refusal +
passedderivation) andis not yet serialized to the v2-owned artifact. Binding, footer and atomic publish are
v2's, and land next.
Scope the seed does not acquire
No candidate digest, no expectation join, no artifact verification, no general evidence
API, no CLI surface, no pass telemetry, no timing histograms, no external TSV
compatibility promise. Nothing changes what counts as a Pass or which claims execute.
The binding — which candidate this evidence is for — is v2's to compute and mean; this
side hands over facts, not identity semantics.
Verification
cargo test --release -p v1-compiler --lib terminal_ledger_completeness_law→ 3 passedgrep -ac TerminalLedgerIncomplete target/release/claim_executor= 1, control string = 0cargo fmt --all --checkclean; no new clippy warning attributable to this diff