Identity-bearing required-lens registration, and a closed registration/observation join at the compile door

[briansrls]

Step 1 of the compile-obligation activation brief (ACT lane, work item adhoc-74a1fd50-8f9): the substrate everything else keys on — the required-lens roster names its lenses, and registration/observation is one closed, machine-checkable join.

What changed

• One registration roster. required_compile_lens_roster carries all eight required lenses, each as CompileLens { identity: DeclarationRef, grain, gate }. required_lenses_at_grain derives the two execution partitions; always_required_lenses / always_required_root_lenses are deleted at the root and their five consumers cut over.
• Witnesses name their producer. LensGateWitness { lens, grain, witness }.
• The join refuses by name. join_required_lens_coverage → RequiredLensCoverageClosed { roster_digest, rows } or RequiredLensCoverageRefused { cause }, with causes RequiredLensRosterEmpty | RegistrationDuplicated | RegistrationUnobserved | ObservationUnregistered | ObservedAtWrongGrain | RootLensObservedMoreThanOnce. Root grain states exactly-one; subtree grain is at-least-one, because subtree registrations are observed once per node by construction — stating exactly-one for both would refuse every tree with more than one node.
• The door gates on it. validate_then_compile runs each lens at its registered grain (caller-supplied lenses included — they previously ran at root whatever grain they declared), derives the coverage from the witnesses it collected, and refuses the compile when it is not closed. Validated carries the receipt.
• Joins go through map_lookup on the display key, never map_keys (the determinism lens registered here refuses key-order reads), and are linear in the observation count.

Divergence, stated (DESIGN §3b)

The brief named a new RequiredCompileLens beside CompileLens. Requiredness is membership in the roster, not a property of the carrier — and a caller-supplied lens has the same three facts and must stamp its witnesses identically for the join to be closed at all — so one carrier gains the two fields instead of a second type being minted.

Evidence, by execution

claim_batch --source-root dag --source-root src/v2, local release build.

v2.test.lens_application.required_lens_coverage_join — 7 green:

• required_lens_coverage_closes_on_complete_observations_holds (positive control over the real roster, digest asserted)
• required_lens_coverage_closes_over_executed_gates_holds — runs all eight registered gates through the door's own two runners and joins the witnesses they actually stamped
• five discriminating REDs, one per refusal arm, each asserting the cause and the lens identity

The eight touched pre-existing lens witnesses: all green (rejecting_lens_blocks_before_compile, enforce_rejecting_gate_fires, introspect_clean_tree_passes, apply_lens_introspect_rejection_is_advisory, empty_required_lenses_skip_gate, hollow_alias_blocked_via_always_required_lenses, unit_modeling_blocked_via_always_required_lenses, modeled_unit_field_admitted_via_always_required_lenses).

Not established, and not claimed (DESIGN §4b rung honesty)

An Accepted validate_then_compile carrying the receipt. No fixture in this corpus reaches Accepted through that door today — measured on fixture_add_resolved_tree in both TranslateTo (stub target) and Eval, where the refusal is upstream of the lens rosters and names neither compile_pipeline_not_realized nor compile_lens_gate_rejected. The door-grain positive control is a declared frontier whose trigger is a route that reaches Accepted through the door — the activation authority's Executed→Qualified step. The frontier is recorded in the test module header, not only here.

Side finding for the census lane: door_root_roster_runs_and_passes_clean_tree in v2.test.long.accumulator_copy_compile_gate is green on a fixture the door rejects — its assertion tolerates any rejection that is not the poly2 suspect.

Follow-ups from the brief (separate PRs): the all-lens introspection ledger, the activation authority compile_obligation_activation.dag, the complexity bundle, and receipts into promotion admission. The census join (every registration has one census row) waits on gunbc.v2_compile_obligation_census landing.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f

[gunbai-bot]

srv2 167-member closure receipt (closure-neutral; emitted compiler builds with the new 00_compile.dag root)

Provenance. main 267d69b86c; PR head at fetch 8825767f overlaid as commit 6f0c9c7b; the two later pushes (f6a16f96, e8f49dc7) differ from 8825767f only in src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag and one renamed field in dag/gunbc/witness/witness_deferral_freeze.dag, neither a closure source, so this receipt carries to e8f49dc7. Producer = pinned claim_executor sha256 87a69424ab1060de built from the overlaid tree, --v2-native-route --source-root dag --source-root src/v2 (post-#11003 route). Emission: 172 files, closure bb946c9d…, emitted compiler built to sha256 85d22ab3…. Closure fold wall 283.4 s, rss 1.23 GB.

Result. 66 refusing closure members, 0 regressed, after-set IDENTICAL row-for-row to the #10988 recovery baseline on the same main (68 -> 66 vs the immutable 2fb67b41 reference is main's D1+G effect, not this PR's). The rewrite of the lens-registration roster and validate_then_compile in src/v2/compiler/00_compile.dag changes no closure member's acceptance and the emitted whole compiler still builds.

Not established here: whole-v2.test.* admission; the drop gunbc.rung_drop v2_native_route_off_the_merge_path is not retired by this receipt. Voided by any push touching src/v2/{compiler,std,lens,extdeps}, dag/std or dag/extdeps.

[gunbai-bot]

Both findings in review 63457 verified against the current tree and fixed in 0230f764b75.

1. Stale citations — confirmed, and wider than the note. required_lens_grain_note was re-asserted verbatim while both symbols it is about were deleted in the same diff. git grep across the tree found five further prose sites naming them. The note is rewritten to carry the same cost argument in terms of what survives — a CompileLensSubtree registration runs per subtree node (node-local predicates, a nested walk inside the gate would stack with run_required_lens_gates_on_subtree's fold_node and be O(n²)); a CompileLensRoot registration runs once at the root (rooted whole-tree walks, where per-node invocation would be O(n²)); grain is a field, and required_lenses_at_grain derives each execution's list from the one roster, so the cost argument is carried by the row rather than by which of two lists a lens was written into. It also now records the behaviour change the diff introduced: a caller-supplied lens runs at its own declared grain.

Also cut over: v2.lens.determinism, v2.lens.mandatory_tag, v2.lens.mandatory_tag.corpus_scan, v2.lens.machine_shape, v2.lens.undecidable_verdict_collapse, v1.compiler.emit_rust, gunbc.declaration_index_seed_growth, test.claim.computation_demand_duplication_witness.

2. Dropped prohibition — confirmed, and the new text did invite the regression. The lens_module_gate de-enrollment rationale is carried forward in force beside the roster, with its named red class (lying_substrate_inputs_only_stamp_census, 31 stamps) and its honestly-stamped replacement consumer. Because "adding a lens is one row" otherwise reads as an invitation, the eligibility rule it implies is now stated explicitly: a row must be a pure fold over the tree being compiled at its declared grain; a nullary gate, a corpus scan, or any gate that reads the live tree rather than its InferredTree argument is ineligible at either grain — a corpus-grain invariant enrolls on the corpus cadence with a ReadsLiveTree stamp, never in the per-tree door.

Not done, stated rather than left silent. Three test modules still carry the deleted symbol in their own names (lens_fact_density.hollow_alias_blocked_via_always_required_lenses and the two lens_unit_modeling siblings). Renaming them is a file-and-module rename whose citations include gunbc.live_deploy.srv1_residue_rehearsal — a recorded path wire, i.e. an observation receipt — and dag/gunbc/witness/witness_row_cost_basis.tsv. Editing a recorded observation so it matches a later rename is not a citation repair, so that cut is its own change rather than a hunk in this one.

Evidence: the coverage-join witnesses re-run green after the edits (required_lens_coverage_closes_over_executed_gates_holds, required_lens_coverage_refuses_unobserved_registration_holds).

— sent from calm-crane-722

[gunbai-bot]

Both fixed in ced80f419a9, and one correction to the aside.

src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag:24 — confirmed, and the sharpest form of the finding: the file is already in this diff (its import moved to required_lenses_at_grain / CompileLensRoot), so prose and code disagreed inside one file. Now reads "the CompileLensRoot partition of required_compile_lens_roster".

docs/plans/determinism-boundary-relative.md:8 — confirmed, fixed differently, and the difference is deliberate. That citation sits inside a block the file's own header declares "preserved verbatim from that row" (a DESIGN.md row deleted on operator ruling 2026-08-18). Rewriting a symbol inside a quotation falsifies the quotation, so the quoted sentence is left as authored and the current symbol is named beside it in brackets: always_required_root_lenses [since #11004 that roster is required_compile_lens_roster, read at CompileLensRoot grain through required_lenses_at_grain; the sentence is preserved as authored and the current symbol is named here rather than rewritten into the quotation]. §3 is satisfied — a reader greps a symbol that resolves — without editing a record. Same reasoning as the three test-module renames deferred out of this PR, whose citations include a recorded path wire.

You misread the stage0 hits, and it is worth knowing in which direction. src/v1/stage0/src/v2_compiler_compile.rs is not a generated snapshot: its own header says "Seed realization for v2.compiler.compile (Wave 2 Gate-A flip). Hand-retained Rust oracle — independent of the self-emitted artifact under test. Dissolve-on: self-emit cutover retires this module…". So it is hand-retained, and it carries the pre-PR required_lens_grain_note string verbatim — a real divergence between the .dag authority and its seed oracle, not an out-of-scope artifact.

I am not fixing it in this PR, and the reason is not scope-aversion: that module is the independent oracle this change is checked against, and editing the oracle in the same push as the subject removes the independence for exactly the run that matters. It also widens a registration change into a seed edit whose bootstrap blast radius is its own review. It is reported to the lane owner as its own item; if the call is to fold it in, say so and it is one string.

git grep -n always_required_root_lenses now returns only those stage0 hits and the bracketed editorial note above.

— sent from calm-crane-722

[gunbai-bot]

srv2 167-member closure receipt, re-taken at afdec358 (carries to ced80f41)

Supersedes the receipt above (which was taken on 8825767f, before the review-63457 citation cutover touched six closure-source files).

Provenance. main 0267f385 (D1+G plus the #10978 failure-mode row, which touches no closure source); PR head afdec358 overlaid as commit bb9260a0; pinned claim_executor sha256 4a065e03a7fb2fdc built from the overlaid tree, --v2-native-route --source-root dag --source-root src/v2 (post-#11003 route); emitted compiler built to sha256 c03f6e73…. Closure fold wall 284.1 s, rss 1.23 GB. ced80f41 differs from afdec358 in one test-file prose line and one docs-plan line, neither a closure source, so this receipt binds to ced80f41.

Result. 66 refusing closure members, 0 regressed, after-set IDENTICAL row-for-row to the #10988 recovery baseline (the 66-row set on the post-D1+G main). The registration roster rewrite, the citation cutover across 00_compile.dag and five lens modules, and the carried-forward de-enrollment prohibition change no closure member's acceptance, and the emitted whole compiler builds.

Not established: whole-v2.test.* admission; gunbc.rung_drop v2_native_route_off_the_merge_path is not retired by this receipt. Voided by any further push touching src/v2/{compiler,std,lens,extdeps}, dag/std or dag/extdeps.

[gunbai-bot]

review 63517 is right and I am reversing my earlier position on this PR. Fixed in cd7388c36f7.

What I got wrong, and why it is worth stating rather than just patching. Earlier in this PR I argued the opposite — that the stage0 oracle should not be cut over here, because editing the independent oracle in the same push as its subject removes the independence for exactly the run that matters. That reasoning is sound in general. It is wrong for this string, and I never checked the one thing that decides it: whether anything asserts equality on it.

Something does. dag/gunbc/instruments/self_host_00_compile_shims/witness_main.rs compares emitted::required_lens_grain_note() against seed::required_lens_grain_note() and makes that equality the Gate-A behavioral receipt. So the literal is not a mirror of the authority for a reader's benefit — it is the value the self-host equivalence claim is made of. Changing the .dag without it does not preserve the oracle's independence; it falsifies the receipt my own change exists to keep true. You measured the divergence (1288 vs 934); I had asserted it away from a principle.

The fix, and how it was verified rather than eyeballed. The seed literal is derived from the .dag line programmatically rather than retyped, then byte-compared: equal? True, 1288 == 1288. cargo check --release -p v1-compiler --lib is clean.

I also changed the oracle's header to say what it actually is, so the next reader does not repeat my reasoning:

The Gate-A behavioral witness (dag/gunbc/instruments/self_host_00_compile_shims) asserts EQUALITY between the emitted artifact and this oracle, so this string is not documentation of the authority — it is the compared value, and it cuts over with it.

One note on the §7 framing, which I think is exactly right and is the part I would have missed even after fixing the string: the seed-retained oracle is the self-host differential, so "do not touch the oracle" and "the oracle must agree with the authority" are not in tension — the oracle is independent in its derivation, not in its content.

— sent from calm-crane-722

[gunbai-bot]

The failing check on cd7388c is not this diff, and I am deliberately not re-running it yet.

What failed: required-witnesses-build, at

error: could not compile `v1-stage0-std-surface` (lib)
  could not execute process `…/_temp/rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/rustc …`
  No such file or directory (os error 2)
##[error]Process completed with exit code 101.

followed by the runner losing its own action cache:

Can't find 'action.yml' … under '…/_actions/actions-rust-lang/setup-rust-toolchain/v1.16.0'
Can't find 'action.yml' … under '…/_actions/actions/checkout/v5'

So rustc vanished mid-job and the runner's _actions/ directory went with it. On srv1-19. This is the same failure that took #11025's wet lane an hour ago on srv3-15, where the workflow's own toolchain_filesystem_probe captured the joined reading: rustc exists=no at start, ENOENT at use, exists=yes mtime=06:24:39 at end — reinstalled nine minutes after it was needed. Two hosts, same shape, which is the condition that probe's dissolve-on names ("the fleet fixes the toolchain deleter").

Why not re-run now: this PR is held from merge pending the D-train, and when it is released it must re-merge main and take a fresh closure receipt anyway — so a run started now is a run that gets superseded, on a runner pool that is currently the binding constraint for three other PRs and for main itself (main is red on the floor at c047472bf4f with 12 blockers, 11 of them interrupted_before_verdict). Spending a build cycle to produce a result that will be re-produced after the remerge is the wrong trade while the fleet is in this state.

The check will be re-run as part of the post-D4 remerge, which is the point at which its result means something about the head that will actually land.

— sent from calm-crane-722

[gunbai-bot]

Both fixed in c6bd401a921.

1. The header claim was false, and I wrote it. RequiredLensJoinCause has six arms; the module header said "one discriminating RED per refusal arm" and the PR body said "five discriminating REDs, one per refusal arm". RegistrationDuplicated — the arm whose entire job is catching a roster that acquired a second row for one identity — had no control asserting it fires. Your grep is right: declaration, reason mapping, construction site, five => false exhaustiveness arms, and nothing that makes it go.

The "unreachable at the door" observation is true and is not a defence, and §4b settles where the question is decided: a state unrepresentable in the ACCEPTED corpus may still be perfectly representable as source handed to the compiler by a fixture… if the refusal is still authorable there, the evidence is enrollable there and declining it is specification-without-execution. The sibling REDs already hand the join synthetic rosters, so this was one call — list_append(required_compile_lens_roster(), [first_root_registration()]) — which is what makes it an omission rather than a judgement call. Eight controls now pass, and the header sentence is true for the first time.

2. The census witness citation. Cut over to required_compile_lens_roster, with the annotation now recording that the gap it describes — no identity join between the census's rows and the roster's contents — never turned on there having been two lists.

That is the third instance today of the same shape, and it is worth naming since it will keep happening: v2_compile_obligation_census_witness_test arrived with #10942 after my citation sweep, citing symbols this PR deletes at their root. Neither lane could see it alone — the census cited declarations that were live on main, and my sweep covered every citation that existed when I swept. The break exists only in the merge, which is why the declarations phase is the only thing that catches it, and only on whichever PR merges second. A row for that class is queued for after this lands.

Untouched deliberately: the entry/function/module_path rows for hollow_alias_blocked_via_always_required_lenses and siblings — module and function identities that still resolve, not symbol citations, and their rename touches a recorded path wire.

— sent from calm-crane-722

[gunbai-bot]

Review 63827's finding is correct and is fixed in c12c66c.

I verified the claim rather than taking it: at c6bd401a92, git grep always_required_root_lenses\|always_required_lenses over src/v1, src/v2 and dag leaves src/v1/stage0/src/cli_run.rs as the only surviving citation of the deleted symbol — the other hits are witness function names (hollow_alias_blocked_via_always_required_lenses_holds) and the module paths those witnesses live at, which name themselves rather than the roster. src/v1/05_emit_rust.dag had already been cut over in this PR, and the hand-retained oracle in src/v1/stage0/src/v2_compiler_compile.rs already carries the new note (it is the compared value for the Gate-A byte-equality witness, so it had to).

The comment now names the registration as it actually stands: required_compile_lens_roster at CompileLensRoot grain, the mandatory_tag_lens row. That wording is deliberate rather than a mechanical substitution — the point of the rename is that the grain is a field on the row instead of a fact about which of two lists a lens was written into, so a citation that named a list would be stale in meaning even if the symbol resolved.

Thank you for checking whether the file was a projection before recommending a hand edit; it is hand-maintained seed Rust, and had it been generated the repair would have belonged in the authority instead.

On the run at this head: the floor's measurement completed (3625 passed, 0 failed) with one identity budget-refused at 507/500 ms cpu while the host was page-thrashing at 300-400k majflt/min — an unobserved host condition rather than a result, so this push's run is the observation.

— sent from calm-crane-722

[gunbai-bot]

Pushed 540c92c — the per-claim cost of this PR's touched witness, cut at the place the measurement pointed rather than the place it was first assumed to be.

Why the obvious cut was wrong. The blocker is gate_refusal_ledger_counted_not_gating reaching the 500 ms per-claim CPU ceiling without a terminal verdict (three runs now; the latest log names it outcome=budget-refuse). The intuitive fix is to shrink its planted ledger. Measured with claim_batch over this module's four witnesses in one remote dispatch:

witness	cpu	path
gate_red_quadratic_rejects	618 ms	source → tokenize/parse/normalize → gate
gate_green_identity_accepts_clean	534 ms	same
gate_refusal_ledger_counted_not_gating	680 ms	same
door_root_roster_accepts_clean_inferred_tree	50 ms	node fixture, no front end

Three different four-line snippets spread ~150 ms over a ~530 ms base, so the base is the front end, not the snippets — and the ledger-free siblings pay 534 and 618 for the same prefix. Shrinking the ledger could not have moved a 680 ms witness under 500 ms. The larger fact: all three source-path witnesses here are at or over the ceiling on an unloaded runner. This one is not defective beside three healthy ones; it is the one 80 ms above its nearest sibling. Host thrash is why it trips today; the budget is why it would trip anyway.

The cut keeps the source path. The three claims are now nullary producers enrolled WARM in v2.workflow.floor_pure_producer_share, so strict preparation forces each once, outside every per-claim budget. Same source, same tokenize, same parse, same normalize, same tree — paid once instead of three times. The precedent is v2.test.claim.parse.d1_declaration_grammar_parse, whose annotation records seven of its eight rows interrupted at this same ceiling and repaired the same way.

I did not move the ledger assertion onto a hand-built fixture. That buys the budget by trading what the witness proves — ledger behaviour on a tree the real front end produced — which §4b(1) prices as a rung drop, not a cost fix.

One deliberate divergence from the precedent: d1 shares at the parse tree because some of its claims name normalize as their subject. No witness here names any front-end stage, so the whole front end is upstream of every subject in this file and the honest seam is its output.

Verification bound, stated plainly: claim_batch under my invocation refuses this module with no field 'kind' on type 'NormalizedTree' inside normalize while the floor accepts it (3625 passed, 0 failed), so I cannot execute these three witnesses locally. What I verified is that both modules parse in a whole-corpus index and the roster fold evaluates with the three rows present. Whether the NormalizedProbe value reifies portably is decided by the floor — and a warm row that refuses to store stops the line rather than degrading, which is the correct failure mode but is a real risk, not a formality. The precedent shares Outcome<Node>, the same shape class. That instrument-vs-floor disagreement is being filed separately as a receipt.

Review 63865's approval noted, with nothing actionable in it.

— sent from calm-crane-722

[gunbai-bot]

Accepted-path measurement, and a correction to my own earlier reasoning on this PR.

The floor at 6b153bf8 produced real accepted-path CPU for the three source-path witnesses:

witness	source bytes	cpu	outcome
gate_red_quadratic_rejects	116	503 ms	BUDGET-REFUSED
gate_refusal_ledger_counted_not_gating	109	505 ms	BUDGET-REFUSED
gate_green_identity_accepts_clean	88	525 ms	BUDGET-REFUSED

The shortest snippet is the slowest. Sizes differ by 32%, costs by 4%, and the ordering is inverted — source size and cost are uncorrelated here.

That refutes the rationale in commit 87a3632. That commit cut the probe sources and predicted ~3 ms/byte, saving 27/30/57 ms. The model was fitted to two lower-bound points from claim_batch runs that died inside normalize; three clean accepted-path points destroy it. The cut is semantic-neutral and harmless, but it bought nothing and its stated premise was wrong — I'm recording that here because a squash drops branch commit messages, so this comment and the PR body are the record that survives. The cut will be reverted in the next push that has to happen anyway, rather than as a push of its own.

What the numbers actually establish, which is more useful than the cut:

1. All three source-path witnesses are over the line, not one defective witness beside two healthy ones.
2. The per-claim cost is ~500 ms of fixed front end — dag_language_model plus tokenize/parse/normalize — before any subject-specific work exists.

And the framing I had wrong. These three witnesses are never planned on main: v2/test/claim/long/ is a DeclinedLongModule whose cadence has been declared-unrealized since falsifier.yml was deleted, and no green floor's claim-cost artifact carries a row for this module. The 500 ms line applies here only because this PR touched the file, so the floor planned its rows as changed witnesses, which take the armed line. I was measuring a cost no green floor ever pays and reading it as a defect in the witnesses. It is neither a regression nor debt this PR created.

The corpus already carries the policy for this shape — v2.workflow.required_floor changed_witness_cost_policy implements the FLOOR-CHANGED-COST-0 ruling (a changed witness whose expensiveness is already declared debt runs CpuDeadlineObservedOnly, verdict still gating) — and it simply does not consult the long-lane classification. That is an operator decision and has been escalated; this PR is held pending it rather than working around it.

Separately, review 63901's fix is in 8c80a9a5: the grain note no longer claims prepend-then-reverse for a fold that does append-in-step. I did not swap the operands to make the claim true, because list_append costs its left operand and rc_list_concat copies its right one — no ordering makes a tree fold linear, so swapping would have moved the copy while letting me report it fixed. The repair is a concat that copies neither operand, which is carrier work and tracked separately.

— sent from calm-crane-722

[gunbai-bot]

The snippet cut is now falsified by a paired measurement, not just a cross-sectional one.

Same three witnesses, before and after the cut, both on the floor's accepted path:

witness	6b153bf8 (before)	8c80a9a5 (after cut)	Δ	bytes removed
gate_red_quadratic_rejects	503 ms	516 ms	+13	9
gate_refusal_ledger_counted_not_gating	505 ms	508 ms	+3	19
gate_green_identity_accepts_clean	525 ms	507 ms	−18	10

Commit 87a3632558 predicted savings of 27/30/57 ms from a ~3 ms/byte marginal model. The actual result is noise in both directions, with two of three slower after removing bytes. Combined with the earlier cross-sectional finding — the 88-byte snippet was the slowest of the three — source size is not a cost term here at all. The cut bought nothing and its premise is refuted twice over; it reverts in the next push.

What the numbers do establish: the per-claim cost is a ~500 ms fixed front end — dag_language_model plus tokenize/parse/normalize, rebuilt in every claim's own evaluation frame — and it is invariant to the subject-specific work the witness actually does.

This PR needs no further fix for it. These three witnesses are never planned on an ordinary floor (v2/test/claim/long/ is a DeclinedLongModule whose cadence has been declared-unrealized since falsifier.yml was deleted; no green floor's claim-cost artifact carries a row for the module). The 500 ms line reaches them only because this PR touched their file, making them changed witnesses — so the floor is reporting interrupted_before_verdict on a cost no green run has ever paid.

The operator ruled on it (A, via fierce-lark-661): changed_witness_cost_policy already implements FLOOR-CHANGED-COST-0 for a changed witness whose expensiveness is declared debt, and simply did not consult the long-lane classification. That arm is #11073, now open. This PR remerges onto it once it lands, folding in the snippet-cut revert and review 63922's identity-join fix.

— sent from calm-crane-722

[gunbai-bot]

Review 64245, secondary finding — not fixed, and here is why rather than an acknowledgement.

The finding is that required_lens_grain_note puts a ruling citation, a measured cost claim and a deferral inside a String row, where §4c wants a typed carrier or a // annotation, and that // is available two screens above.

The premise that makes that repair cheap does not hold here: this string is not commentary, it is a compared value. It is the only case in the self-host behavioral receipt — dag/gunbc/instruments/self_host_00_compile_shims/witness_main.rs compares emitted::required_lens_grain_note() against seed::required_lens_grain_note(), and src/v1/stage0/src/v2_compiler_compile.rs is a nine-line module whose entire content is that same string. Moving the prose to a // annotation does not relocate commentary; it empties the receipt's case list, because annotations are erased before any semantic pass and no Accepted program can read one (§4c's own second consequence).

The defect the finding is pointing at is real, and it is already rostered: gunbc.recurring_failure_mode receipt_subject_is_the_prose_about_the_mechanism names this exact declaration as its specimen, and states the problem more sharply than a §4c placement note would — "the strongest verdict the emitted crate can publish about the compile door is that two copies of a sentence about lenses agree, while the door's eight enrolled gates, its lens fold, its subtree walk and its rejection path are all outside the receipt's subject." Shrinking the string would leave that intact while making the receipt's subject smaller, which is motion, not repair. The repair is that row's trigger — a receipt whose subject is the mechanism.

So the honest disposition is: the §4c placement is a consequence of the rostered defect rather than an independent one, and fixing it locally in this PR would change the self-host receipt's subject as a side effect of a comment-placement edit. That belongs with the row that owns it.

The primary finding is fixed in 56074004b3. The deferral named no carrier because none existed — the sentence asserted a disposition that did not exist, which is §4b(2)'s untracked stall in the authority a reader consults first. gunbc.recurring_failure_mode enforcement_exhibits_the_shape_it_refuses is filed and cited, with the trigger named as a capability (a concat copying neither operand — carrier work in the list algebra) and the falsified experiment recorded beside it, since docs/plans/emit-type-surface-traversal-cost.md measured that exact substitution at 215 sites as byte-identical with no measurable change at the emit seam. Citing that plan as the owner would have pointed a reader at a document whose finding contradicts the framing; recording it as falsified for that seam is what stops the next author re-running it as the repair.

Both sides of the receipt moved in lockstep and are byte-identical at 2556 characters, asserted by extracting and comparing the two strings rather than by inspection.

— sent from calm-crane-722

[gunbai-bot]

For the accumulator-copy analyzer lane — the three-way discriminator, verbatim, so you start from evidence rather than rediscovering it.

gate_red_quadratic_rejects can fail three ways and they demand different repairs. These ran in a throwaway worktree at origin/main (2090c1b01b), appended to src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag:

test fn diag_stage_rejected() -> Bool {
  match normalized_of(source: quad_snippet) {
    ProbeStageRejected { stage: _ } => true
    ProbeNormalized { root: _ } => false
  }
}

test fn diag_gate_accepted() -> Bool {
  match normalized_of(source: quad_snippet) {
    ProbeStageRejected { stage: _ } => false
    ProbeNormalized { root: root } =>
      match accumulator_copy_compile_gate(node: root) {
        Rejected { diagnostics: _ } => false
        Accepted { value: _, diagnostics: _ } => true
      }
  }
}

test fn diag_rejected_but_other_reason() -> Bool {
  match normalized_of(source: quad_snippet) {
    ProbeStageRejected { stage: _ } => false
    ProbeNormalized { root: root } =>
      match accumulator_copy_compile_gate(node: root) {
        Rejected { diagnostics: d } =>
          !non_empty_contains_reason(d: d, reason: ^accumulator_copy_poly2_suspect)
        Accepted { value: _, diagnostics: _ } => false
      }
  }
}

Result on origin/main: diag_stage_rejected FAIL, diag_rejected_but_other_reason FAIL, diag_gate_accepted PASS. The specimen normalizes fine and the gate is not rejecting with a wrong reason — it accepts. accumulator_copy_findings returns no suspect for fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) }).

Latency, established rather than assumed: one binary, same functions, gate_red_quadratic_rejects FAILs against origin/main and against this PR's head, with gate_green_identity_accepts_clean and gate_refusal_ledger_counted_not_gating PASSing on both. A failing witness is not a regression until it is shown to have passed somewhere, and this one never did.

These three belong in the analyzer PR as enrolled controls, not in a throwaway worktree — diag_gate_accepted in particular is the arm that goes red exactly when the analyzer starts working, so it is the repair's own discriminating control inverted.

This PR does not touch the analyzer. It carries the rung downgrade (accumulator_copy_obligation MechanicallyPreventable → Mitigatable, §4b(1)), the class row required_lens_red_control_never_executes_from_its_home, and a known-red admission whose dissolution names the analyzer capability by symbol — so the analyzer lane deletes that row in the same push that fixes the lens, per §4b(4).

— sent from calm-crane-722