Coercion fork fixture follows #12227: Bool->Int is now refused by both algebras

dag/gunbc/plans/dag_v2_defork_audit.dag

@@ -78,7 +78,7 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
     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 three decision points -- `kernel_value_declared_type_mismatch_bounded`, `application_type_names_compatible` and `validate_cast` (explicit `as`)). `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: "**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`, `Int→Nat` — and `Bool→Int` at #12055, until #12227 withdrew its row (a `Bool` is not an `Int`), after which both sides refuse it and the fixture keeps it as the control that the withdrawal holds. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That cell is a property of the RAW HELPER roster, not a production refusal: every live composition in `v1.compiler.infer` admits name identity before it consults `dag_cast_rules`. Both sides matched their OWN declared 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,

dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag

@@ -13,7 +13,7 @@ data two_admission_authorities_keyed_on_different_relations: RecurringFailureMod
 
     "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 three decision points -- kernel_value_declared_type_mismatch_bounded, application_type_names_compatible and validate_cast (explicit `as`). 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. That last cell is a property of the RAW HELPER roster, not of production: every live composition in v1.compiler.infer (kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast) admits name identity before consulting dag_can_cast, so the compiler does not refuse an identity crossing. What the specimen establishes is two admission contracts on disjoint keys, not a production refusal.",
+    "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 three decision points -- kernel_value_declared_type_mismatch_bounded, application_type_names_compatible and validate_cast (explicit `as`). 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 were admitted name-only (Bool->Int left the name-keyed roster in #12227), while String->String -- an IDENTITY crossing -- is admitted homomorphism-only, because dag_cast_rules carries no identity row for it. That last cell is a property of the RAW HELPER roster, not of production: every live composition in v1.compiler.infer (kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast) admits name identity before consulting dag_can_cast, so the compiler does not refuse an identity crossing. What the specimen establishes is two admission contracts on disjoint keys, not a production refusal.",
 
     "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.",
 

dag/gunbc/representation_boundary.dag

@@ -311,7 +311,7 @@ data coercions_boundary: RepresentationBoundary = RepresentationBoundary {
   crossing_evidence: InterpretedOnly {
     what_goes_red: "the identity-keyed half is a real climb with a receipt: passing the empty string once meant identity-unknown, and eight reference sites doing so rendered dag/std/integer.dag aliases as crate::std_nat::Nat instead of i64. There is now no empty string to pass -- an absent identity is DeclarationIdentityAbsent, and the degraded answer is stamped GroundedByUnidentifiedBareRow so it stays countable rather than silent." as NonEmptyStr,
     blocked_on_a_two_route_oracle: "THE FORK ITSELF. No execution joins the cast table to the homomorphism fold, so if they disagreed today nothing would go red. That is the finding, and it is why this row is not recorded as DEFERRED: a fork whose disposition reads as adjudicated is worse than an unrecorded one, and this fork stayed invisible precisely because the census that holds it asked whether the two modules SHARE TYPE NAMES -- see the scope note on gunbc.plans.dag_v2_defork_audit, whose coercion row answers a resolver-collision question and not this one." as NonEmptyStr,
-    unbuilt_but_testable_now: "BUILT (#12055, v2.test.claim.coercion.two_algebra_fork), and it measures the two HELPER CONTRACTS, not the production judgments. Seven supplied pairs reach dag_can_cast and coercion_fold directly, each held to an expectation transcribed from ITS OWN declaration: Int to Float, Bool to Int and Int to Nat are admitted name-only, String to String homomorphism-only. WHAT IT DOES NOT ESTABLISH, TWO THINGS. First, no independent semantic oracle: each column restates its own side, so the agree-and-both-wrong arm is still unreportable. Second, no production refusal: every live composition -- kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast -- admits name identity BEFORE consulting dag_can_cast, so the String to String cell is a property of the raw helper roster and not an identity crossing the compiler refuses. What remains unbuilt and climbable is the context matrix named on the trigger." as String
+    unbuilt_but_testable_now: "BUILT (#12055, v2.test.claim.coercion.two_algebra_fork), and it measures the two HELPER CONTRACTS, not the production judgments. Seven supplied pairs reach dag_can_cast and coercion_fold directly, each held to an expectation transcribed from ITS OWN declaration: Int to Float and Int to Nat are admitted name-only (Bool to Int was too, until #12227 withdrew the row), String to String homomorphism-only. WHAT IT DOES NOT ESTABLISH, TWO THINGS. First, no independent semantic oracle: each column restates its own side, so the agree-and-both-wrong arm is still unreportable. Second, no production refusal: every live composition -- kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast -- admits name identity BEFORE consulting dag_can_cast, so the String to String cell is a property of the raw helper roster and not an identity crossing the compiler refuses. What remains unbuilt and climbable is the context matrix named on the trigger." as String
   },
   next_trigger: climbs_when(capability: "every consumer of the shared name-pair cast rosters asks ITS OWN judgment through that judgment's one authority, SUFFICIENT FOR dag_can_cast, dag_cast_rules and is_dag_cast_domain_type to have no remaining decision-making caller and be deleted or derived, and for the per-target CastSyntax cast_rules to be consumed by target realization rather than re-deciding legality. THE ROSTER IS NOT ONE QUESTION WITH ONE REPLACEMENT HOME: it is consulted inside declared-type compatibility (v1.compiler.infer kernel_value_declared_type_mismatch and application_type_names_compatible) and inside explicit `as` validation (validate_cast), while v1.compiler.coercion can_cast and the emitter's cast arm read a SEPARATE per-target roster. Literal introduction at a structural destination is already owned by std.literal_elaboration, and Int to Nat is already split between that literal homomorphism and a proof-requiring refinement cast (refinement_cast_rules); neither is a widening. So the homes are expected to be several -- declared-type inhabitance, literal elaboration, an explicit-conversion judgment, target realization -- and naming one fold here, v2.std.coercion coercion_fold or v2.std.inhabitance alike, would be an over-broad home that repointing callers could satisfy while a question stayed forked. The prerequisite is a consumer-by-judgment partition with context-discriminating probes (literal, arbitrary value at a formal, explicit cast, emitted) per admitted pair; if it shows several questions, this row is split per judgment rather than retired whole. Deleting the v1 seed does not fire this: four extdeps language types modules author per-target cast rows and survive v1.")
 }

docs/plans/dag-v2-defork-audit.md

@@ -110,7 +110,7 @@ Three tiers. **Mirror** = v2's used symbols ⊆ dag → mechanical delete + repo
 
 **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).
 
-**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.
+**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`, `Int→Nat` — and `Bool→Int` at #12055, until #12227 withdrew its row (a `Bool` is not an `Int`), after which both sides refuse it and the fixture keeps it as the control that the withdrawal holds. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That cell is a property of the RAW HELPER roster, not a production refusal: every live composition in `v1.compiler.infer` admits name identity before it consults `dag_cast_rules`. Both sides matched their OWN declared 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.
 
 **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.