Nat census follow-up: discharge BLOCKED+LAST, regen defork audit

dag/gunbc/plans/dag_v2_defork_audit.dag

@@ -17,7 +17,7 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
       alignments: [AlignNone, AlignNone, AlignNone, AlignNone, AlignNone, AlignNone],
       rows: [
         row(cells: [cell(text: "**algebra**"), cell(text: "16 (13 differ; 3 byte-identical `Lattice`/`Magma`/`Ordering`)"), cell(text: "same concept, divergent **encoding** (dag flat records vs v2 compositional/coproduct)"), cell(text: "**LIVE — 75 entries**"), cell(text: "grounding (Root-A: v2 coproduct authority RULED 2026-06-22)"), cell(text: "cant-unify-yet, **has path** (de-fork-resolved, not exempted)")]),
-        row(cells: [cell(text: "**nat**"), cell(text: "1 (`Nat`: `= CommutativeSemiring<Magnitude>` vs `= Zero \\| Succ`)"), cell(text: "same concept, divergent **model**"), cell(text: "**LIVE — 138 floor entries** (946 scanned; was 4 @ 351, 2026-06-23)"), cell(text: "grounding (#5428 numeric tower; escalated smart-ant-466)"), cell(text: "cant-unify-yet, has path; BLOCKED + LAST · census nat-grounding-unification-design.md")]),
+        row(cells: [cell(text: "**nat**"), cell(text: "1 (`Nat`: `= CommutativeSemiring<Magnitude>` vs `= Zero \\| Succ`)"), cell(text: "same concept, divergent **model** (semiring alias vs Peano coproduct — representational, not nominal)"), cell(text: "**LIVE — 138 floor closures** (946 scanned; was 4 @ 351) — **risk measure, not a task count** (see §2A note)"), cell(text: "grounding (#5428 numeric tower; census nat-grounding-unification-design.md)"), cell(text: "**DESIGN READY** · IMPLEMENTATION LARGE/ATOMIC · SEQUENCED WITH integer+float repoint (not last)")]),
         row(cells: [cell(text: "**effects**"), cell(text: "3 (`EffectShape`/`KeySource`/`CreateCause`; `EffectShape` body re-modeled on a different axis)"), cell(text: "divergent **axis** (operation-kind vs idempotency-class)"), cell(text: "latent (0)"), cell(text: "grounding"), cell(text: "cant-unify-yet, has path (axis-authority decision)")]),
         row(cells: [cell(text: "**float**"), cell(text: "3 (2 differ; 1 byte-identical `Float = Float64`)"), cell(text: "same concept, divergent encoding"), cell(text: "latent (0)"), cell(text: "grounding (#5428)"), cell(text: "cant-unify-yet, has path")]),
         row(cells: [cell(text: "**integer**"), cell(text: "14 (11 differ only on `MachineWidth<8>` vs `<Word8>`; 3 byte-identical)"), cell(text: "same concept, near-identical (token diff)"), cell(text: "latent (0)"), cell(text: "grounding (#5428)"), cell(text: "cant-unify-yet, has path (mechanical once the tower lands)")]),
@@ -27,6 +27,7 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
         row(cells: [cell(text: "**node**"), cell(text: "**0** (dag v1-only `compiler_inductive_fields` vs v2 Node substrate)"), cell(text: "divergent concept, **no name overlap**"), cell(text: "none (0 shared)"), cell(text: "v1-artifact name-collision"), cell(text: "dissolve-on v1-delete; **0 type-name collisions → exemption vacuous for the guard**")]),
       ],
     },
+    p(text: "**Co-occurrence closure counts (algebra 75, nat 138):** each integer counts floor `*_test.dag` **import closures** where both `std.<b>` and `v2.std.<b>` are reachable — a **risk and closure-population measure** for the LIVE fail-open pair, **not** a migration task count or work estimate. New floor entries and tests can grow these numbers legitimately; **do not** ratchet on the integer (gate the unsafe facts instead — nat census §7.6 in [nat-grounding-unification-design.md](nat-grounding-unification-design.md)). Until the fork dissolves, mixed closures silently shadow record-with-record (benign today for nat; coproduct-variant-drop for algebra)."),
     p(text: "**Confirms parent's derived distribution; cant-unify-yet == \{node, coercion\} exactly; flag-ANY +\n\{node,coercion\} HOLDS.** Two scope refinements (strengthen, do not refute the ruling):"),
     ol(items: [
       li(text: "**The \{node,coercion\} exemption is VACUOUS for the type-name guard.** node/coercion (and logic,\nand now verification) share **zero** type names — only the *basename*. The guard keys on a shared\nunqualified **type name** within one closure, so it never fires on them; their de-fork is a\n*module-basename* rename (Route-C / v1-delete), a different surface. The guard needs no\n\{node,coercion\} roster entry to land green — keeping it would be a dead (non-firing) exemption,\nitself a §5 smell. Recommend marking the roster entry explicitly \"Route-C basename, non-firing\"\nor dropping it from the guard model."),
@@ -78,7 +79,7 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
       rows: [
         row(cells: [cell(text: "**algebra**"), cell(text: "16 abstract structures (`Magma`…`Field`, `FreeMonoid`, `Ordering`)"), cell(text: "no (the structures match)"), cell(text: "dag-only 19 = template/codegen machinery **+ `GroupCompletion`/`FieldOfFractions`**; v2-only 74 = **41 `_node`/`_type_node` substrate projections** + the list/fold framework (213 importers)"), cell(text: "numeric tower (`GroupCompletion` = `Int = GroupCompletion<Nat>`) **+** model↔realization substrate reflection. Each side owns a different grounding.")]),
         row(cells: [cell(text: "**logic**"), cell(text: "**0**"), cell(text: "— (no overlap)"), cell(text: "dag-only = `Classical`/`classical_and/or/not`; v2-only = `Bool` + boolean-algebra instance + 6 node-projections + `BoolEncodingFact`/`BoolWidthFact`/`BoolPrimitiveFacts`"), cell(text: "Bool grounded into **bit-width** (model↔realization). Operator picks: genuinely different concepts (→ rename) **or** one boolean modeled twice (→ unify on v2's grounded).")]),
-        row(cells: [cell(text: "**nat**"), cell(text: "`Nat` (the name)"), cell(text: "yes (thin alias vs coproduct)"), cell(text: "dag = 4-decl `Nat = CommutativeSemiring<Magnitude>`; v2 = 12-decl coproduct `Zero/Succ` + `nat_cata`/`nat_add`/`nat_mul`/`is_zero`/`nat_lte`/`nat_gte`/`NatAlgebraLawObligation`"), cell(text: "**#5428** grounded numeric tower (`Zero → Int(0)`, `Succ → Int(k+1)`). Escalated (smart-ant-466).")]),
+        row(cells: [cell(text: "**nat**"), cell(text: "`Nat` (the name)"), cell(text: "yes (thin alias vs coproduct)"), cell(text: "dag = 4-decl `Nat = CommutativeSemiring<Magnitude>`; v2 = 12-decl coproduct `Zero/Succ` + `nat_cata`/`nat_add`/`nat_mul`/`is_zero`/`nat_lte`/`nat_gte`/`NatAlgebraLawObligation`"), cell(text: "**#5428** grounded numeric tower (`Zero → Int(0)`, `Succ → Int(k+1)`). Census complete (2026-08-01): **DESIGN READY** — [nat-grounding-unification-design.md](nat-grounding-unification-design.md); prerequisites discharged (#6341 merged; coproduct keystone green). **IMPLEMENTATION LARGE/ATOMIC**, sequenced with integer+float repoint (not last).")]),
         row(cells: [cell(text: "**integer**"), cell(text: "14 = the **whole `Int`/`UInt` width tower** (`Int`, `Int8…128`, `UInt`, `UInt8…128`, `IntPlatform`, `UIntPlatform`)"), cell(text: "no"), cell(text: "v2-only +72 = the arithmetic ops grounded **on** the tower"), cell(text: "`Int = GroupCompletion<Nat>` numeric tower.")]),
         row(cells: [cell(text: "**float**"), cell(text: "3 (`Float`, `Float32`, `Float64`)"), cell(text: "no"), cell(text: "v2-only +18 = algebraic-vs-bit-level ops"), cell(text: "the algebraic-vs-bit-level layer of the numeric tower + bit-width.")]),
         row(cells: [cell(text: "**effects**"), cell(text: "6 core (`EffectShape`, `KeySource`, `CreateCause`, +3 fns)"), cell(text: "**YES — the shared `EffectShape` body is re-modeled on a different axis**"), cell(text: "dag = **operation axis** (`ReadEffect`/`UpsertEffect`/`DeleteEffect`/`CreateEffect`/`AppendEffect`) + derivation (`derive_effect_shape`/`OperationEffect`/`compose_effects`); v2 = **idempotency-class axis** (`IsIdempotent(IdempotentShape)`/`IsBreaking(BreakingShape)`) + idempotency machinery + node-projections"), cell(text: "DESIGN §4 \"idempotency dissolved from an `idempotent:Bool` flag into the `EffectShape` variant\" — v2 is that grounding. Unification question: *which axis is the single authority, or are they orthogonal dimensions of one `EffectShape`?*")]),
@@ -93,7 +94,7 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
       li(text: "**Step-4 data import:** `probe_selector` `Option`/`Optional` + `std.*` collision, so `dag/product/compute_fabric` imports cleanly into v2. **DONE (#5904).**"),
     ]),
     p(text: "**Deferred to v1-shrink (the not-a-fork renames):** `coercion`, `node`. v1-seed-coupled; ruled DEFER with the dissolution trigger *\"when v1's consumers of `dag/std/\{node,coercion\}` are removed\"* — at which point `node` self-dissolves (delete the dead file) and `coercion` shrinks to a v1-free disambiguation. Not dispatched until then."),
-    p(text: "**Grounding cluster — held for the operator** (a single-authority unification *design*, downstream of the numeric tower #5428 and the model↔realization grounding): `algebra`, `logic`, `nat`, `integer`, `float`, `effects`, `verification`. These are **not** dispatched as mechanical PRs. The grounded dag authority for each has to be *designed* before any fan-out can repoint to it (the same shape as the project's \"substrate migration precedes the ratchet, is not a path to it\"). `nat` is already escalated (smart-ant-466) and stays BLOCKED + LAST."),
+    p(text: "**Grounding cluster — held for the operator** (a single-authority unification *design*, downstream of the numeric tower #5428 and the model↔realization grounding): `algebra`, `logic`, `nat`, `integer`, `float`, `effects`, `verification`. These are **not** dispatched as mechanical PRs. The grounded dag authority for each has to be *designed* before any fan-out can repoint to it (the same shape as the project's \"substrate migration precedes the ratchet, is not a path to it\"). **`nat` census complete (2026-08-01):** per-concept design in [nat-grounding-unification-design.md](nat-grounding-unification-design.md) — **DESIGN READY**; prerequisites discharged (`algebra` `FreeMonoid` shadow #6341 merged; generic-alias coproduct keystone green). **IMPLEMENTATION LARGE/ATOMIC**, **SEQUENCED WITH integer+float repoint** (not last). Operational gate before the wave: bounded P3b PR2 overflow on `std.integer` lands first (#7511 merged; both lanes touch the numeric authority — one writer at a time). **Atomic wave file ownership (one push):** `dag/std/nat.dag` ← coproduct + Peano ops; delete dag semiring alias; `v2.std.nat` ← thin reimport + node-bound law roster only; `integer`/`float` repoint `GroupCompletion<Nat>` to `std.nat.Nat`; all importer repoints in the same push (§5 auto-committer hazard)."),
     p(text: "**Hazard (atomicity):** the dashboard auto-committer can snapshot a multi-file rename/collapse mid-edit (a symbol deleted in file A while file B still calls it) → an internally-inconsistent intermediate commit caught by a *frozen* merge-sha CI run → phantom \"not found in scope\" red. `gh run rerun` cannot fix it (it re-merges the broken head); only a fresh consistent push. Stage every file of a rename/collapse together."),
     ThematicBreak,
     h2(text: "3b. OPERATOR RULING — grounding-cluster anchor (2026-06-22) — the brief"),

dag/std/integer.dag

@@ -25,7 +25,7 @@ type Signedness
   = Signed
   | Unsigned
 
-data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring<Magnitude> with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). Disposition: awaiting an operator dispatch decision — not deferred work; a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it, so the trigger and acceptance condition above are fixed and what is missing is only the dispatch; naming a fabricated owner would assert an ownership fact that is not true. The bound on the deferral, which is what keeps it tracked rather than parked: until the trigger fires, a bare reference to a Nat operation in a closure containing both authorities is ambiguous by construction and must be qualified — no consumer may assume a bare Nat name resolves, and the two Nat types are not interchangeable at any call site even where the name matches."
+data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring<Magnitude> with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Per nat-grounding-unification-design (census complete 2026-08-01): DESIGN READY; IMPLEMENTATION LARGE/ATOMIC sequenced with integer+float repoint after bounded P3b PR2 overflow on std.integer (#7511 merged first). Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). The bound on the deferral: until the wave lands, a bare reference to Nat or nat_compare in a closure containing both authorities is ambiguous by construction and must be qualified — no consumer may assume a bare name resolves, and the two Nat types are not interchangeable at any call site even where the name matches."
 
 type IntPlatform  = Compose<Int,  MachineWidth<PointerWidth>>
 type UIntPlatform = Compose<UInt, MachineWidth<PointerWidth>>

docs/plans/algebra-grounding-unification-design.md

@@ -14,7 +14,7 @@ Two files define `algebra` on the two std trees:
 - `dag/std/algebra.dag` — module `std.algebra`, **332 lines, 32 importers** (the `dag/` tree + the `src/v1` seed).
 - `src/v2/std/algebra.dag` — module `v2.std.algebra`, **816 lines, 290 importers** (the v2 compiler).
 
-They share **unqualified type names** — the algebraic-structure records (`Magma`/`Semigroup`/`Monoid`/`Group`/…) and, most sharply, the `FreeMonoid<T> = Empty | Cons { head, tail }` coproduct. When a single import closure pulls in *both* trees, those unqualified names bind ambiguously and the resolver silently **drops the coproduct's variant bindings** — the `dag/std/algebra.dag:115` `free_monoid_coproduct_authority` note records the live reproduction (2026-07-05: *"undefined variable: Empty"* in a closure containing both trees). The audit measures this as the **LIVE fail-open** pair `{algebra (75 floor entries), nat (4)}`: it is benign today only because it shadows record-with-record rather than dropping a variant, and a flag-ANY guard wall reds it the moment the fork lands.
+They share **unqualified type names** — the algebraic-structure records (`Magma`/`Semigroup`/`Monoid`/`Group`/…) and, most sharply, the `FreeMonoid<T> = Empty | Cons { head, tail }` coproduct. When a single import closure pulls in *both* trees, those unqualified names bind ambiguously and the resolver silently **drops the coproduct's variant bindings** — the `dag/std/algebra.dag:115` `free_monoid_coproduct_authority` note records the live reproduction (2026-07-05: *"undefined variable: Empty"* in a closure containing both trees). The audit measures this as the **LIVE fail-open** pair `{algebra (75 floor closures), nat (138)}` — closure counts are **risk measures, not task estimates** (see nat-grounding-unification-design §2): it is benign today only because it shadows record-with-record rather than dropping a variant, and a flag-ANY guard wall reds it the moment the fork lands.
 
 This is §5 fail-open (a wrong resolution passes silently) sitting on a §3 single-authority violation (one concept, two homes). It is also the concrete blocker under the QualifiedName-key parking I closed in `type-env-single-authority-design.md` §5.1: `QualifiedName = FreeMonoid<Symbol>`, so it cannot get a clean `std.qualified_name` home — reachable from the v1 SymbolIndex — until `FreeMonoid` has a single authority. **Unforking `algebra` is the gate that unparks that item.**
 
@@ -57,7 +57,7 @@ Because `FreeMonoid`/`Empty`/`Cons` then exist in exactly one place, the **dange
 - **The keystone residue is IN-SCOPE here** (signed Q3). The audit's Root-B keystone (generic-alias instantiation) partially landed (#5552); the residue was *raw variant-matching a value bound from a recursive `Cons.tail` field* failing in the `04_infer` fixpoint (*"variant not found in type FreeMonoid"*). Recon (§7.1 step 2) finds no such pattern live in `04_infer` and the error string absent, so it **appears already resolved** — to be confirmed by executing the keystone witness before the collapse relies on raw `Cons.tail` matching. Load-bearing `03_resolve`/`04_infer` work: model-first, escalate if a real fixpoint gap resurfaces.
 - **Root A is a separate lane, currently UNOWNED.** The `src/v1/05_emit_rust.dag` grounding emit-seam (host `Vec`) is not authored here; **this design does not touch `05_emit_rust.dag`**. Its prior owner (jolly-cat) is gone from the tree (§7 Q4). This lane is **not blocked on Root A** — it lands `QualifiedName` only, which needs no host-`Vec` alias grounding; the `String`/`List` alias follow-on is what depends on Root A being re-dispatched.
 - **Atomicity hazard.** The dashboard auto-committer can snapshot a multi-file rename mid-edit → an internally-inconsistent commit → phantom "not found in scope" red on a frozen merge-sha CI run. **Every file of the collapse (FreeMonoid delete + moved ops + 290 repoints) stages together in one push.**
-- **Land-green ordering.** The `FreeMonoid` collapse (delete + moved ops + repoint) lands green only when all its files are in the same push. Because the **records stay forked** here (deferred, §3.1), the flag-ANY co-occurrence wall for the algebra pair does **not** go green on this lane — see §6. `nat` (escalated, smart-ant-466) stays BLOCKED + LAST per the audit; `algebra`'s FreeMonoid is the anchor that goes first.
+- **Land-green ordering.** The `FreeMonoid` collapse (delete + moved ops + repoint) lands green only when all its files are in the same push. Because the **records stay forked** here (deferred, §3.1), the flag-ANY co-occurrence wall for the algebra pair does **not** go green on this lane — see §6. `nat` census is **DESIGN READY** (prerequisites discharged: #6341 merged, generic-alias coproduct keystone green) — **IMPLEMENTATION LARGE/ATOMIC**, **SEQUENCED WITH integer+float repoint** (not last); `algebra`'s FreeMonoid shadow-removal remains the anchor that goes first on this lane.
 
 ## 6. Validation (§5 prove-by-execution, not typecheck)