Coercion ledgers: truth-only repair after #12055; DESIGN §4 records the coercion ruling

[gunbai-bot]

• coercions_boundary: cite the two_algebra_fork witness; record that it measures the two
  helper contracts (disagreeing in both directions), not production judgments and not an
  independent semantic oracle; String->String is admitted by name identity at every live
  site before dag_can_cast is consulted; v1.compiler.coercion reads per-target
  CastSyntax cast_rules, not dag_can_cast.
• trigger (boundary + stall): no longer names one replacement fold. The roster serves
  several judgments (declared-type compatibility, explicit as, target realization;
  literal introduction is std.literal_elaboration; Int->Nat is literal homomorphism vs
  proof-requiring refinement cast), so retirement is per-judgment consumption.
• failure-mode specimen and fixture header: same corrections.
• DESIGN §4 (gunbc.design_document + projection): coercion is the implicit-safe subset
  of declared conversions (operator ruling 2026-09-26).

No behaviour change.

Local interpreter check could not run (remote runner refused HostBudgetUnreadable before evaluating); CI parse, floor and the docs projection drift gate are the verification.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 71467 in d29d9aa. Confirmed: SPECIMEN 1 still said "in the type-relation fold". Checking the actual call sites showed my replacement labels were loose too: the three dag_can_cast callers in v1.compiler.infer are kernel_value_declared_type_mismatch_bounded, application_type_names_compatible and validate_cast. All four places in this PR now name those symbols (§3: cite the symbol). The same stale sentence also appeared in gunbc.plans.dag_v2_defork_audit and its docs/plans/dag-v2-defork-audit.md projection, so both are fixed as well. A grep for the old phrase now finds nothing.

[gunbai-bot]

One correction to review 71476, so the record doesn't overstate what was checked. It says the DESIGN.md paragraph was regenerated from its authority. It wasn't. I wrote the same paragraph by hand into both gunbc.design_document section_4_blocks and DESIGN.md, because the local regeneration couldn't run: the remote runner refused with HostBudgetUnreadable before evaluating anything. So nothing has yet shown that the two match; the CI docs-projection drift gate is that check. I'll treat this PR as unverified until that gate is green.

— sent from silent-swift-419