Derive admission consumption from exact candidate sets

dag/gunbc/namespace/namespace_wave_admission.dag

@@ -13,7 +13,7 @@ import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopula
 // parented over its enforcement grades its own homework -- so what counts as ADMISSIBLE is
 // homed here, and what the deltas MEAN over the import population stays with that program.
 
-data namespace_wave_admission_note: String = "THE REQUIRED WAVE-ADMISSION WALL over closure, subject-membership and occurrence-binding deltas: gunbc.compiler_frontend_program_interlock milestone NamespaceWaveAdmissionEnrolled.\n\nWHAT IT ANSWERS. For one change, at merge-base grain: which modules entered or left each module's subject, what each module's transitive closure gained or lost, and whether any spelling already authored on both sides changed WHICH DECLARATIONS IT ADMITS. Every motion is classified into NamespaceDeltaDisposition and the run is ADMITTED only when the UNADJUDICATED set is empty -- never when the delta is empty, which is the one-word difference the ruling states explicitly and the weaker spelling of which would refuse the cut itself and then be repaired by weakening the wall.\n\nWHERE IT RUNS. As the namespace-wave-admission phase of claim_executor --required-ci, in the witnesses lane, consuming the index the parse phase built. It acquires no second corpus: the base index is the head index with the diff applied in reverse at FILE grain, so only the files a change touched are parsed again, from their base blobs, while closure and binding are recomputed over both whole graphs -- a module whose own text did not move can still have its subject moved by one that did.\n\nTHE CHANGE CLASS IS DERIVED, NOT DECLARED. NamespaceChangeClass splits preparatory work from work that alters membership or binding. Nothing asks an author which they wrote: the delta is measured and the answer falls out, so PreparatoryNoSemanticMotion is a property of a diff rather than a claim in a pull-request body. Construction over validation.\n\nTWO NON-VERDICTS ARE REPORTED UNDER THEIR OWN NAMES AND ONLY ONE PASSES. A push whose baseline IS its own head -- main after a squash merge -- has no diff to adjudicate, and that is NoSubject: nothing was compared and nothing is admitted. A baseline that does not resolve is NotEvaluated, which the ruling puts on the refusing side, because I could not see what changed and nothing changed are different states with different remedies and the second is the empty-observation narrow.\n\nA STALE ADMISSION REFUSES TOO. A transition-admission row matching no delta is a permission standing over nothing; leaving it would let the roster stop being a fact about the corpus and become a list nobody pruned."
+data namespace_wave_admission_note: String = "THE REQUIRED WAVE-ADMISSION WALL over closure, subject-membership and occurrence-binding deltas: gunbc.compiler_frontend_program_interlock milestone NamespaceWaveAdmissionEnrolled.\n\nWHAT IT ANSWERS. For one change, at merge-base grain: which modules entered or left each module's subject, what each module's transitive closure gained or lost, and whether any spelling already authored on both sides changed WHICH DECLARATIONS IT ADMITS. Every motion is classified into NamespaceDeltaDisposition and the run is ADMITTED only when the UNADJUDICATED set is empty -- never when the delta is empty, which is the one-word difference the ruling states explicitly and the weaker spelling of which would refuse the cut itself and then be repaired by weakening the wall.\n\nWHERE IT RUNS. As the namespace-wave-admission phase of claim_executor --required-ci, in the witnesses lane, consuming the index the parse phase built. It acquires no second corpus: the base index is the head index with the diff applied in reverse at FILE grain, so only the files a change touched are parsed again, from their base blobs, while closure and binding are recomputed over both whole graphs -- a module whose own text did not move can still have its subject moved by one that did.\n\nTHE CHANGE CLASS IS DERIVED, NOT DECLARED. NamespaceChangeClass splits preparatory work from work that alters membership or binding. Nothing asks an author which they wrote: the delta is measured and the answer falls out, so PreparatoryNoSemanticMotion is a property of a diff rather than a claim in a pull-request body. Construction over validation.\n\nTWO NON-VERDICTS ARE REPORTED UNDER THEIR OWN NAMES AND ONLY ONE PASSES. A push whose baseline IS its own head -- main after a squash merge -- checks the roster against that index. A nonempty roster is adjudicated and refuses there, whether stale or provably consumed; only an empty roster reports NoSubject. A baseline that does not resolve is NotEvaluated, which the ruling puts on the refusing side, because I could not see what changed and nothing changed are different states with different remedies and the second is the empty-observation narrow.\n\nA STALE ADMISSION REFUSES TOO. Stale rows refuse every PR; proven consumed rows refuse roster edits and landing (base equals head). Binding admissions author the exact expected candidate set, not a predicted lifecycle disposition. A matching delta is admitted only if its head candidate set equals that authored set. For an unused row, equality at the base derives consumption; otherwise it is stale, with expected and observed members reported. This preserves exact equality while permitting multi-member narrowings such as #11137, whose documented two-member head could never satisfy the old singleton target proof. No lifecycle disposition is authored: the evaluator computes it and the renderer prints it. Between a consuming merge and execution of its main run, roster debt awaits that run; this does not synchronously delete Git content."
 
 // WHY THE GRAIN IS AUTHORED CONTAINMENT IDENTITY AND NOT OCCURRENCE IDENTITY, which is a CLOSED
 // RESULT rather than a shortcut.
@@ -114,7 +114,7 @@ data namespace_wave_admission_note: String = "THE REQUIRED WAVE-ADMISSION WALL o
 
 // THE TRANSITION-ADMISSION ROSTER IS EMPTY AT LANDING, AND THAT IS THE CORRECT STATE: no wave has
 // run, so no transition has been authorised. A row names one exact subject under one exact
-// disposition, and a row matching no delta refuses as stale, so the roster can only shrink toward
+// disposition, and a row matching no delta refuses on main or a roster-touching change, so the roster can only shrink toward
 // its subject.
 //
 // WHAT THE FIRST WAVE WILL NEED, RECORDED NOW AND NOT BUILT NOW. The import/namespace program's
@@ -263,7 +263,7 @@ data namespace_wave_admission_seed_growth_justification: SeedGrowthJustification
     },
     DeclarationRef {
       module_path: "v1_compiler.namespace_wave_admission",
-      decl_name: "admission_consumed_at_base",
+      decl_name: "admission_satisfied_at",
       field: WholeDeclaration
     },
     DeclarationRef {
@@ -424,7 +424,7 @@ data namespace_wave_admission_seed_growth_justification: SeedGrowthJustification
   ],
   reason: "THE OPERATOR RULED THAT A REQUEST TO ADD HAND RUST IS THE OCCASION TO MIGRATE OR DELETE HAND RUST (2026-08-26, relayed by warm-hawk-909: `yes we need to stop adding hand rust asap` and `use it as an opportunity to migrate/delete hand rust`). So this row answers at DECLARATION grain rather than as a count, and it records what the growth request bought back.\n\nWHAT THIS CHANGE DELETES OR AVOIDS, MEASURED, NOT ARGUED. (i) leaf_of was DELETED: it 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. That is a section 3 fork this change had introduced and removed before landing, and it is also the stronger construction, because the reduction the wall keys on is now the corpus authority rather than a local respelling. (ii) render_set was DELETED and inlined at its two call sites. (iii) claim_executor carried a BYTE-IDENTICAL PRIVATE COPY of git_stdout; the wall needed the same helper, and rather than land a third spelling the lib now owns the one copy, the bin`s copy is DELETED and its call sites read it. That is a NET REDUCTION of one pre-existing hand declaration and one fork.\n\nWHAT WAS NOT DELETED AND WHY, PER CLASS, BECAUSE `THESE ARE IRREDUCIBLE` IS A CLAIM AND A REASON PER DECLARATION IS AN ARGUMENT.\n\nCLASS A -- THE PURE FOLD, the declarations named here (a count is deliberately not carried: this row answers at declaration grain, and a transcribed number decays independently of the list it summarizes): adjudicate, binding_rows, binding_disposition, declaring_candidates, declarer_of, closure_of, membership_map, direct_membership, module_prefix_of, membership_declared, membership_bound_through, blast_radius, disposition_label, disposition_auto_admitted, delta_subject_render, report_unadjudicated, render_delta, vocabulary_findings, and the types and constants they fold over. Every one is a pure function of two indexes and needs NO host effect. They are host Rust for exactly ONE reason and it is not effort: their INPUT TYPE is host-only. ModuleDeclarationRecord and DeclarationIndex are Rust types produced by a host walk, and there is no .dag carrier for a per-module declaration record. Authoring one now would be a SECOND REPRESENTATION of a type gunbc.declaration_index_seed_growth already owns -- the section 3 violation this wall exists to refuse elsewhere -- so the correct move is to FOLLOW that carrier`s migration rather than fork it. Its trigger already names this class: when the record derivation is modeled, `the record builder and every finding function follow it`. This roster is one of those consumers.\n\nCLASS B -- THE ACQUISITION, four declarations: git_stdout, in_sweep_scope, base_records, run_required_wave_admission. These are blocked on a DIFFERENT grounding, which is why they are named separately rather than swept into class A: there is no typed repository-read transport a .dag fold can call to obtain the text of a file AT A REF. That is the scm lane`s subject, not a missing surface this change could have authored. base_records additionally needs the frontend`s own per-source parse, which is the same acquisition boundary.\n\nPR #9436 CHECKABLE HAND-RUST RECEIPT (review 56812). The 53 exact transition admissions are DATA consumed by the already-rostered NAMESPACE_TRANSITION_ADMISSIONS declaration; they add no compiler function, type, or admission mechanism. Measured against origin/main after rebasing: `git diff --numstat origin/main -- src/v1/stage0/src/namespace_wave_admission.rs` reports 559 added / 7 removed. `git show origin/main:src/v1/stage0/src/namespace_wave_admission.rs | grep -cE '^(pub )?(fn|struct|enum|const|static) '` reports 34 declarations, and the same grep on the worktree file reports 37. The anchored added/removed forms over `git diff` report 4 and 1 respectively: the unchanged roster declaration moves from the old `DeltaSubject` element type to `AdmissionSubject`, while `AdmissionSubject`, `admission_subject_matches`, and `admission_subject_render` are the three net additions. All three are enumerated in this justification. The initializer is a literal authored roster, not a scan, file read, environment read, or computed predicate. Each row is exact on subject and disposition; stale rows refuse, so the roster has its own deletion trigger: any absorbed or vanished delta makes required CI red until that row is removed. This is an expansion in maintained lines, not in declarations or host capability, and it dissolves row-by-row with the transition it names.\n\nONE THING THIS ROW WILL NOT DO: shrink the wall`s coverage to lower the count. A smaller wall that adds less Rust would spend correctness to buy a metric, which is the ratchet failure DESIGN names in the other direction.\n\nAND THE COUNT WENT UP RATHER THAN DOWN, WHICH IS THE HONEST DIRECTION. This roster was authored at 25 rows and is now 36, because it was JOINED against the module`s actual declaration population instead of listed from memory: leaf_of, binding_rows, vocabulary_findings and three constants 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. Four methods were also converted from inherent impl blocks to free functions, because std.decl_ref names WholeDeclaration or NamedField and neither names a method on an impl block -- so as methods they would have been UNCITABLE items the roster structurally cannot enumerate. The module now carries no impl block, and every declaration in it is enumerated here.\n\nNO LABEL CONSTANT IS ENUMERATED HERE ANY LONGER, AND FOUR HAVE NOW BEEN DELETED BY THEIR OWN TRIGGERS. THE STANDING GAP THIS ROW ALREADY WARNED OF HAS NOW FIRED IN THE OTHER DIRECTION, AND THAT IS WHY THE COUNT MOVES. CALL_SEMANTICS_TARGET_REHOME_LABEL was gunbc#10688`s own; gunbc#10813 deleted the constant when its rows reported CONSUMED but left this enumeration`s DeclarationRef for it standing, so the roster cited a declaration the module no longer carries -- the exact decay this row predicts, now visible from the surviving side rather than the missing one. gunbc#10856 removes that stale reference. RECURRING_FAILURE_MODE_CLASS_ADDED_LABEL, which gunbc#10813 added and never enumerated here, is deleted with its row on the same change. Those two are the LABEL half of the decay only; the same change also repairs the nine non-label defects recorded below, after which no reference here is dangling and no declaration is unenumerated. NAMESPACE_TRANSITION_ADMISSIONS therefore stands as an EMPTY enumeration, which is the honest reading that no transition is currently admitted -- the declaration is not deleted, because the roster`s population is an enumeration and never a predicate. AND IT IS EXPECTED TO STAY EMPTY FOR THE FAILURE-MODE LEDGER SPECIFICALLY: the per-class admission row gunbc#10813 authored was admitting a BASELINE defect rather than the ledger`s growth shape, and gunbc#10856 repairs that baseline, so appending a class no longer produces a delta needing a row. EXIT_OK_REHOME_LABEL and SCM_REPOSITORY_BUILDER_REHOME_LABEL are likewise NOT listed because they no longer exist: both sets of rows reported CONSUMED and came due on the next roster-touching change, which this one is, so the rows and their labels went together, each adjudicated by the per-spelling declaration join those rows demanded rather than by their own trigger sentence. A label constant is text shared by the rows that cite it -- no compiler function, type, or host capability -- and it dissolves with the last row carrying it, which is why the enumeration loses every one of them and gains none.
 
-THE STANDING GAP THIS RECORDED HAD ALSO DECAYED IN THE OTHER DIRECTION, AND gunbc#10856 RAN THE JOIN BY HAND RATHER THAN REPEATING THE CLAIM. EXIT_OK_REHOME_LABEL was never enumerated while it lived, and neither was SCM_REPOSITORY_BUILDER_REHOME_LABEL before it, so the sentence above -- that every declaration in the module is enumerated here -- had been false for two lanes running without anyone being at fault. It was false again at this change`s own head, in BOTH directions at once: membership_supported was enumerated here after the declaration had been renamed away (the module`s membership arm is membership_declared over membership_bound_through), and eight declarations were enumerated nowhere -- KERNEL_DECLARATION_IDENTITY, ADMISSION_ROSTER_REL_PATH, diff_sides, admission_consumed_at_base, membership_declared, membership_bound_through, locally_authored_claim_added and wave_admission_refusal. All nine are repaired here, and the enumeration now stands in EXACT BIJECTION with the module`s declarations, joined at NAME rather than at count. That bijection is a MEASUREMENT OF ONE HEAD, not a mechanism: nothing in the repository performs this join, so it will decay again the moment a lane adds a declaration without adding a row. The mechanical repair is unchanged and is precisely the per-module declaration record gunbc.declaration_index_seed_growth owes, which this roster`s CLASS A already waits on.",
+THE STANDING GAP THIS RECORDED HAD ALSO DECAYED IN THE OTHER DIRECTION, AND gunbc#10856 RAN THE JOIN BY HAND RATHER THAN REPEATING THE CLAIM. EXIT_OK_REHOME_LABEL was never enumerated while it lived, and neither was SCM_REPOSITORY_BUILDER_REHOME_LABEL before it, so the sentence above -- that every declaration in the module is enumerated here -- had been false for two lanes running without anyone being at fault. It was false again at this change`s own head, in BOTH directions at once: membership_supported was enumerated here after the declaration had been renamed away (the module`s membership arm is membership_declared over membership_bound_through), and eight declarations were enumerated nowhere -- KERNEL_DECLARATION_IDENTITY, ADMISSION_ROSTER_REL_PATH, diff_sides, admission_satisfied_at, membership_declared, membership_bound_through, locally_authored_claim_added and wave_admission_refusal. All nine are repaired here, and the enumeration now stands in EXACT BIJECTION with the module`s declarations, joined at NAME rather than at count. That bijection is a MEASUREMENT OF ONE HEAD, not a mechanism: nothing in the repository performs this join, so it will decay again the moment a lane adds a declaration without adding a row. The mechanical repair is unchanged and is precisely the per-module declaration record gunbc.declaration_index_seed_growth owes, which this roster`s CLASS A already waits on.",
   owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
   trigger: "Delete these in TWO steps, one per class above, and a PARTIAL migration is the expected shape rather than a failure. Class A follows gunbc.declaration_index_seed_growth`s first step: the moment a per-module declaration record is a .dag carrier, every one of the CLASS A declarations moves with it, because they are pure folds over it and nothing else. Class B follows the scm lane: when a typed repository-read transport can supply a file`s text at a ref. adjudicate, binding_disposition, declaring_candidates, declarer_of, closure_of, membership_map, direct_membership, module_prefix_of, membership_declared, membership_bound_through and blast_radius are pure functions of two indexes and move to .dag the moment the per-module record derivation does -- they need no host effect at all, so they follow gunbc.declaration_index_seed_growth's first step rather than waiting for its second. git_stdout, in_sweep_scope, base_records and run_required_wave_admission stay behind until a typed repository-read transport can supply a file's text at a ref, which is the scm lane's subject. A PARTIAL migration is the expected shape. What does NOT dissolve them is the phase moving to another host entry point, and what does NOT dissolve them is a hermetic witness over a fabricated pair of indexes -- the fixture suite already does that, and it is the evidence rather than the dissolution.",
   current_boundary: "src/v1/stage0/src/namespace_wave_admission.rs; src/v1/stage0/src/declaration_index.rs dotted_chain and ModuleDeclarationRecord.referenced; src/v1/stage0/src/bin/claim_executor.rs phase namespace-wave-admission; src/v1/stage0/tests/namespace_wave_admission.rs; dag/gunbc/namespace/namespace_wave_admission.dag"