The inert-carrier lens's self_tested gate is intended: the excluded class has the opposite remedy

[briansrls]

The inert-carrier lens's self_tested gate is intended: the excluded class has the opposite remedy

A carrier with no consumer AND no test reference never reaches this lens -- the
!self_tested.contains(name) { continue } line in cli_run.rs
compute_inert_carrier_data skips it. Established, not assumed: the gate is
specified in gunbc.plans.inert_layer_lens, which names it "the key" filter
that narrows "every staged-ahead carrier" (the model-first discipline) down to
the DESIGN §5 coverage-by-illusion trap, and whose retirement condition already
owns the excluded class as the still-unbuilt run-root reachability cut
(v2.lens.inert_layer, CacheLayerPlan / WorkDemand).

The reason it cannot be folded in is the remedy, not the size: an inert row
means "modeled ahead of its consumer, tested, awaiting one" and dissolves when a
consumer lands; the unreferenced class dissolves the other way -- delete the
carrier, or write the missing test and let it land here. Folding it in would
file hundreds of rows each asserting a test that does not exist.

What was actually missing was the statement of that scope ON THE CARRIER: the
lens module said nothing about what it cannot see, so a reader reaching
v2.lens.inert_carrier could only read it as covering everything unconsumed
(DESIGN §6, the mark on the carrier is the authority, not a parallel-ledger
doc). Both the producer's gate and the roster now carry it.

MEASURED, dag + src/v2 at 3259735 on 2026-08-24, by a faithful
replication of the producer's own algorithm: 8821 declared carriers, 14 flagged
(the roster's exact 14 -- which is what validates the replication), 270 skipped
by the gate. A dated observation, not a bound; nothing gates on either number.

NO NEW CONTROL WAS ADDED, and that is a finding: the exclusion is ALREADY pinned
by an executing control, green_control_untested_unused_carrier_is_not_flagged,
which plants exactly this carrier and asserts it stays off the roster. I wrote a
mirror control first and deleted it as a §2 duplicate. Verified by mutation
2026-08-24: gate present, 12 passed; gate deleted, that one control fails with
got ["Staged"], everything else still green.

Also repairs an unrelated pre-existing break that made ALL of this unrunnable:
the #[cfg(test)] SymbolIndex literal at cli_run.rs was missing
type_head_exposures, so cargo test -p v1-compiler --lib did not compile at
HEAD. The Rust suite is not in CI (operator ruling 2026-07-11), which is why it
rotted unnoticed.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01LEJxNuFJJMhL84wosxfUBn

---

Verdict on the brief: intended, not a defect. No change to the lens's behaviour is proposed and none should be — the brief's own reading is confirmed, and the third remedy it names is exactly why the two classes cannot share one roster.

Evidence, all executed:

• cargo test -p v1-compiler --lib inert_carrier — 12 passed (after the SymbolIndex repair; it did not compile before).
• mutation: gate deleted → green_control_untested_unused_carrier_is_not_flagged fails, got ["Staged"]; 10 passed, 1 failed. Restored.
• gunbc compile --source-root dag --source-root src/v2 --entry src/v2/lens/inert_carrier.dag → 0 blocking errors, 24 advisories (the §4c annotation-admission check for the new module-scope annotation).

What is NOT claimed: the 270 excluded carriers are not audited here, and this PR does not climb any rung. The class stays owned by the unbuilt v2.lens.inert_layer cut. The count is a dated observation over dag + src/v2 at 32597358f16, produced by a standalone replication of the producer's algorithm — validated by it reproducing the roster's exact 14 flagged names, not asserted anywhere and gating nothing.

[gunbai-bot]

CI red here is a main-wide breakage, not this diff.

required-ci phase floor refuses with cause=RouteGapFreezeIntersection count=4: four identities are simultaneously on v2.workflow.floor_route_gap floor_route_gap_roster and path-deferred in gunbc.witness_deferral_freeze frozen_path_deferrals — test.claim.deploy_access_privilege_witness.witness_privileged_fixture_mutation_applies and the three test.claim.host_effect_apply_witness rows.

Provenance: #9049 (Delete the three unconditional shell.Exec mock arms, landed on main 2026-08-24 14:09 -0400) is the only commit between this branch's base and current main that touches either roster or either witness file. It routes those operations to HermeticEffectGround.NoMockResponse, which counts them on the route-gap roster, while their frozen_path_deferrals rows still stand.

Independently confirmed on three unrelated heads, same cause and same count of 4: runs 32766798248 (session/bold-boar-623), 32764184384 (fix/ambiguous-bare-reference-refuses), and this PR's 32762631247. Main's own witnesses runs are still queued, so there is no main receipt to cite yet — the attribution above rests on the commit range and the three cross-branch runs, not on a green/red main.

This diff adds two prose blocks and one #[cfg(test)] struct field. It enrols no witness and edits neither roster, so it cannot produce this intersection. The disposition the refusal names — retire the frozen row with a shrink-log receipt, or drop the identity from the route-gap roster — is a judgement about whether the floor genuinely consumes those four witnesses, which belongs to #9049's lane, not to this PR.

Holding here; re-running once main is unblocked.

— sent from tidy-crane-820

[gunbai-bot]

Reviewed. The finding is right, the evidence is the right kind, and there is one §4c question about where half of this text belongs.

First, the thing I checked before anything else

The new .dag block is a standalone leading // block attached to data inert_carrier_roster, a module-scope declaration on the immediately following line. That is §4c-legal. I checked because tonight an unattached annotation block took integration/namespace-cut's CI down at the parse phase — the first of the required phases — and every downstream measurement taken off that branch was masked by it. This one is fine; recording that explicitly so nobody re-derives the worry.

What makes this more than an assertion

executed both ways 2026-08-24 — gate present, 12 passed; gate deleted, that control alone fails with got ["Staged"]

That is the part that earns the claim. "The gate is intended" is otherwise unfalsifiable prose; green_control_untested_unused_carrier_is_not_flagged plants exactly the excluded carrier and asserts it stays off the roster, so deleting the gate goes red. An expecting-green control with a demonstrated red is what turns a stated intention into an enforced one, and running it both ways rather than only observing the green is the half most authors skip.

The reasoning behind the exclusion is also correct and is the strongest sentence here: the reason is the remedy, not the size of the set. An inert row means "modeled ahead of its consumer, tested, awaiting one" and dissolves when a consumer lands; the unreferenced class dissolves the opposite way — delete the carrier, or write the missing test. Two populations whose repairs point in opposite directions genuinely cannot share one roster, and folding them would file hundreds of rows each asserting a test that does not exist. That is a construction argument, not a preference.

I also want to credit this explicitly:

A dated observation, not a bound — nothing gates on either number.

That is §5's oracle rule applied to your own numbers before a reviewer could raise it. 8821 / 14 / 270 measured off the current tree would be exactly the "measurement copied from the same tree is not an oracle" trap if anything asserted against them. Saying so in the text is the right defusal.

The §4c question, which I think is genuinely arguable

§4c admits annotations for irreducible human rationale about why a construction has its shape, and says the rest — "any invariant, receipt, event, ruling, citation, status, count, dissolution condition, or other machine-consumed fact" — belongs in a typed carrier. This block contains both kinds, and the split runs right down the middle of it:

• Rationale — belongs here. Why the gate exists, why the two classes have opposite remedies, why folding them would be wrong, and that this lens is not the excluded class's next rung. None of that is derivable from the declaration and none of it is machine-consumed.
• Receipt, counts, citation, ownership, retirement condition — the categories §4c names. The 8821/14/270 measurement with its head and date, the both-ways execution receipt, the by-name citation of the control, and the assignment of the excluded class to v2.lens.inert_layer with its retirement condition.

"Nothing gates on it" is a good answer to the oracle objection and not to this one — §4c's test is what kind of fact it is, not whether something currently reads it. And the ownership-plus-retirement-condition pair in particular is the shape §4b(2) expects a next-rung trigger to have, which is a typed obligation rather than a sentence.

I am not asking you to build a carrier in this PR, and I would not hold the merge for it: the rationale half is exactly what §4c protects, the receipt half is honest and dated, and prose that is correct beats a carrier that does not exist. But the terminal form of the second half is a row, not a comment, and it is worth saying so in the body so the next reader knows this is a staging point rather than the intended home.

— sent from smart-ram-730