diff --git a/docs/research/2026-05-03-math-proofs-honest-assessment.md b/docs/research/2026-05-03-math-proofs-honest-assessment.md
index 726a03f69..08188d1f2 100644
--- a/docs/research/2026-05-03-math-proofs-honest-assessment.md
+++ b/docs/research/2026-05-03-math-proofs-honest-assessment.md
@@ -295,7 +295,7 @@ to publishable form:
 | `.cfg` for 4 C1 specs | C1 → B | 2 days | P2 | open |
 | TLA+ spec for `Recursive.fs` LFP | C2 → B | 2-3 days | P2 | open |
 | TLA+ spec for WDC protocol | C2 → B | 3-5 days | P1 | open |
-| 15 FsCheck properties (C3) | C3 → B | 3 days | P2 | open |
+| 15 FsCheck properties (C3) | C3 → B | 3 days | P2 | **Partial (3 of 15): PN-counter merge commutative + idempotent + associative ✓ this PR (mirrors G-counter pattern in `Math.Invariants.Tests.fs`). Remaining ~12 properties: OR-Set + LWW-Register + DeltaCrdt + Residuated lattice + Recursive fixpoint + Merkle + Watermark + KLL** |
 | `chain_rule_poly` (3-group) | C4 → A | research | P3 | open |
 | Registry rows for A4 specs | external-fidelity claim | 1 day | P0 | **Done (PR #1393, 2026-05-03)** |
 | Peer-review email draft | publishability | 2 hours | P0 | **Done (PR #1387, 2026-05-03)** |
diff --git a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs
index 2e5574729..f4985f048 100644
--- a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs
+++ b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs
@@ -71,6 +71,37 @@ let ``G-counter merge is associative`` (NonNegativeInt a) (NonNegativeInt b) (No
     lhs.Value = rhs.Value
 
 
+// ─── PN-Counter — semilattice laws (positive + negative G-counters) ─
+// PN-Counter merges elementwise: P-side max-merge + N-side max-merge.
+// The semilattice laws (commute / idempotent / associative) inherit
+// from G-counter directly because PN.Merge is just (G-merge,G-merge).
+// These properties pin that derivation: any future change to PNCounter
+// that breaks one of the laws (e.g. accidentally min-merging instead
+// of max-merging) trips a property here.
+
+[<Property>]
+let ``PN-counter merge is commutative`` (aP: int) (aN: int) (bP: int) (bN: int) =
+    // Bound to non-negative for Increment's contract; PN allows
+    // both positive (P side) and negative (N side) deltas.
+    let a = PNCounter.Empty.Increment("r1", int64 (abs aP)).Increment("r1", -(int64 (abs aN)))
+    let b = PNCounter.Empty.Increment("r2", int64 (abs bP)).Increment("r2", -(int64 (abs bN)))
+    (PNCounter.Merge a b).Value = (PNCounter.Merge b a).Value
+
+[<Property>]
+let ``PN-counter merge is idempotent`` (p: int) (n: int) =
+    let a = PNCounter.Empty.Increment("r1", int64 (abs p)).Increment("r1", -(int64 (abs n)))
+    (PNCounter.Merge a a).Value = a.Value
+
+[<Property>]
+let ``PN-counter merge is associative`` (a: int) (b: int) (c: int) =
+    let x = PNCounter.Empty.Increment("r1", int64 (abs a))
+    let y = PNCounter.Empty.Increment("r2", int64 (abs b))
+    let z = PNCounter.Empty.Increment("r3", int64 (abs c))
+    let lhs = PNCounter.Merge (PNCounter.Merge x y) z
+    let rhs = PNCounter.Merge x (PNCounter.Merge y z)
+    lhs.Value = rhs.Value
+
+
 // ─── HyperMinHash — Jaccard monotonicity ───────────────────────────
 // Reference: Yu & Weber arXiv:1710.08436.