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

dag/gunbc/plans/dag_v2_defork_audit.dag

@@ -72,6 +72,17 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
         row(cells: [cell(text: "**node**"), cell(text: "**0**"), cell(text: "dag = `compiler_inductive_fields`/`compiler_recursive_types`/`is_compiler_recursive_type` — the complexity analyzer's inductive-structure *authority* (instance of `std/induction.dag`); v2 = 126-decl, 506-importer real Node substrate"), cell(text: "dag side imported by `src/v1/04_infer.dag`, emitted to `src/v1/stage0/src/std_node.rs`, guarded by `src/v1/tests/src/source_audit.rs`; `compiler_inductive_fields` is consumed **only by v1, never v2**"), cell(text: "**DEFERRED — self-dissolves.** Since `compiler_inductive_fields` is v1-only, on v1-delete `dag/std/node.dag` goes **dead → delete it, collision gone, no rename needed at all.** It is a live v1-only authority today (not a dead imposter); the collision with the v2 substrate is a v1-existence artifact.")]),
       ],
     },
+    h3(text: "2B. 2026-09-22 executed correction to the `coercion` row — shared-symbol-count 0 was the wrong discriminator"),
+    p(text: "**This audit classified `coercion` as a genuine not-a-fork on a shared *symbol* count of 0. Measured by execution, that count answers the wrong question.** The two modules share no symbol and denote no different concept: they answer ONE question — may this value cross from one model to another — and they answer it with **two admission authorities keyed on different identity relations**. `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 `v2.std.find_witness` `find_witness` for a structure-preserving witness, keyed on node **IDENTITY**, and has **no established executing consumer**. A shared-symbol count cannot see this, because the two sides cannot share a symbol: they cannot share a KEY."),
+    p(text: "**The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity)."),
+    p(text: "**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `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. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either."),
+    p(text: "**NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all."),
+    p(text: "**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`. Each pins ONE algebra to its OWN independently specified contract, so a move in either side's admission set — consolidation included — reds the claim that owns it and the author must restate the row. **There is deliberately no fourth claim comparing the two algebras to each other** (review 70065): with both sides pinned to independent expectations, such a comparison is ENTAILED and its RED is not independently authorable, which DESIGN §4b rules out before the check is written. The agreement relation is DERIVED from the two expectation columns a row carries side by side. Two mutation arms establish discrimination rather than change detection: adding a `Bool→Float` row to `dag_cast_rules` reds ONLY the roster claim, and weakening the structural-preservation predicate reds ONLY the two homomorphism claims."),
+    ThematicBreak,
+    h3(text: "2C. 2026-09-22 — the bindings selection fold is a NEGATIVE, and the shape of the negative matters"),
+    p(text: "`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. Measured over five supplied populations — empty, singleton, two distinct, **duplicate**, three — **they agree on all five, and each independently matches the trichotomy as the modeled contract states it**, so this is not merely \"the two match\"."),
+    p(text: "**It is NOT agreement by construction, and the distinction is load-bearing.** 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. In inventory terms this is **no-evidence with a named absence**, not AgreesByConstruction. **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 it is green on both sides — it is the probe that reds when that silence is broken on one side only."),
+    p(text: "**SCOPE, stated because it is the whole point.** The subject is the selection fold on a SUPPLIED population. Their 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 versus the containment chain walk) are legitimately layered and are not compared. `symbol_index_lexical_selection` was split out of `symbol_index_lexical_lookup` — same composition, no behaviour change — so the boundary can be asked with its inputs supplied (DESIGN §3, the witness standing rule); the split's pairing obligation is discharged by `the_real_chain_walk_emits_the_population_the_fixtures_supply_holds`, which runs the real `symbol_index_lexical_collect` walk over a real `SymbolIndex` and feeds THAT population into the same selection fold, so deleting the walk cannot leave the suite green. Mutation arms, each redding ONLY the claim that owns the mutated side: collapsing std's fold so it never leaves `FoldOne` reds std's claim alone; making v2's selection answer `Ambiguous` on the empty population reds v2's claim alone. As in §2B there is no third claim comparing the two folds — it would be entailed by these two, both being pinned to the same expected class."),
     h3(text: "Grounding cluster (operator authority) — 7 concepts, a unification *design*"),
     p(text: "Each row is **operator decision-input**: what is shared (and whether the shared body itself diverges), what each side uniquely carries, and the specific grounding entanglement that makes it a design, not a repoint."),
     TableBlock {

dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag

@@ -0,0 +1,30 @@
+module gunbc.recurring_failure_mode.two_admission_authorities_keyed_on_different_relations
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data two_admission_authorities_keyed_on_different_relations: RecurringFailureMode = RecurringFailureMode {
+  identity: "two_admission_authorities_keyed_on_different_relations" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: two authorities answer one admission question -- may this value cross from one model to another -- and each is keyed on a DIFFERENT IDENTITY RELATION, with no conversion between the two keys anywhere in the corpus.",
+
+    "HARM: the ordinary single-authority fork (DESIGN section 3) is at least comparable -- two answers to one question, so a join can be written and a disagreement can be made to refuse. This class is worse in a way that hides it: the two answers cannot be compared AT ALL without an authored bridge, so no join exists to go red, no census counts the divergence, and the fork does not present as a fork. It presents as two unrelated modules. The cost is paid at consolidation, when the bridge must be authored anyway and every decision taken in the meantime was premised on whichever key the local caller happened to hold.",
+
+    "DISTINGUISHING FACTS, and the first is the recognition rule: A FIXTURE THAT WANTS TO ASK BOTH AUTHORITIES ABOUT ONE SUBJECT MUST AUTHOR THE SUBJECT TWICE. That is not fixture awkwardness -- it IS the measurement, and it is available before any execution. Further tells: the two admission sets differ in BOTH directions, so neither authority is merely the stricter one and the comfortable reading is unavailable; and one side's key is a SPELLING while the other's is a resolved structural identity.",
+
+    "SPECIMEN 1 (gunbc, 2026-09-22, v2.test.claim.coercion.two_algebra_fork). std.coercion dag_can_cast folds over dag_cast_rules and 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 v2.std.find_witness find_witness for a structure-preserving witness, keyed on NODE IDENTITY, and it has no established executing consumer. Measured over seven supplied pairs, the admission sets differ in both directions: Int->Float, Bool->Int and Int->Nat are admitted name-only, while String->String -- an IDENTITY crossing -- is admitted homomorphism-only, because dag_cast_rules carries no identity row for it. The sharpest single fact is that last one: the case everyone assumes is free is the case the executing authority refuses.",
+
+    "SPECIMEN 2 (gunbc, 2026-09-22, smart-tern-891, a different surface and an independent sighting). One resource appeared under two labels, Network and std.resources.Network, because a diagnostic field carried the caller's IMPORT SPELLING while the wall itself compared through the resolved declaration identity. Correct by identity in one place, keyed by spelling in another, and only the second was load-bearing for the new consumer. Two independent sightings on one day is what makes this a class rather than a fact about coercion.",
+
+    "RUNG FOUND AT: below the ladder for the divergence itself -- nothing refuses, nothing counts it, and each authority answers confidently within its own key. The coercion specimen is now MITIGATABLE at the measurement grain only: v2.test.claim.coercion.two_algebra_fork pins the admission relation pair by pair over a supplied population, so a change to either side's admission set reds a claim. That is a wall around the MEASUREMENT, not around the state.",
+
+    "CEILING: structurally impossible, and the derivation is ordinary rather than aspirational. Admission over a key relation is decidable and fully modeled, so one authority keyed on one relation makes the divergent state unwritable -- there is no second admission set to diverge from. The ceiling is reached by a replacement migration (DESIGN section 3, replacement migrations cut over at the root), not by a check: one key wins, the other algebra is cut at its root, and the surviving authority carries every refusal the cut one carried.",
+
+    "NEXT TRIGGER: the route belongs in the identity key. Concretely, an admission authority whose key is a resolved declaration identity rather than a spelling, and one conversion or one deletion -- not a bridge kept standing, which would be a third authority. The measurement lands first deliberately: the repair is a replacement migration with its own blast radius, and it should start from executed values rather than from the derivation that found them.",
+
+    "WHAT IS NOT CLAIMED: no wrong compiled output is attributed to the coercion specimen. The homomorphism side has no executing consumer, so the divergence has had no opportunity to produce one. The class is filed on the STATE SPACE -- two admission authorities that cannot be compared -- and a class that has produced no incident is the one that will otherwise be found last.",
+  ],
+
+  evidence: [],
+}