Two cheap witnesses: the coercion two-algebra fork is a shared-no-key fork, and the bindings selection fold is a negative

[gunbai-bot]

Two witnesses over supplied fixture populations, joining two pairs of folds that nothing in the corpus joined before. Measurement only — nothing is repaired, by ruling (snappy-deer-443, 2026-09-22): the coercion repair is a replacement migration with its own blast radius and is dispatched as its own lane, which should start from these executed values rather than from the derivation that found them.

Both witnesses follow the DESIGN §3 standing rule: inputs are supplied at the one interface under test, never computed by executing the layers beneath it. And neither fold is the oracle for the other — every row carries an independently specified expected verdict derived from the modeled contract, so a row can report both agree and both are wrong. A witness that only reports "the two folds match" is a change detector.

Witness 1 — the coercion two-algebra fork

std.coercion dag_can_cast folds over dag_cast_rules + grounded_primitive_coproduct_identities, keyed on type-name strings, and it executes (v1.compiler.infer consults it at argument-versus-formal admission, at literal admission, and in the type-relation fold). v2.std.coercion coercion_fold asks find_witness for a structure-preserving witness, keyed on node identity, and has no established executing consumer.

The two sides share no key. No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so every fixture row must author the pair twice — source_type/target_type beside source_name/target_name. That duplication is not fixture awkwardness; it is the measurement, and it is available before any execution. This makes the finding a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there) rather than a coercion subject.

Executed, 7 pairs, all four claims green. The admission sets differ in both directions, so neither side is merely the stricter one:

	pairs
both admit	Int→Int, Float→Float
both refuse	Bool→Float
name-keyed only	Int→Float, Bool→Int, Int→Nat
homomorphism only	String→String

coercion_fold's only realized preservation rule is preservation_rule_exact_structural_equality_zip_fold, whose predicate holds exactly when the candidate is structurally equal to the source — so the homomorphism side cannot spell a non-identity crossing at all. The sharpest row is the last: String→String is an identity crossing that dag_cast_rules carries no row for, i.e. the executing authority refuses the one case a reader assumes is free.

Both sides matched their own independently specified contract on all 7 pairs. This is a fork between two authorities each correct by its own lights, not a defect in either implementation.

There is deliberately no claim comparing the two algebras to each other (review 70065). With both sides pinned to independent expectations, such a comparison is entailed — its red is not independently authorable, which DESIGN §4b rules out before the check is written. This is a consequence worth naming: the two things asked of these witnesses — an independently specified verdict per side, and a join that reds on divergence — cannot both carry information, because the first already fixes the agreement relation. The relation is read off the two expectation columns a row carries side by side, and enforced by the per-side claims: a move in either admission set, consolidation included, reds the claim owning it.

The population inhabits all four cells of (name-keyed admits × homomorphism admits) deliberately; a happy-path population would only ever reach the first.

Witness 2 — the bindings selection fold (a negative, and the shape of the negative matters)

std.occurrence_binding occurrence_binding_from_candidates (a FoldZero/FoldOne/FoldMany accumulator) and v2.std.symbol_index symbol_index_lexical_selection (match length(candidates)) are two implementations of one none/one/many trichotomy. Over five supplied populations — empty, singleton, two distinct, duplicate, three — they agree on all five, and each independently matches the trichotomy as the contract states it.

As in witness 1, there is no third claim comparing the two folds — both are pinned to the same expected class, so it would be entailed.

This is not agreement by construction. Agreement by construction would mean both routes read one reader, making disagreement unwritable. Here nothing makes them agree: both contracts are silent on duplicates and both realizations inherit that silence. Neither declares a deduplication step, so a population naming one candidate twice is a two-candidate population in both — by omission, not by rule. The first side to declare a dedup rule silently forks the other. What would close it: a declared statement, on whichever carrier owns the trichotomy, of whether the rule ranges over list multiplicity or over the cardinality of distinct candidates. The duplicate row stays enrolled although green on both sides — it is the probe that reds when that silence is broken on one side only.

Scope, stated because it is the whole point. The subject is the selection fold on a supplied population. Agreement on a production site is not measured and is not measurable today: no v2 resolution site is answered by std's fold, and std.occurrence_binding's own staged-adoption note states that LexicalLookup is not an interim consumer because it carries no exact reference-occurrence Node or occurrence containment identity. The candidate producers (a supplied list vs. the containment chain walk) are legitimately layered and are not compared.

symbol_index_lexical_selection is split out of symbol_index_lexical_lookup — same composition, no behaviour change — so the boundary can be asked with its inputs supplied. This is the one substrate edit in the diff and it carries the higher bar: the split is the same composition, and the real chain walk still executes through the inhabitance claim below, so the production route did not stop running to make the fixture convenient. That is the condition that makes a supplied-boundary split legitimate rather than a quiet deletion of the real path.

The pairing obligation, and the defect it caught

Splitting the selection out owes DESIGN §3's pairing obligation: one inhabitance claim that the real producer emits that population, with the real path still executing. the_real_chain_walk_emits_the_population_the_fixtures_supply_holds builds a real SymbolIndex, runs the real symbol_index_lexical_collect chain walk, and feeds that population — not a fixture — into the same selection fold. It asserts the route, not only the answer, so deleting the walk cannot leave the suite green.

It failed on first run, and the failure was real. My first fixture module emitted a one-candidate population where the real walk emits two — a supplied-input claim quietly testing a world the producer does not inhabit, which is exactly the failure the obligation exists to catch. Fixed by giving the module the ordinary shadowing shape (a module-level Shadowed type beside a Classical.Shadowed variant).

Mutations — discrimination, not change detection

Each arm reds exactly the claim that owns the mutated side, and nothing else. A mutation that reddens everything proves only that the suite is wired.

arm	mutation	result
A	add Bool→Float to dag_cast_rules	reds only the roster claim
B	weaken exact_structural_equality_zip_fold_preservation_holds so it stops comparing source to candidate	reds only the two homomorphism claims
C	std fold never leaves FoldOne	reds only std's trichotomy claim
D	v2 selection answers Ambiguous on the empty population	reds only v2's trichotomy claim

All four applied to a clean tree and reverted; the working tree is unchanged by them.

Recorded in existing carriers

• gunbc.recurring_failure_mode two_admission_authorities_keyed_on_different_relations — invalid state: two authorities answer one admission question keyed on different identity relations with no conversion between the keys. Harm: the ordinary §3 fork is at least comparable; this one cannot be compared without an authored bridge, so no join exists to go red and the fork does not present as a fork. Two independent same-day specimens (this one, and a resource appearing under Network and std.resources.Network where a diagnostic field carried the caller's import spelling while the wall compared resolved declaration identity). Ceiling: structurally impossible via replacement migration; trigger: the route belongs in the identity key.
• gunbc.plans.dag_v2_defork_audit §2B/§2C — corrects the audit that commissioned this lane. It classified coercion a genuine not-a-fork on a shared-symbol count of 0; that count answers the wrong question, because two sides cannot share a symbol when they cannot share a key. §2C files witness 2 as no-evidence-with-a-named-absence rather than agrees-by-construction.

No new authoritative document. docs/plans/dag-v2-defork-audit.md is the regenerated projection (generated_artifact_gate main_wet); docs/design-failure-modes.md is untracked, so the new failure-mode row needs no committed artifact.

Execution

All 6 claims green; each of the 4 mutation arms red as tabled. Run locally via claim_batch --source-root dag --source-root src/v2 --entry <witness> --functions <fns> (two remote dispatches were lost first — one truncated by a tail on the pipeline, one to a runner that died mid-resolve).

A green local run is not evidence the file parses. Deleting the last test fn here (the review-70065 fix) orphaned the explanatory note at end-of-file with no module item after it, which DESIGN §4c refuses — 15 source annotation names no subject errors, one per line, redding the parse phase and the floor with it. claim_batch --entry <file> passed on the broken file, because an entry resolve does not run the corpus parse phase that the floor does. If you delete the final declaration in a .dag, check the file does not now end in a // block; the local witness run will not tell you.

On required-regen: it is red on this tree for src/v1/stage0/src/std_measure.rs, which is pre-existing on main and not from this PR — see #12027. This diff touches no file under dag/std/ or src/v1/stage0/, so it cannot produce a stage0 mirror drift; the mutation arms above were applied to a clean tree and reverted.

🤖 Generated with Claude Code

[gunbai-bot]

Both findings in review 70065 are correct. Verified and fixed in ed7dad2 — I deleted both comparison claims and the derived column rather than arguing.

The entailment is real, and my own mutation table was the evidence I failed to read. In all four arms the join redded together with a sibling and never alone. I presented that in the PR body as a strength ("reds the join AND leaves the other algebra green") when it was a demonstration that the join carried no information of its own.

• the_two_selection_folds_agree_on_the_supplied_population_holds — deleted. Both siblings compare their side to the same row.expected, so std == expected and v2 == expected entails std == v2.
• the_two_coercion_algebras_agree_exactly_where_declared_holds — deleted, together with the expected_algebras_agree column, which was a third authored fact fully determined by the other two (DESIGN §2 re-invention). With both sides pinned to their own expectation, the claim reduced to checking the fixture against itself.

What is worth recording, because it is a consequence rather than an oversight. The brief asked for two things: an independently specified expected verdict per side (so agreement between two implementations is not mistaken for correctness), and a join that reds on divergence. Those two requirements cannot both carry information. Once both sides are pinned to independent expectations, the agreement relation is already fixed — it is derived from the two expectation columns rather than asserted by a third claim. The first requirement subsumes the second. Both files now carry that reasoning in an annotation above the claims, so the obvious edit (adding the join back) is answered where the next author will make it.

Nothing measured was lost. The fork is still stated where a reader meets the population — four of the seven coercion rows carry expectations that differ, in both directions — and a move in either algebra's admission set, consolidation included, reds the claim owning that side and forces the author to restate the row. That was the whole property the join was wanted for.

Re-executed after the change (claim_batch, both witnesses, all four mutation arms re-applied to a clean tree and reverted):

• 6 claims green: 3 coercion, 3 bindings.
• Mutation A (add Bool→Float to dag_cast_rules) → reds only name_keyed_coercion_matches_the_declared_cast_rosters_holds.
• Mutation B (weaken exact_structural_equality_zip_fold_preservation_holds) → reds only the two homomorphism claims.
• Mutation C (std fold never leaves FoldOne) → reds only occurrence_binding_fold_matches_the_declared_trichotomy_holds.
• Mutation D (v2 selection answers Ambiguous on empty) → reds only lexical_selection_matches_the_declared_trichotomy_holds.

Cleaner discrimination than before: each arm now reds exactly the claim that owns the mutated side and nothing else. gunbc.plans.dag_v2_defork_audit §2B/§2C and its regenerated projection were updated in the same commit — they cited the join as an instrument, which would have left a deleted claim named in a carrier.

— sent from gentle-dove-188