version bumps, MAX_RECV_SEEN patch, FIPS interop, doc updates

Abstract.md

@@ -646,14 +646,11 @@ recv_seen, prev_recv_seen, local_fp, remote_fp, epoch)
 - (d) s = 0 ∧ sk_s set is unreachable.
 - (e) s = 0 ∧ pending = ⊥ ∧ pk_r set ∧ sk_s unset is unreachable.
 - (f) prev_ek_r is set iff prev_pk_r is set (co-presence).
-- (g) |recv_seen| ≤ MAX_RECV_SEEN; |prev_recv_seen| ≤ MAX_RECV_SEEN. Note: the
-  runtime bound allows recv_seen to reach exactly MAX_RECV_SEEN entries (the
-  check-before-insert pattern at §5.4 Step 6 passes at MAX_RECV_SEEN − 1, then
-  the insert produces MAX_RECV_SEEN). However, a state with MAX_RECV_SEEN
-  entries cannot be serialized — serialization rejects at |recv_seen| ≥
-  MAX_RECV_SEEN. The serialization invariant is therefore |recv_seen| <
-  MAX_RECV_SEEN. Models reasoning about serialization should use the strict
-  bound.
+- (g) |recv_seen| < MAX_RECV_SEEN; |prev_recv_seen| < MAX_RECV_SEEN. The
+  runtime check (§5.4 Step 6) rejects when a successful insert would push the
+  set to MAX_RECV_SEEN entries, so the live invariant matches the serialization
+  invariant: no reachable live state has MAX_RECV_SEEN or more entries, and
+  every live state is serializable on this dimension.
 - (h) local_fp ≠ remote_fp (self-messaging rejected at construction).
   Additionally, local_fp ≠ 0³² and remote_fp ≠ 0³² (all-zero fingerprint
   rejected at construction; constant-time check). Under SHA3-256 modeled as a
@@ -910,7 +907,7 @@ symmetric rollback for both operations produces an incorrect model.
    replaying a legitimate ciphertext; AEAD succeeds but the plaintext is
    discarded). These must be modeled as separate failure branches with different
    adversary capabilities.
-6. If |seen_set| ≥ MAX_RECV_SEEN: fail (ChainExhausted). seen_set ← seen_set ∪
+6. If |seen_set| + 1 ≥ MAX_RECV_SEEN: fail (ChainExhausted). seen_set ← seen_set ∪
    {n\*}. If epoch is CurrentEpoch or NewEpoch: r ← max(r, n\* + 1).
    (PreviousEpoch messages do not update r — they belong to a prior receive
    epoch, and updating the current-epoch high-water mark would corrupt