Skip to content

docs: reconcile numeric-tower grounding status (landed→grounded, post-#5428 + #5425) - #5440

Merged
briansrls merged 1 commit into
mainfrom
doc/model-realization-fork-grounded
Jun 21, 2026
Merged

briansrls merged 1 commit into
mainfrom
doc/model-realization-fork-grounded

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 21, 2026

Copy link
Copy Markdown
Contributor

Summary

Deferred doc reconciliation from #5428 (smart-crane) which explicitly noted: "The shared-doc status reconciliation (numeric row landed→grounded; DESIGN §5 open-thread b) is deferred to the lane manager post-#5425." #5425 has now merged.

Two targeted edits, no logic changes:

  • DESIGN.md §5 open-thread (b): numeric tower marked GROUNDED (Numeric-tower grounding: ground Nat construction-side so native form == modeled form (§0) #5428, 2026-06-21); records that eval_binop CrossRepresentationEquality guard is dead-in-corpus for numerics but deliberately kept as fail-closed backstop until Value::Null split (guard removal bundled with that work, fenced out of this window). Remaining item: Value::Null split (~131 sites, its own runway).

  • docs/plans/model-realization-fork.md §3.1: numeric row updated from "Finish … Start here." (pending) to GROUNDED: exact realization (Zero→Int(0), Succ{prev:Int(k)}→Int(k+1)), discriminating witness noted, guard-kept rationale recorded. §3.2 (Value::Null split) unchanged.

Test plan

  • Doc-only PR; no .dag or .rs changes — CI floor runs compile-clean + layering-imports, no functional gates to break.
  • Verify §3.1 in model-realization-fork.md matches Numeric-tower grounding: ground Nat construction-side so native form == modeled form (§0) #5428's behaviour (Zero/Succ realizations, guard kept, witness confirmed).
  • Verify DESIGN.md open-thread (b) is now a consequence-chain (grounded fact → guard dead-in-corpus → remaining root = Null split) with no orphan claim.

🤖 Generated with Claude Code

#5428 (smart-crane) grounded Nat construction-side — Zero→Int(0),
Succ{prev:Int(k)}→Int(k+1) — so native form == modeled form.
Deferred doc update explicitly to lane manager post-#5425.

DESIGN.md §5 open-thread (b): mark numeric tower GROUNDED; note that
eval_binop CrossRepresentationEquality guard is dead-in-corpus for
numerics but kept as fail-closed backstop until Value::Null split
(guard removal bundled with that work, fenced out of this window).

docs/plans/model-realization-fork.md §3.1: numeric row landed→grounded;
records the exact realization, discriminating witness, and why the guard
stays (bundled removal, not a regression). §3.2 (Value::Null split)
unchanged — still the deeper root, its own runway.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls
briansrls merged commit 116dd3f into main Jun 21, 2026
1 check passed
@briansrls
briansrls deleted the doc/model-realization-fork-grounded branch June 21, 2026 06:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant