Dissolution upstream P6 — std/algebra.dag+std/nat.dag fold/cata FreeMonoid+Nat Wave-A2 [#3243 §1.1]

src/v4/DECISIONS.md

@@ -912,6 +912,22 @@ PROPOSES; it does not decide.
 
 **PR receipt:** gunbc **#3255** (P7) + on-thread **#3244** disposition history.
 
+### SL-P6-FREEMONOID-IS-EMPTY-VPRED — `std/algebra.dag` `free_monoid_is_empty` (predicate-dissolution interim)
+
+**Authority:** PR #3249 cursor review artifact #14097 plus Practice 10's post-#3258 blocking disposition rule.
+
+**Disposition:** **🟡 gated** — `fn free_monoid_is_empty` is a **Practice 10 predicate-dissolution** interim: hand `match` derives the `FreeMonoid<T> = Empty | Cons { … }` **variant discriminant** (`Empty => true; Cons => false`) where the canonical surface is a **substrate-derived `Empty`-variant projection** once the discriminant-predicate machinery exists. **Not 🟢 terminal** while a named dissolve target exists.
+
+**`feature:` gate:** coproduct **variant-discriminant predicate** substrate (generated / compiler-owned discriminant API — canonical `is_<Ctor>` / projection family).
+
+**Plan bind:** internal work node **`node://adhoc-2145db6b-69a`** (same substrate bucket as `SL-P7-NAT-IS-ZERO-VPRED`).
+
+**Dissolve-on-arrival:** replace `free_monoid_is_empty`'s **body** with the substrate-derived **Empty discriminant** when **`node://adhoc-2145db6b-69a`** closes. **Explicitly forbidden interim “fix”:** rewriting into a **`free_monoid_fold`** / generic fold carrier as **fold laundering**; under strict evaluation that also turns a discriminant query into a full-spine walk.
+
+**Live substrate tag:** one-line **`// 🟡 gated — …`** immediately precedes `fn free_monoid_is_empty` in `src/v4/std/algebra.dag`; header **`// Ledger: … SL-P6-FREEMONOID-IS-EMPTY-VPRED`**.
+
+**PR receipt:** gunbc **#3249** rework after review artifact **#14097**.
+
 ### SL-3229-INTEGER-GROUP-COMPLETION — `GroupCompletion<M>` constrained-inhabitance gap
 
 Verbatim `//` lines from merge-base `integer.dag` (lines **124–132**):

src/v4/std/algebra.dag

@@ -1,9 +1,10 @@
 // src/v4/std/algebra.dag
 // Scope: algebraic structures and canonical carrier constructions.
 // Anchor: https://en.wikipedia.org/wiki/Algebraic_structure
-// Owns: Magma, Semigroup, Monoid, CommutativeMonoid, Group, AbelianGroup, Semiring, CommutativeSemiring, Ring, CommutativeRing, OrderedRing, Field, ApproximateField, Lattice, BoundedLattice, BooleanAlgebra, FreeMonoid, free_monoid_is_empty, free_monoid_length, PointwisePower, Ordering, Homomorphism.
+// Owns: Magma, Semigroup, Monoid, CommutativeMonoid, Group, AbelianGroup, Semiring, CommutativeSemiring, Ring, CommutativeRing, OrderedRing, Field, ApproximateField, Lattice, BoundedLattice, BooleanAlgebra, FreeMonoid, free_monoid_fold, free_monoid_is_empty, free_monoid_length, PointwisePower, Ordering, Homomorphism.
 // Consumes: none.
 // Status: T-2 modeled.
+// Ledger: DECISIONS.md Part 6 — SL-P6-FREEMONOID-IS-EMPTY-VPRED.
 
 
 module v4.std.algebra
@@ -73,6 +74,13 @@ type BooleanAlgebra<T> {
 type FreeMonoid<T>
   = Empty
   | Cons { head: T, tail: FreeMonoid<T> }
+fn free_monoid_fold<T, A>(xs: FreeMonoid<T>, empty: A, cons: fn(T, A) -> A) -> A {
+  match xs {
+    Empty => empty
+    Cons { head: h, tail: t } => cons(h, free_monoid_fold(xs: t, empty: empty, cons: cons))
+  }
+}
+// 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: coproduct variant-discriminant predicate substrate — bind node://adhoc-2145db6b-69a — dissolve-on-arrival: substrate-derived Empty-variant discriminant projection; forbidden: free_monoid_fold laundering.
 fn free_monoid_is_empty<T>(xs: FreeMonoid<T>) -> Bool {
   match xs {
     Empty => true
@@ -82,10 +90,7 @@ fn free_monoid_is_empty<T>(xs: FreeMonoid<T>) -> Bool {
 
 
 fn free_monoid_length<T>(xs: FreeMonoid<T>) -> Int {
-  match xs {
-    Empty => 0
-    Cons { head: _, tail: t } => 1 + free_monoid_length(xs: t)
-  }
+  free_monoid_fold(xs: xs, empty: 0, cons: fn(_, acc) { 1 + acc })
 }
 type PointwisePower<T> {
   member: fn(T) -> Bool

src/v4/std/nat.dag

@@ -1,7 +1,7 @@
 // src/v4/std/nat.dag
 // Scope: natural numbers.
 // Anchor: https://en.wikipedia.org/wiki/Natural_number
-// Owns: Nat, nat_add, nat_mul, nat_is_zero, nat_additive_commutative_monoid, nat_semiring.
+// Owns: Nat, nat_cata, nat_add, nat_mul, nat_is_zero, nat_additive_commutative_monoid, nat_semiring.
 // Consumes: std algebra.
 // Status: T-3 modeled.
 // Ledger: DECISIONS.md Part 6 — SL-P7-NAT-IS-ZERO-VPRED.
@@ -13,17 +13,17 @@ import v4.std.algebra { Magma, Semigroup, Monoid, CommutativeMonoid, Semiring, C
 type Nat
   = Zero
   | Succ { prev: Nat }
-fn nat_add(a: Nat, b: Nat) -> Nat {
-  match a {
-    Zero => b
-    Succ { prev: p } => Succ { prev: nat_add(a: p, b: b) }
+fn nat_cata<A>(n: Nat, zero: A, succ: fn(A) -> A) -> A {
+  match n {
+    Zero => zero
+    Succ { prev: p } => succ(nat_cata(n: p, zero: zero, succ: succ))
   }
 }
+fn nat_add(a: Nat, b: Nat) -> Nat {
+  nat_cata(n: a, zero: b, succ: fn(acc) { Succ { prev: acc } })
+}
 fn nat_mul(a: Nat, b: Nat) -> Nat {
-  match a {
-    Zero => Zero
-    Succ { prev: p } => nat_add(a: b, b: nat_mul(a: p, b: b))
-  }
+  nat_cata(n: a, zero: Zero, succ: fn(acc) { nat_add(a: b, b: acc) })
 }
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: coproduct variant-discriminant predicate substrate — bind node://adhoc-2145db6b-69a — dissolve-on-arrival: substrate-derived Zero-variant discriminant projection; forbidden: nat_cata / fold launder (operator CORE 2026-05-18).
 fn nat_is_zero(n: Nat) -> Bool {