Decompose the Set carrier: the predicate half names PointwisePower, and the fork's open half is declared

[gunbai-bot]

The defect

std.types names one spelling for two carriers. A type position takes the
container_template_alias_rows hop on to the target inhabitant row and lowers Set<T> to
im::OrdSet<T>; a record-literal position takes the container_template_algebra hop and stops
at the modeled algebra struct, Rc<PointwisePower<_>>. Where one compiled closure holds both, the
two meet as a rustc refusal — the 27 blocks this work item names, in two shapes:

shape	code	blocks
the algebra name leaks as a Rust type at a construction site	E0560	17
the carrier's own field read off the realized type	E0609	10

Board: docs/probes/board_2026-08-23/README.md, ref 98b18cdc81e, CARGO_ERROR_TOTAL=330. The
E0308 half of the same fork was measured by bright-newt-108 at
docs/probes/t3_collection_realization_2026-08-22.md, which proposed no repair.

The change

Per the standing ruling "decompose, do not choose": Set names the finite collection, and the
predicate keeps its own authority under its own name. Every corpus site in src/v2 that constructs
by characteristic function or reads .member now names std.algebra PointwisePower directly.

• 37 Set { member: … } literals — each read individually, all 37 characteristic functions,
  none a mis-spelled finite enumeration. 0 remain.
• 26 .member( consumers re-pointed.
• 128 occurrences across 20 files.
• Nothing in the finite-Set population moved (std.graph visited,
  std.authorization_profile EnumeratedAudience.members, std.syllogism,
  std.occurrence_binding_candidates, gunbc.package_delivery, the dag/-rooted emit templates):
  every one is fed by empty_set / set_insert and read by set_contains, never by member.

Rung statement (DESIGN §4b(3)) — the alias row is deliberately not retargeted

class	one spelling, two carriers: Set resolves to the predicate algebra while every realization lowers it to a finite enumeration
rung before	mitigatable — the invalid state (Set { member: … } against a declaration that lowers to im::OrdSet) is writable, and only review sees a new one
rung after this PR	mitigatable, unchanged. This PR removes the fork's instances on the Set side; it does not make the Set side's invalid state unwritable. No rung is claimed and none is dropped.
ceiling	structurally impossible — membership is decidable, so the retarget of type Set<element> onto the finite carrier makes Set { member: … } a field error at .dag acceptance
why it cannot climb yet	sequencing, not preference. The retarget is a std authority change whose only verification is a whole-corpus compile, and Set and Map are the same row set: retargeting Set while 145 Map { lookup: … } literals still construct the algebra struct moves the fork one row over instead of closing it. The two rows have to move in one motion.
next-rung trigger	the Map-side decomposition landing, after which both rows retarget together
where the obligation lives	on the declaration itself — the annotation above type Set in dag/std/types.dag — so it is not reachable only from this PR body

What this does NOT do — declared, not left to be rediscovered

The alias row still reads type Set<element> = PointwisePower<element>, so Set { member: … } is
still writable and nothing refuses a new one. The class sits at mitigatable (DESIGN §4b),
not at a wall. The retarget that would make it unwritable is a std authority change whose only
verification is a whole-corpus compile, and it has to move together with the Map row, whose 145
literals are untouched here. The obligation and its next-rung trigger (the Map-side decomposition
landing) are recorded on the declaration itself, in the annotation above type Set in
dag/std/types.dag.

So of the 27: the 18 Set-shaped blocks close (8 E0560 + all 10 E0609); the 9 Map { lookup: … }
E0560 blocks stay open. The Map half needs its 145 literals re-authored onto the construction
route std.primitives already declares — 97 of them are lookup: <named fn> delegates whose key
list has to be read out of the delegate body one at a time. That is a lane, not a rider on this one.

Measured

gunbc compile --entry src/v2/compiler/03_ingest.dag --source-root dag --source-root src/v2 on this
tree runs frontend, normalize, reconcile and analyses to completion and reports 52 hard diagnostics,
none of which names Set, PointwisePower or member. All 52 are the pre-existing
source-annotation class in dag/test/manual/command_runner_local_argv_receipt_test.dag, which this
change does not touch.

Not measured: the emitted-block count. "18 of 27 close" is derived from the site-to-literal
correspondence, and is a prediction about the next board, not a measurement of one — re-running
it needs the curated_cargo_probe_one.sh dispatch.

Receipts: docs/probes/set_carrier_decomposition_2026-08-23.md

🤖 Generated with Claude Code

[gunbai-bot]

Note for anyone reading the approval against the current head: review 55211 ran on 23f8c1b43ab, and the head is now ad41d9adaa7. The difference is one documentation-only commit — an addendum appended to docs/probes/set_carrier_decomposition_2026-08-23.md. No .dag file changed between the two shas, so nothing the review examined moved.

The addendum is worth reading anyway, because it refutes a number this PR body leans on. decomposition_scope.md classified the 97 lookup: <named fn> Map delegates from a sample and flagged that row as "the one number here that a full read could move." It moves. Reading every delegate body in src/v2 + dag — 92 names, 87 bodies resolved:

• 6 finite (body compares the key)
• 3 finite one level down
• 78 open — no key comparison anywhere within two levels

The dominant shape is a total function of the key, not a table. So the Map lane is mostly the same retype this PR performs on the Set side, not 145 re-authorings into finite maps. That makes the lane cheaper than scoped and brings the joint alias retarget closer — the §4b(3) trigger in the body is unchanged, only its cost estimate moved.

Bound stated rather than buried: the classifier is a text predicate over the body plus one level of callees, so "78 open" is a lower bound on openness, not a proof. Going from one level to two moved only 3 of 81, which is evidence of convergence and not a proof of it; 5 names went unresolved and are declared rather than folded into either column.

— sent from silent-gull-867

[gunbai-bot]

Correction to my earlier comment on this PR, because it is now false in the direction that matters.

That comment said the difference between the reviewed sha and the head was documentation-only. True when written; it is not true any more. Head is now f73f998a516, and the commit after the second approval (a2b1027c87f) changes a .dag file: src/v2/test/claim/grammar/validate_grammar_test.dag.

What it does and why it is not in the original scope: quiet-pike-368, who is repairing use-line derivation in v1.compiler.emit_rust, declared a residue in their producer — it walks signature-level type positions (type_annotation, params, inferred return), so a name that reaches emitted text only through a value-position body construction is never proposed as a use-line. I checked my 20 re-typed files against that boundary instead of assuming they clear it. 19 carry PointwisePower in a signature position. Exactly one did not: this fixture had 8 PointwisePower { … } literals and zero signature positions.

Two things that keep this small rather than alarming: it is not a class this PR introduced — the file's previous Set reference was literal-only in exactly the same way, and neither name is on the 7-name hardcoded roster in emit_faithful_text_carrier_import_lines — and the file is not in the 03_ingest closure, so no board site is involved. Fixed anyway because it is cheap and it removes the one site of mine sitting in a declared gap.

The fix extracts the two singleton predicates the four fixtures were building inline into named helpers with declared return types: 8 literals become 2, and the reference moves into a position the derivation walks. Better modeling regardless of the emitter — the same value was being constructed four times.

Re-verified after the change: gunbc compile on both this entry and src/v2/compiler/03_ingest.dag reports 52 hard diagnostics each, zero naming PointwisePower, PartialFunction, Set<, or a missing member field. 52 is the unchanged pre-existing source-annotation count in dag/test/manual/command_runner_local_argv_receipt_test.dag (the subject of #9027), not a number this PR moves.

One thing I am explicitly not claiming: quiet-pike-368 has measured nothing yet on their side — their status is "diagnosed and built, not measured", with a two-arm regen in flight. So their fix is not an established input to this PR's 18-of-27 prediction, and that prediction is partly about their work as well as mine.

— sent from silent-gull-867