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

DESIGN.md

@@ -236,8 +236,12 @@ still a violation) · internal review finds missing tests, external review finds
   `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is
   the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`,
   so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its
-  realization (numeric tower first, `Int = GroupCompletion<Nat>` still bottoming in Peano `Nat`), which
-  dissolves the straddle and makes the guard dead code. (operator: `==` fail-closed, 2026-06-20)
+  realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded
+  (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop`
+  `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until
+  the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window).
+  **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper
+  root, its own runway). (operator: `==` fail-closed, 2026-06-20)
 - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)
 
 ## Building & checks

docs/plans/model-realization-fork.md

@@ -45,10 +45,13 @@ other primitive is per-site.
 
 ## 3. Grounding order (does it dissolve the guards?)
 
-1. **Numeric tower — grounds cleanly; YES, dissolves the guard.** Finish `Int = GroupCompletion<Nat>`
-   bottoming in Peano `Nat`, so the native form *is* the modeled form. Then
-   `cross_representation_numeric_straddle` (and the `eval_binop` guard) become **dead code**. Highest
-   value / lowest risk. Start here.
+1. **Numeric tower — GROUNDED (#5428, 2026-06-21).** Nat construction-side grounded:
+   `Zero → Value::Int(0)`, `Succ{prev:Int(k)} → Value::Int(k+1)` — native form == modeled form.
+   `cross_representation_numeric_straddle` is dead-in-corpus for numerics; `eval_binop`'s
+   `CrossRepresentationEquality` guard is **kept as fail-closed backstop** (not removed — guard removal
+   is bundled with the `Value::Null` split in §3.2, fenced out of this window). The discriminating
+   witness `cross_representation_equality_test` confirms: former fork cases now reconcile to `Bool(true)`;
+   genuine diffs (`1==2`, `Succ{Zero}==Zero → Int(1)==Int(0)`) stay `false`. **Done.**
 2. **`Value::Null` overload — the deeper root; NO, needs SPLITTING not grounding-away.** `Value::Null`
    means *None* / *Absent* (Optional) / *miss* (map lookup) / *Violates* (Witness) **all at once**. So a
    blanket equality guard is wrong — `present == None → false` is *legitimate* at ~131 sites. The fix is