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

[gunbai-bot]

Repurposed. This PR originally deleted the Bool→Int cast row itself. #12227 landed the same cut first (a Bool → Bool identity row keeps Bool in the explicit-cast domain, so validate_cast refuses b as Int instead of abstaining). The merge of main therefore takes main's version of std.coercion, the stage0 mirror, the interpreter comment and the failure-mode row in full. My declared-domain variant is dropped, and nothing of it remains in the diff.

What remains is the fallout #12227 left behind:

• v2.test.claim.coercion.two_algebra_fork still expected dag_can_cast(Bool, Int) to be admitted, so name_keyed_coercion_matches_the_declared_cast_rosters_holds asserted a row that no longer exists. bool_to_int now expects CrossingRefused on both sides. It stays in the fixture as the control that the withdrawal holds. The population comment and the three-of-seven count are updated to match.
• The coercions_boundary evidence and the two_admission_authorities_keyed_on_different_relations specimen (both from Coercion ledgers: truth-only repair after #12055; DESIGN §4 records the coercion ruling #12332 / Two cheap witnesses: the coercion two-algebra fork is a shared-no-key fork, and the bindings selection fold is a negative #12055) listed Bool→Int as admitted name-only. They now record it as withdrawn by Int->Nat refinement PR1: subtraction leaves Nat, count/length return Nat, Bool as Int refused by the checker #12227.

No behaviour change.

🤖 Generated with Claude Code

[gunbai-bot]

Stage0 mirror std_coercion.rs is now committed, taken verbatim from a remote claim_executor --required-regen candidate: the Bool row is gone, dag_cast_domain_types is added, and is_dag_cast_domain_type reads it. Without it, the PR floor would have run the old seed and shown no change. Marking ready so the floor produces the census. The PR's purpose is unchanged: every refusal is a dependent site to classify, not a reason to restore the row.

— sent from silent-swift-419

[gunbai-bot]

Addressed review 71551 in 4a9523e. Both findings were confirmed against the tree.

1. the_checker_admits_a_cast_the_evaluator_refuses still listed Bool as Int as residue, and the hand-authored comment in v1_interpreter.rs still said dag_cast_rules admits it. That specimen is now closed: with the row gone and Bool kept in dag_cast_domain_types, validate_cast refuses it at compile time, so the checker and the evaluator agree. The row now records that. Its remaining residue, casts outside the declared domain and the implicit Int to Nat identity, is unchanged, and so is its trigger, which still describes the open capability. The interpreter comment is updated to match.
2. The ruling citation pointed at DESIGN §4 on main, where the ruling hasn't landed yet: it lands with Coercion ledgers: truth-only repair after #12055; DESIGN §4 records the coercion ruling #12332. It now cites the operator ruling of 2026-09-26 through gunbc#12332, which resolves today and still resolves after that PR merges.

— sent from silent-swift-419

[briansrls]

HOLD at f9d82dc875633efc1ff106e850693db8769f3b4b.

The mechanical change is right: main's dag_cast_rules now carries Bool -> Bool and no Bool -> Int, the fixture correctly changes bool_to_int.expected_name_keyed to CrossingRefused, all four matrix cells remain inhabited, and the differing-row count is now 3/7.

Two truth-maintenance gaps remain:

1. dag/gunbc/plans/dag_v2_defork_audit.dag §2B still publishes the current executed result as Admitted name-only: Int→Float, Bool→Int, Int→Nat, and its generated projection docs/plans/dag-v2-defork-audit.md repeats it. This PR updates the fixture, the representation-boundary row and the RFM specimen, but leaves the plan authority and projection contradicting them. Update both—ideally preserving the #12055 historical reading while stating that #12227 withdrew the Bool→Int cell.

2. src/v2/test/claim/coercion/two_algebra_fork_test.dag still says a row can report “BOTH AGREE AND BOTH ARE WRONG.” The updated coercions_boundary correctly says the opposite: each expected column restates its own authority, so without an independent semantic oracle the agree-and-both-semantically-wrong arm is unreportable. Rewrite the fixture header to distinguish “both implementations deviate from their own declared contracts” from “both authorities agree but the shared semantic answer is wrong.”

Required floor, clippy, compiler and the aggregate witnesses job are green at this head; emit-build was still running when reviewed. These findings are about the PR's stated truth-only completeness, not runtime behavior.

[gunbai-bot]

Addressed GitHub review 5327152632 in 43c5fc7. Both points were confirmed.

1. gunbc.plans.dag_v2_defork_audit and its docs/plans/dag-v2-defork-audit.md projection still listed Bool→Int as admitted name-only. Both now keep the Two cheap witnesses: the coercion two-algebra fork is a shared-no-key fork, and the bindings selection fold is a negative #12055 result and record Int->Nat refinement PR1: subtraction leaves Nat, count/length return Nat, Bool as Int refused by the checker #12227's withdrawal. That same paragraph also still called the String→String cell a case the executing authority refuses, which is the production overclaim Coercion ledgers: truth-only repair after #12055; DESIGN §4 records the coercion ruling #12332 corrected elsewhere, so it now says it is a raw-helper property. It also said "independently specified", which is now "own declared".
2. The fixture header claimed it could report both agree and both are wrong. It can't: each column is transcribed from its own algebra, so there is no independent oracle. The header now makes only the narrower claim and points to coercions_boundary, which records the same limit.

— sent from silent-swift-419

[briansrls]

APPROVE at exact head 43c5fc7a4d67c4656b15ce6e7588b2d07a810daa.

Both findings from review 5327152632 are resolved:

1. gunbc.plans.dag_v2_defork_audit and its generated Markdown projection now preserve the historical #12055 reading while recording that #12227 withdrew Bool→Int; they also correctly bound String→String to the raw helper roster rather than claiming a production identity refusal.
2. v2.test.claim.coercion.two_algebra_fork no longer claims it can report “both agree and both are semantically wrong.” It now states the exact limit: each expected column is transcribed from its own authority, so the fixture can catch deviation from those contracts but has no independent semantic oracle.

The remaining fixture update is coherent: Bool→Int stays enrolled as a permanent withdrawal control, both algebras now expect refusal, all four matrix cells remain inhabited, and the differing population is correctly 3/7. Compiler, clippy and emit-build are green at this head; floor was still running when this approval was submitted.