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

dsl/std/nat.dag

@@ -0,0 +1,59 @@
+// std/nat.dag -- Natural numbers (ℕ) as semiring over the abstract counting carrier.
+//
+// Layer 2 of the construction chain authored in
+// `docs/design-numeric-construction.md`:
+//
+//   Magnitude → Nat → Int → Rational → Real
+//
+// `Nat = Semiring<Magnitude>` says "ℕ is the algebra of addition + multiplication
+// (with identities 0 and 1) over the unbounded counting carrier `Magnitude`."
+// No additive inverse — `Semiring` is the right algebra layer for ℕ; `Int`
+// extends to `AbelianGroup<Nat>` in a later slice (Grothendieck construction).
+//
+// TRACKED SCAFFOLD (algebra-strength sharpening) — P5 dissolution trigger:
+//   The denotational note at `dsl/std/algebra.dag:54` says
+//     "Nat inhabits CommutativeSemiring  (because (Nat, *, 1) is a commutative monoid)"
+//   but `dsl/std/algebra.dag` declares only `type Semiring<T>` (no
+//   `type CommutativeSemiring<T>`). `Semiring<Magnitude>` is the closest
+//   honest algebra surface available today; multiplicative commutativity
+//   of ℕ is true denotationally but not yet pinned structurally in the
+//   substrate. Precedent for the sharpening is already in algebra.dag:
+//   `Monoid → CommutativeMonoid` is the same shape (`algebra.dag:111-122`).
+//
+//   **Dissolution trigger:** when an algebra-strength sharpening slice
+//   introduces `type CommutativeSemiring<T>` to `dsl/std/algebra.dag`,
+//   change this declaration to
+//     `type Nat = CommutativeSemiring<Magnitude>`
+//   and update the structural ratchet
+//   `nat_resolves_to_semiring_over_magnitude` in
+//   `src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs`
+//   to match the new template id. No consumer migration needed —
+//   `CommutativeSemiring<T>` extends `Semiring<T>` at the algebra layer;
+//   downstream callers see no signature change.
+//
+//   The construction-chain progression in `docs/design-numeric-construction.md`
+//   sequences concept-layer introduction first (this slice + Slices 3+);
+//   algebra-strength sharpening is a parallel lane (see PR #1399 inbox
+//   discussion at #1130).
+//
+// CONSUMERS: none in this slice. Refinements `Nat<N>` (later slices, gated
+// on T-V2-Retirement per design doc §"path (a) coordination") parameterize
+// the namespace to bind concrete bit-width at grounding time.
+//
+// HARD BOUNDARIES:
+//   - Carrier is `Magnitude`, the canonical algebraic counting carrier.
+//     `Word64` / `Word128` (and `Byte`/`Word16`/`Word32`) at `dsl/std/bit.dag`
+//     remain **storage refinements** at the bit-/byte-record layer; they are
+//     not alternate `Nat`/`Magnitude` authorities.
+//   - No tokenizer / `LitInt` / literal-grammar changes.
+//   - No refinement syntax (`Nat<N>`, `where bits <= N`) — gated on
+//     T-V2-Retirement per design doc.
+//   - No migration of legacy `dsl/std/integer.dag` `Semiring<Word*>` / `OrderedRing<Word*>`
+//     chain — sequenced for design doc §6 cascade slice.
+
+module std.nat
+
+import std.algebra { Semiring }
+import std.magnitude { Magnitude }
+
+type Nat = Semiring<Magnitude>

src/v3/compiler/src/bootstrap_regen_fresh.rs

@@ -26,6 +26,7 @@ const BIT_DAG: &str = include_str!("../../../../dsl/std/bit.dag");
 const ERROR_PRIMITIVES_DAG: &str = include_str!("../../../../dsl/std/error_primitives.dag");
 const ALGEBRA_DAG: &str = include_str!("../../../../dsl/std/algebra.dag");
 const MAGNITUDE_DAG: &str = include_str!("../../../../dsl/std/magnitude.dag");
+const NAT_DAG: &str = include_str!("../../../../dsl/std/nat.dag");
 const INTEGER_DAG: &str = include_str!("../../../../dsl/std/integer.dag");
 const FLOAT_DAG: &str = include_str!("../../../../dsl/std/float.dag");
 const STRING_TYPE_DAG: &str = include_str!("../../../../dsl/std/string_type.dag");
@@ -138,6 +139,7 @@ fn std_fixtures() -> &'static [(&'static str, &'static str)] {
         ("dsl/std/error_primitives.dag", ERROR_PRIMITIVES_DAG),
         ("dsl/std/algebra.dag", ALGEBRA_DAG),
         ("dsl/std/magnitude.dag", MAGNITUDE_DAG),
+        ("dsl/std/nat.dag", NAT_DAG),
         ("dsl/std/integer.dag", INTEGER_DAG),
         ("dsl/std/float.dag", FLOAT_DAG),
         ("dsl/std/types.dag", TYPES_DAG),