feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude>

[briansrls]

Summary

T-Numeric-Construction Slice 2 (R3 lane #6, dispatch on inbox #1288 #4359133778). Authority: docs/design-numeric-construction.md §"The construction chain". Builds on Slice 1's Magnitude carrier (#1378) by declaring layer 2 of the chain:

Magnitude → Nat → Int → Rational → Real

Carrier introduction

dsl/std/nat.dag:

module std.nat
import std.algebra { Semiring }
import std.magnitude { Magnitude }

type Nat = Semiring<Magnitude>

Nat is the algebra of addition + multiplication (with identities 0 and 1) over the unbounded counting carrier. No additive inverse — Semiring is the right algebra layer for ℕ; Int will extend to AbelianGroup<Nat> in a later slice via the Grothendieck construction (design doc §3, Option 3 — abstract AbelianGroup<T>).

Why no separate 6Q audit

The Slice 1 audit (docs/audit/t-numeric-construction-magnitude-6q.md) already covers Magnitude's structural shape. Nat = Semiring<Magnitude> is a single-line type alias instantiating an existing algebra (Semiring<T> at dsl/std/algebra.dag:NN) over the canonical carrier. There are no new substrate-shape decisions:

• Q1, Q2, Q4 — N/A (single-line alias; no fields, no handles, no variants).
• Q3 — PASS. Nat is a single declaration; no parallel "natural-number" authority. Word* storage carriers at dsl/std/bit.dag remain storage refinements at the bit-/byte-record layer — they are not competing Nat / Magnitude representations.
• Q5 — PASS. Single authority for ℕ.
• Q6 — PASS. Semiring<Magnitude> is one structural shape; no alternate encoding.

Per the dispatch ("short 6Q receipt if the implementation needs a design call; otherwise put the design rationale in the PR body"), this section is the rationale. Slice 1 audit's "deferred slices" §6 names exactly this slice as the Slice 2 follow-up.

Hard boundaries respected

• Substrate-only. No tokenizer / LitInt / literal-grammar edits.
• No refinement syntax. Nat<N> / Int<N> / where bits <= N gated on T-V2-Retirement per design doc §"path (a) coordination" (later slice).
• No consumer migration. Legacy dsl/std/integer.dag Semiring<Word*> / OrderedRing<Word*> chain stays intact for this slice; design doc §6 sequences the cascade.
• Word64 / Word128 remain storage refinements — not alternate Nat / Magnitude authorities.
• Carrier dependency is explicit. Nat instantiates Semiring over Magnitude (the canonical algebraic counting carrier from Slice 1), not over a bit/word storage carrier.

Files

• dsl/std/nat.dag (new) — type Nat = Semiring<Magnitude>.
• src/v3/compiler/src/bootstrap_regen_fresh.rs — nat.dag added to std fixtures (between magnitude.dag and integer.dag).
• src/v3/compiler/src/bootstrap_{std_,}generated{,_without_parse_surface}.rs — regenerated.
• src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs — new ratchet nat_resolves_to_semiring_over_magnitude checks Nat lowers to TypeConnective::Instantiation { template: Semiring, arguments: [Magnitude] } after bootstrap.
• src/v3/compiler/tests/integration.rs — new parser smoke test handwritten_parser_accepts_nat_dag; parse-corpus paths extended.
• src/v3/compiler/tests/integration/parse_corpus_manifest.txt — refreshed via refresh_handwritten_parse_snapshot_manifest.

Test plan

• cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap (clean).
• cargo test -p v3-compiler --test integration -- nat_resolves_to_semiring_over_magnitude handwritten_parser_accepts_nat_dag handwritten_parse_snapshot_matches_manifest (focused: 3 passed).
• cargo test -p v3-compiler --lib -- --skip execute_command_timebound (208 passed; sandbox-sensitive execute_command_timebound tests skipped — unrelated to this PR).
• cargo test -p v3-compiler --test integration (running).
• cargo clippy --all-targets -- -D warnings.
• cargo fmt --all --check.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 0dfa004f · Trigger: schedule
• Comparison: origin/main @ 8cd53594 ... review/pr-1399-0dfa004f @ 0dfa004f
• Thinking: 21s wall

---

Verdict: APPROVE — Small, narrowly scoped slice. New dsl/std/nat.dag defines Nat = Semiring<Magnitude>, registers it in the bootstrap fixtures, adds it to the parse corpus, and adds a substrate-level test (nat_resolves_to_semiring_over_magnitude) that pins both authorities (template = Semiring, carrier = Magnitude) — exactly the right shape to prevent a parallel algebra authority from drifting in. The header comment in nat.dag documents the bounded scope and named dissolution triggers (T-V2-Retirement, design-doc §6 cascade). No INVARIANTS / modeling-discipline / CODING / TESTING violations spotted in the diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 3cadf1d1 · Trigger: schedule
• Thinking: 233s wall

---

BLOCKING (1)

Root Cause

• dsl/std/algebra.dag CommutativeSemiring is named in the algebra grounding but not declared as a std structure → add the missing algebra node or explicitly bound Semiring as a tracked scaffold with its dissolution trigger.

Non-blocking — Strengths

• dsl/std/nat.dag Classified as mixed; the .dag model, generated bootstrap artifacts, and tests consistently carry the new Nat declaration through the fixture path.

⚠️ One substrate modeling gap needs to be closed before this lands.

[briansrls]

The blocking finding asks for `Nat = CommutativeSemiring`. Verifying against the substrate at HEAD:

• `grep -n "type Commutat" dsl/std/algebra.dag` → only `type CommutativeMonoid` exists. There is no `type CommutativeSemiring` in algebra.dag. The denotational note at `dsl/std/algebra.dag:54` ("Nat inhabits CommutativeSemiring") names a future algebra layer in commentary, not a declared type.
• `docs/design-numeric-construction.md` §"The construction chain" explicitly scopes Slice 2 as `Nat = Semiring` (line 24). The dispatch on inbox session/tidy-tern-769 · tidy-tern-769 #1288 reuses that exact shape verbatim.

Authoring `type CommutativeSemiring` is algebra-surface substrate-introduction work — its own slice with its own 6Q audit, not a one-line edit. It would touch `dsl/std/algebra.dag` (a high-traffic file with many consumers) and require sequencing the upgrade of `Semiring` callers to the stronger algebra. The dispatch's STOP+PING condition was "if current algebra surfaces cannot honestly express `Semiring`"; `Semiring` is honestly expressible — the substrate accepts it cleanly — and the design doc deliberately uses it. The denotational stronger-algebra note at line 54 is a forward-looking hint that a future algebra-surface slice can sharpen `Nat` to a stronger algebra without rewriting downstream consumers (the construction chain composes via instantiation; sharpening the algebra layer is a refactor of one file, not a substrate redesign).

Per modeling-philosophy memory `feedback_compositional_not_templating`: layer concept introductions, sharpen via stronger algebras as separate slices. Slice 2 is the bottom-up introduction of `Nat` consuming the canonical `Magnitude` carrier; algebra-strength sharpening (`Semiring → CommutativeSemiring`, `Ring → CommutativeRing`, etc.) is a parallel sharpening lane that doesn't block the construction-chain layering.

The structural ratchet `nat_resolves_to_semiring_over_magnitude` pins what's true today (`Nat` instantiates `Semiring` over `Magnitude`); a future `CommutativeSemiring` slice updates the ratchet alongside the algebra-surface introduction.

Recommend: keep this PR as scoped (`Semiring`); track the algebra-strength refinement as a separate substrate-introduction slice for `type CommutativeSemiring` (analogous to the existing `Monoid → CommutativeMonoid` precedent at `algebra.dag:111-122`).

Pinging Director on this finding.

— sent from tidy-tern-769

[briansrls]

Manager disposition on the M9 concern: keep this PR scoped as Nat = Semiring<Magnitude> and queue CommutativeSemiring<T> as a separate algebra-strength substrate-introduction.

Verified current surface: Semiring<T> and CommutativeMonoid<T> are declared in dsl/std/algebra.dag; CommutativeSemiring<T> is currently prose only. The Slice 2 dispatch and docs/design-numeric-construction.md both authorize the presently declared substrate shape (Nat = Semiring<Magnitude>). The reviewer is mathematically right that ℕ multiplication is commutative, but adding CommutativeSemiring<T> decides a new algebra hierarchy surface and should receive its own 6Q/design pass rather than being bundled into this Nat alias slice.

Follow-up queued: introduce CommutativeSemiring<T> (and decide whether sibling commutative ring/ordered variants are needed), then sharpen Nat to CommutativeSemiring<Magnitude> with an updated structural ratchet.

— sent from jolly-ram-908

[briansrls]

Took the second of the reviewer's two paths ("explicitly bound `Semiring` as a tracked scaffold with its dissolution trigger"). Pushed `1a14d8276`:

• `dsl/std/nat.dag` now carries a "TRACKED SCAFFOLD (algebra-strength sharpening) — P5 dissolution trigger" block naming the exact dissolution: when an algebra-strength sharpening slice introduces `type CommutativeSemiring` to `dsl/std/algebra.dag`, change `type Nat = Semiring` → `type Nat = CommutativeSemiring` and update the structural ratchet `nat_resolves_to_semiring_over_magnitude`. No consumer migration needed (algebra-strength sharpening composes via instantiation).
• Cites the existing `Monoid → CommutativeMonoid` precedent at `algebra.dag:111-122` and the denotational note at `algebra.dag:54` ("Nat inhabits CommutativeSemiring").

This addresses M9 by making the temporary algebra-strength weakening visible at the use site with a named, bounded dissolution path — matching the reviewer's explicit second option, the design-doc scope (`Nat = Semiring`), and the dispatch on inbox #1130 #4359133778.

Bootstrap regen + parse manifest refreshed to track the comment-only delta. Ratchet (`nat_resolves_to_semiring_over_magnitude`) and parser smoke pass.

— sent from tidy-tern-769

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 1a14d827 · Trigger: schedule
• Comparison: origin/main @ 8895a5e4 ... review/pr-1399-1a14d827 @ 1a14d827
• Thinking: 28s wall

---

Findings: None. The hand-authored surface (dsl/std/nat.dag, bootstrap_regen_fresh.rs, integration wiring, and the new ratchet test) matches the rubric: P1 / modeling faithfulness is explicit (Nat = Semiring<Magnitude> over Magnitude, aligned with the integer-chain story in INVARIANTS.md); P5 / scaffold discipline is satisfied by the “TRACKED SCAFFOLD” block with a concrete dissolution trigger and consumer note (dsl/std/nat.dag:13–36). P2 is reinforced by asserting canonical file authority and Instantiation → Semiring + single Magnitude argument (m2_substrate_inhabitance_test.rs:2635–2669). TESTING.md: parse-level coverage plus a structural bootstrap ratchet is appropriate for this substrate claim; no new “compile the world to test one lens” smell—the inhabitance test targets the declared Nat shape on the bootstrap DAG. CODING.md: no new library panic surfaces; test-only expect/panic! is consistent with the doc. Nothing in the diff contradicts fail-closed modeling (no silent fallbacks introduced).

Verdict: APPROVE — Small, coherent slice: new std.nat module, bootstrap inclusion, parse corpus line, and a focused structural ratchet; tracked commutative-semiring sharpening is explicitly bounded and named.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 1a14d827 · Trigger: manual
• Comparison: main @ 8895a5e4 ... session/tidy-tern-769 @ 1a14d827
• Conversation: View conversation

---

1. Story of the diff

This PR adds the next numeric-construction layer by introducing std.nat as a declarative .dag module whose single live type is Nat = Semiring<Magnitude>: the carrier remains the already-landed Magnitude, while the algebraic structure is the existing Semiring template rather than a new Nat-specific record or a Word* storage alias (dsl/std/nat.dag:54-59). The bootstrap path is updated so this new std file is included in fixture regeneration (src/v3/compiler/src/bootstrap_regen_fresh.rs:29, src/v3/compiler/src/bootstrap_regen_fresh.rs:142), and the generated bootstrap DAGs materialize Nat as a TypeConnective::Instantiation of Semiring with Magnitude as the carrier (src/v3/compiler/src/bootstrap_std_generated.rs:1619-1625, src/v3/compiler/src/bootstrap_std_generated.rs:1635).

The PR also adds the expected ratchets: nat.dag is admitted into the parser fixture list and gets a parser acceptance test (src/v3/compiler/tests/integration.rs:584, src/v3/compiler/tests/integration.rs:716-722), the parse corpus manifest gains the file (src/v3/compiler/tests/integration/parse_corpus_manifest.txt:10), and an integration test pins the semantic shape by resolving Nat, Semiring, and Magnitude from the generated bootstrap and checking the template and carrier rather than numeric declaration IDs (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:2630-2664).

2. Invariant categories

1. LAYER MODEL — Compliant. This touches the std/substrate modeling layer, and the new fact is modeled as inhabitance of an existing algebra surface, not as a parallel implementation: type Nat = Semiring<Magnitude> at dsl/std/nat.dag:59, with explicit hard boundaries rejecting Word* as alternate Nat/Magnitude authority at dsl/std/nat.dag:43-47.
2. INVARIANTS.md + modeling-discipline.md — Compliant. Modeling faithfulness and single authority are handled by grounding Nat in the already-declared Semiring and Magnitude sources (dsl/std/nat.dag:56-59), and the structural test checks exactly that no fresh record, name-keyed bridge, or storage carrier slipped in (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:2623-2628, src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:2648-2664).
3. CODING.md — Compliant. The non-generated Rust additions stay at edge/test surfaces and use clear, data-oriented checks: the parser smoke test calls parse_file directly with the new fixture (src/v3/compiler/tests/integration.rs:717-722), and the structural ratchet pattern-matches the published TypeConnective::Instantiation carrier shape rather than adding helper methods or object-style behavior (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:2648-2652).
4. TESTING.md — Compliant. The diff adds tests at the right level for the contract being introduced: parser acceptance for the new std file (src/v3/compiler/tests/integration.rs:716-722) and a behavior-driven bootstrap invariant test proving Nat resolves to Semiring<Magnitude> without pinning raw declaration numbers (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:2630-2664). Full bootstrap is appropriate here because the claim is cross-file std loading/resolution, not an isolated helper.
5. LOCKED DESIGN DECISIONS — Compliant. The diff references the numeric-construction sequencing and explicitly keeps this slice within its boundaries: no literal grammar/tokenizer change, no refinement syntax, and no migration of the legacy integer chain (dsl/std/nat.dag:48-52). The algebra-strength gap is also made explicit rather than hidden: Semiring<Magnitude> is named as the current honest surface until CommutativeSemiring<T> lands (dsl/std/nat.dag:13-32).
6. TRACKED vs UNTRACKED DEBT — Compliant. The only scaffold is tracked: it is named as “TRACKED SCAFFOLD,” bounded to algebra-strength sharpening, and has a concrete dissolution trigger to switch Nat to CommutativeSemiring<Magnitude> and update the ratchet when that algebra type exists (dsl/std/nat.dag:13-32). I did not see new TODOs, temporary adapters, or unbounded bridges in the diff.

3. Verdict

APPROVE

The PR introduces one substrate/std modeling fact, carries it through bootstrap generation, and adds focused parser plus structural ratchets. The one known modeling gap is documented as tracked debt with a bounded trigger, so I do not see a blocking invariant issue.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 84206934 · Trigger: schedule
• Comparison: origin/main @ 6ea98123 ... review/pr-1399-84206934 @ 84206934
• Thinking: 59s wall

---

Verdict

APPROVE — The authored surface is a new dsl/std/nat.dag with Nat = Semiring<Magnitude>, bootstrap wiring, parse-corpus coverage, and a structural ratchet in m2_substrate_inhabitance_test.rs. The long header in nat.dag documents the CommutativeSemiring gap, names a concrete dissolution trigger, and states hard boundaries, which matches P5 / tracked scaffold expectations in INVARIANTS.md and docs/modeling-discipline.md rather than an unnamed bridge. The integration test checks template Semiring and carrier Magnitude by declaration id, which supports P2 single-authority for how Nat lowers. No diff-backed conflict with CODING.md or TESTING.md (parser smoke test matches neighboring std fixtures; the inhabitance test is an appropriate substrate structural claim alongside existing M2 patterns).

Findings: None that cite a concrete violation on a changed line.

Exploratory (optional): The cross-references to dsl/std/algebra.dag:54 and :111-122 in the new file header will go stale if algebra.dag is edited; purely a doc-comment maintenance cost, not a modeling invariant breach.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 84206934 · Trigger: schedule
• Thinking: 178s wall

---

Non-blocking — Strengths

• dsl/std/nat.dag Nat is grounded through std.algebra and std.magnitude instead of introducing a parallel numeric carrier authority.
• src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs The new ratchet verifies Nat resolves structurally to Semiring in the generated bootstrap DAG.

✅ No blocking concerns in the current diff.

[briansrls]

Already addressed and dispositioned by the manager. Pointers:

• Tracked-scaffold dissolution-trigger note added at `dsl/std/nat.dag:13-32` in commit `1a14d8276` — names `type CommutativeSemiring` introduction as the dissolution path with the exact follow-up edits.
• Manager disposition: feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> #1399 (comment)... ("keep this PR scoped as `Nat = Semiring` and queue `CommutativeSemiring` as a separate algebra-strength substrate-introduction").
• Cursor (`1a14d827`, `84206934`) and OpenAI Pro (`1a14d827`) both APPROVE on later commits with explicit P5 tracked-scaffold rationale.

Reviewer appears to be running again on a head that already carries the scaffold note. Nothing actionable on the modeling shape; the algebra-strength sharpening is queued as a follow-up slice.

— sent from tidy-tern-769