From 7caf55f9a9d0e89904409de9eb9efe3360e5c6e0 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:21:55 +0000
Subject: [PATCH 1/6] gkat-probe: encode K3 guards as Quack's T/F verdict pair
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Quack carries NULL as a validity plane and a three-valued verdict as the
masks T(φ) and F(φ) (Filter::sql_where); UNKNOWN is neither, so there is
no separate UNKNOWN bit. The probe invented one (is_t, is_u). A K3
observable is now the pair (T, F) with T ∧ F excluded; WHERE = T and
CHECK = ¬F. Same three atoms per observable, same verdicts on every flow.
a_k3_observable_is_quacks_t_f_pair failed before this change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 crates/gkat-probe/src/flow.rs      | 23 ++++++++++++----------
 crates/gkat-probe/tests/rubicon.rs | 31 ++++++++++++++++++++++++++++--
 2 files changed, 42 insertions(+), 12 deletions(-)

diff --git a/crates/gkat-probe/src/flow.rs b/crates/gkat-probe/src/flow.rs
index dbea8f77a..632c90752 100644
--- a/crates/gkat-probe/src/flow.rs
+++ b/crates/gkat-probe/src/flow.rs
@@ -24,13 +24,16 @@
 //! ## Guards and projections
 //!
 //! An observable is declared as Boolean or as three-valued (K3: T, F, U). A
-//! K3 observable occupies two primitive tests, `is_t` and `is_u`, and the
-//! atom set excludes the assignment where both hold, so it has exactly three
-//! values. A K3 observable reaches a Boolean guard only through a declared
-//! projection:
+//! K3 observable is encoded the way Quack's `Filter::sql_where` carries a
+//! three-valued verdict (`crates/lance-graph-quack/src/lib.rs`): two
+//! primitive tests, `T` (it is TRUE) and `F` (it is FALSE). The atom set
+//! excludes `T ∧ F`, so the observable has exactly three values. UNKNOWN is
+//! the atom with neither bit: presence is `T ∨ F`, as a column's validity
+//! plane is in Quack, and there is no separate UNKNOWN bit. A K3 observable
+//! reaches a Boolean guard only through a declared projection:
 //!
-//! * [`Cond::Where`]: designated `{T}`, i.e. `is_t`;
-//! * [`Cond::Check`]: designated `{T, U}`, i.e. `is_t ∨ is_u`.
+//! * [`Cond::Where`]: designated `{T}`, i.e. `T` — what Quack's `WHERE` keeps;
+//! * [`Cond::Check`]: designated `{T, U}`, i.e. `¬F`.
 //!
 //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a
 //! Boolean observable, or `Is` on a K3 one, is refused.
@@ -114,8 +117,8 @@ pub struct Signature {
 }
 
 impl Signature {
-    /// The primitive test of an observable: `is_t` for K3 (and the only test
-    /// of a Boolean), plus `is_u` for K3.
+    /// The first primitive test of an observable: `T` for K3 (followed by
+    /// `F`), or the only test of a Boolean.
     fn tests_of(&self, name: &'static str) -> Result<(Kind, u8), Refusal> {
         let mut next = 0u8;
         for (n, k) in &self.observables {
@@ -151,7 +154,7 @@ impl Signature {
                 max: crate::expr::MAX_TESTS,
             });
         }
-        // Each K3 observable excludes the assignment is_t ∧ is_u.
+        // Each K3 observable excludes the assignment T ∧ F.
         let mut constraint = BExp::True;
         let mut next = 0u8;
         for (_, k) in &self.observables {
@@ -189,7 +192,7 @@ impl Signature {
                 }
             },
             Cond::Check(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t).or(BExp::Test(t + 1)),
+                (Kind::K3, t) => BExp::Test(t + 1).negated(),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,
diff --git a/crates/gkat-probe/tests/rubicon.rs b/crates/gkat-probe/tests/rubicon.rs
index 7b0999456..99765d737 100644
--- a/crates/gkat-probe/tests/rubicon.rs
+++ b/crates/gkat-probe/tests/rubicon.rs
@@ -107,8 +107,10 @@ fn the_check_counterexample_has_an_unknown() {
     let auth = rubicon::authorized().unwrap();
     match commit_safe(&e, &atoms, REQUEST_COMMIT, &auth).unwrap() {
         gkat_probe::Safety::Unsafe { atom, .. } => {
-            // rev is tests 0 (is_t) and 1 (is_u); mul is tests 2 and 3.
-            assert!(atom.holds(1) || atom.holds(3), "{atom:?}");
+            // rev is tests 0 (T) and 1 (F); mul is tests 2 and 3. UNKNOWN is
+            // neither bit.
+            let unknown = |t: u8| !atom.holds(t) && !atom.holds(t + 1);
+            assert!(unknown(0) || unknown(2), "{atom:?}");
         }
         gkat_probe::Safety::Safe => panic!("expected unsafe"),
     }
@@ -147,3 +149,28 @@ fn undeclared_projections_are_refused() {
         Err(Refusal::UnknownObservable("nope"))
     ));
 }
+
+/// A K3 observable is encoded like Quack's `Filter::sql_where` verdict: two
+/// tests, `T` (the rows where it is TRUE) and `F` (where it is FALSE), never
+/// both. UNKNOWN is neither, so presence is `T ∨ F` and there is no separate
+/// UNKNOWN bit. WHERE keeps `T`; CHECK keeps `¬F`.
+#[test]
+fn a_k3_observable_is_quacks_t_f_pair() {
+    use gkat_probe::Atom;
+    use gkat_probe::flow::Cond;
+    let sig = rubicon::signature();
+    let atoms = sig.atoms().unwrap();
+    // rev occupies tests 0 (T) and 1 (F).
+    assert!(atoms.iter().all(|a| !(a.holds(0) && a.holds(1))));
+    let r#where = sig.guard(&Cond::Where(rubicon::REV)).unwrap();
+    let check = sig.guard(&Cond::Check(rubicon::REV)).unwrap();
+    let (t, f, u) = (Atom(0b01), Atom(0b10), Atom(0b00));
+    assert_eq!(
+        (r#where.eval(t), r#where.eval(f), r#where.eval(u)),
+        (true, false, false)
+    );
+    assert_eq!(
+        (check.eval(t), check.eval(f), check.eval(u)),
+        (true, false, true)
+    );
+}

From 3d2e220e73c73627a4089eaba869b41263bc2761 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:23:28 +0000
Subject: [PATCH 2/6] board: D-GKAT-0 shipped (#1676); K3 encoding note

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 .claude/board/PR_ARC_INVENTORY.md                  | 7 +++++++
 .claude/board/STATUS_BOARD.md                      | 2 +-
 .claude/board/entries/2026-10-21-d-gkat-0-probe.md | 6 +++---
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md
index 169322753..1b9fc5391 100644
--- a/.claude/board/PR_ARC_INVENTORY.md
+++ b/.claude/board/PR_ARC_INVENTORY.md
@@ -1,3 +1,10 @@
+## 2026-10-21 — lance-graph PR #1676 (merged `6d7442c4`, branch `ccr-d3ce1263-ied9yh`, head `bccff823`) — D-GKAT-0: PROBE, bounded GKAT checking of structured Rubicon flows
+
+- **Added:** lab crate `crates/gkat-probe` (zero deps, own workspace, excluded): `expr::{Action, Atom, Atoms, BExp, Exp, Refusal, MAX_TESTS}`, `automaton::{thompson, equivalent, commit_safe, Equivalence, Safety, Out}`, `oracle::{explore, same_up_to, unsafe_within, deterministic}`, `flow::{Kind, Cond, Step, Signature, Flow, flows_equivalent}`, `rubicon` fixtures; `.github/workflows/gkat-probe.yml`; entry `2026-10-21-d-gkat-0-probe.md`.
+- **Locked:** the admitted fragment (skip, fail, assert, action, sequence, `if`, `while`) over at most 8 primitive tests; unguarded choice, `GoTo`/`GoBack`, undeclared tests, actions or projections and mismatched signatures are refused, never translated. Equivalence (Thompson + normalization + union-find bisimulation) and commit safety (WHERE(rev) ∧ WHERE(mul) immediately before every `RequestCommit`, fixed by the checker) are separate checks.
+- **Deferred / open:** D-LFA-1 runtime (unclaimed; handoff in EXO-50 `/028`); symbolic guards past 8 tests; G3/G4/G6/G7. Merged by the operator before the Codex re-review of `bccff823` and two workspace jobs finished; the re-review came back clean and no main job failed.
+- **Confidence:** TEST-PINNED, not proven. 28 tests; 11 checker disables red; 2 Codex P2s (fixed-budget divergence, determinacy without acceptance) fixed failing-first; CI green on `55c64a44`.
+
 ## 2026-10-21 — lance-graph PR #1674 (merged `414377f3`, branch `ccr-f5674497-orfkox`, head `ed54930e`) — D-TGB-4: thought-git receipt and deterministic replay
 
 - **Added:** `thought_git_probe::receipt::{BaseRef, VersionStore, ProgramId, DERIVE, ProgramInputs, ExecConfig, EXEC_DEFAULT, Fold, Receipt, ReceiptIdentity, Refusal, Plan, capture, Replayed, replay, replay_live, MetaKey, MetaRow, MetadataTable}`; `tests/receipt.rs` (10 falsifiers); `.github/workflows/thought-git-probe.yml` (first CI line for the crate); entry `2026-10-21-d-tgb-4-receipt-replay.md`.
diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md
index 92a317e2f..b670fe34b 100644
--- a/.claude/board/STATUS_BOARD.md
+++ b/.claude/board/STATUS_BOARD.md
@@ -8,7 +8,7 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac
 | **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) |
 | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
 | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed |
-| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | In PR, PROBE (EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused | 3 flow disables + 11 checker disables red; independent bounded oracle; not a production verifier |
+| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards use Quack's T/F verdict pair (follow-up) | 3 flow disables + 12 checker disables red; independent bounded oracle; not a production verifier |
 
 ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20)
 
diff --git a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
index 07e7e76cb..2cea106a0 100644
--- a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
+++ b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
@@ -26,10 +26,10 @@
 | choice without a condition | `Refusal::UnguardedChoice` |
 
 **K3 guards.**
-- A K3 observable occupies two primitive tests, `is_t` and `is_u`. The atom set excludes `is_t ∧ is_u`, which leaves exactly three values.
+- A K3 observable occupies two primitive tests, `T` and `F`, encoded like Quack's `Filter::sql_where` verdict masks. The atom set excludes `T ∧ F`, which leaves exactly three values; UNKNOWN is neither bit, so presence is `T ∨ F` and there is no separate UNKNOWN bit. (The first version used `is_t`/`is_u`; changed after review, see the follow-up PR.)
 - A K3 guard reaches a Boolean test only through a declared projection:
-  - `Where` = `{T}`
-  - `Check` = `{T,U}`
+  - `Where` = `{T}` = `T`
+  - `Check` = `{T,U}` = `¬F`
   - `Is` applies to Boolean observables only.
 - Any other pairing of projection and observable is refused.
 

From 5a0bf3f06a782ba80b0a5773abf6d23e2e33f5fc Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:30:45 +0000
Subject: [PATCH 3/6] gkat-probe: a K3 guard is a value bit and a presence bit

The previous commit encoded a K3 observable as a T/F verdict pair, which
is not how the substrate stores it. Quack stores a nullable column as a
value lane plus a validity bit; a cleared validity bit is NULL and its
value is 0. A K3 observable is now exactly that: (value, valid) with
value -> valid. WHERE = value, CHECK = value | !valid.
a_k3_observable_is_a_value_bit_and_a_presence_bit failed before this.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 crates/gkat-probe/src/flow.rs      | 34 +++++++++++++++++-------------
 crates/gkat-probe/tests/rubicon.rs | 27 ++++++++++++------------
 2 files changed, 33 insertions(+), 28 deletions(-)

diff --git a/crates/gkat-probe/src/flow.rs b/crates/gkat-probe/src/flow.rs
index 632c90752..23ce8c240 100644
--- a/crates/gkat-probe/src/flow.rs
+++ b/crates/gkat-probe/src/flow.rs
@@ -24,16 +24,17 @@
 //! ## Guards and projections
 //!
 //! An observable is declared as Boolean or as three-valued (K3: T, F, U). A
-//! K3 observable is encoded the way Quack's `Filter::sql_where` carries a
-//! three-valued verdict (`crates/lance-graph-quack/src/lib.rs`): two
-//! primitive tests, `T` (it is TRUE) and `F` (it is FALSE). The atom set
-//! excludes `T ∧ F`, so the observable has exactly three values. UNKNOWN is
-//! the atom with neither bit: presence is `T ∨ F`, as a column's validity
-//! plane is in Quack, and there is no separate UNKNOWN bit. A K3 observable
-//! reaches a Boolean guard only through a declared projection:
+//! K3 observable is a Quack nullable column (`crates/lance-graph-quack`,
+//! `Filter::sql_where`): a **value** bit and a **presence** (validity) bit,
+//! and nothing else. A cleared presence bit is NULL; the atom set excludes a
+//! set value without presence, so a NULL's value is deterministically 0. The
+//! three atoms are `value 1, valid 1` = TRUE, `value 0, valid 1` = FALSE and
+//! `value 0, valid 0` = NULL (UNKNOWN). A K3 observable reaches a Boolean
+//! guard only through a declared projection:
 //!
-//! * [`Cond::Where`]: designated `{T}`, i.e. `T` — what Quack's `WHERE` keeps;
-//! * [`Cond::Check`]: designated `{T, U}`, i.e. `¬F`.
+//! * [`Cond::Where`]: designated `{T}`, i.e. `value` — what Quack's `WHERE`
+//!   keeps, since a set value implies presence;
+//! * [`Cond::Check`]: designated `{T, U}`, i.e. `value ∨ ¬valid`.
 //!
 //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a
 //! Boolean observable, or `Is` on a K3 one, is refused.
@@ -117,8 +118,8 @@ pub struct Signature {
 }
 
 impl Signature {
-    /// The first primitive test of an observable: `T` for K3 (followed by
-    /// `F`), or the only test of a Boolean.
+    /// The first primitive test of an observable: the value bit for K3
+    /// (followed by its presence bit), or the only test of a Boolean.
     fn tests_of(&self, name: &'static str) -> Result<(Kind, u8), Refusal> {
         let mut next = 0u8;
         for (n, k) in &self.observables {
@@ -154,15 +155,18 @@ impl Signature {
                 max: crate::expr::MAX_TESTS,
             });
         }
-        // Each K3 observable excludes the assignment T ∧ F.
+        // Each K3 observable excludes a set value without presence: NULL is 0.
         let mut constraint = BExp::True;
         let mut next = 0u8;
         for (_, k) in &self.observables {
             match k {
                 Kind::Bool => next += 1,
                 Kind::K3 => {
-                    constraint =
-                        constraint.and(BExp::Test(next).and(BExp::Test(next + 1)).negated());
+                    constraint = constraint.and(
+                        BExp::Test(next)
+                            .and(BExp::Test(next + 1).negated())
+                            .negated(),
+                    );
                     next += 2;
                 }
             }
@@ -192,7 +196,7 @@ impl Signature {
                 }
             },
             Cond::Check(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t + 1).negated(),
+                (Kind::K3, t) => BExp::Test(t).or(BExp::Test(t + 1).negated()),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,
diff --git a/crates/gkat-probe/tests/rubicon.rs b/crates/gkat-probe/tests/rubicon.rs
index 99765d737..0a2b02b11 100644
--- a/crates/gkat-probe/tests/rubicon.rs
+++ b/crates/gkat-probe/tests/rubicon.rs
@@ -107,9 +107,9 @@ fn the_check_counterexample_has_an_unknown() {
     let auth = rubicon::authorized().unwrap();
     match commit_safe(&e, &atoms, REQUEST_COMMIT, &auth).unwrap() {
         gkat_probe::Safety::Unsafe { atom, .. } => {
-            // rev is tests 0 (T) and 1 (F); mul is tests 2 and 3. UNKNOWN is
-            // neither bit.
-            let unknown = |t: u8| !atom.holds(t) && !atom.holds(t + 1);
+            // rev is tests 0 (value) and 1 (presence); mul is tests 2 and 3.
+            // UNKNOWN is a cleared presence bit.
+            let unknown = |t: u8| !atom.holds(t + 1);
             assert!(unknown(0) || unknown(2), "{atom:?}");
         }
         gkat_probe::Safety::Safe => panic!("expected unsafe"),
@@ -150,27 +150,28 @@ fn undeclared_projections_are_refused() {
     ));
 }
 
-/// A K3 observable is encoded like Quack's `Filter::sql_where` verdict: two
-/// tests, `T` (the rows where it is TRUE) and `F` (where it is FALSE), never
-/// both. UNKNOWN is neither, so presence is `T ∨ F` and there is no separate
-/// UNKNOWN bit. WHERE keeps `T`; CHECK keeps `¬F`.
+/// A K3 observable is a Quack nullable column: a value bit and a presence
+/// (validity) bit, and nothing else. A cleared presence bit forces the value
+/// to 0, so `value 0, valid 0` is NULL (UNKNOWN), `value 0, valid 1` is FALSE
+/// and `value 1, valid 1` is TRUE. WHERE keeps TRUE; CHECK rejects only FALSE.
 #[test]
-fn a_k3_observable_is_quacks_t_f_pair() {
+fn a_k3_observable_is_a_value_bit_and_a_presence_bit() {
     use gkat_probe::Atom;
     use gkat_probe::flow::Cond;
     let sig = rubicon::signature();
     let atoms = sig.atoms().unwrap();
-    // rev occupies tests 0 (T) and 1 (F).
-    assert!(atoms.iter().all(|a| !(a.holds(0) && a.holds(1))));
+    // rev occupies tests 0 (value) and 1 (presence): no value without presence.
+    assert!(atoms.iter().all(|a| !a.holds(0) || a.holds(1)));
+    assert!(atoms.iter().any(|a| !a.holds(1)), "NULL must be an atom");
     let r#where = sig.guard(&Cond::Where(rubicon::REV)).unwrap();
     let check = sig.guard(&Cond::Check(rubicon::REV)).unwrap();
-    let (t, f, u) = (Atom(0b01), Atom(0b10), Atom(0b00));
+    let (t, f, null) = (Atom(0b11), Atom(0b10), Atom(0b00));
     assert_eq!(
-        (r#where.eval(t), r#where.eval(f), r#where.eval(u)),
+        (r#where.eval(t), r#where.eval(f), r#where.eval(null)),
         (true, false, false)
     );
     assert_eq!(
-        (check.eval(t), check.eval(f), check.eval(u)),
+        (check.eval(t), check.eval(f), check.eval(null)),
         (true, false, true)
     );
 }

From 894e88e36f7cd563bbf01e6f87e9f85dda6786f2 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:31:53 +0000
Subject: [PATCH 4/6] board: D-GKAT-0 K3 encoding is value + presence

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 .claude/board/STATUS_BOARD.md                      | 2 +-
 .claude/board/entries/2026-10-21-d-gkat-0-probe.md | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md
index b670fe34b..750bb3f7f 100644
--- a/.claude/board/STATUS_BOARD.md
+++ b/.claude/board/STATUS_BOARD.md
@@ -8,7 +8,7 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac
 | **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) |
 | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
 | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed |
-| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards use Quack's T/F verdict pair (follow-up) | 3 flow disables + 12 checker disables red; independent bounded oracle; not a production verifier |
+| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards are a value bit plus a presence bit, as Quack's nullable columns (#1679) | 3 flow disables + 12 checker disables red; independent bounded oracle; not a production verifier |
 
 ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20)
 
diff --git a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
index 2cea106a0..6e35386dd 100644
--- a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
+++ b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
@@ -26,10 +26,10 @@
 | choice without a condition | `Refusal::UnguardedChoice` |
 
 **K3 guards.**
-- A K3 observable occupies two primitive tests, `T` and `F`, encoded like Quack's `Filter::sql_where` verdict masks. The atom set excludes `T ∧ F`, which leaves exactly three values; UNKNOWN is neither bit, so presence is `T ∨ F` and there is no separate UNKNOWN bit. (The first version used `is_t`/`is_u`; changed after review, see the follow-up PR.)
+- A K3 observable is a Quack nullable column: a value bit and a presence (validity) bit, nothing else. A cleared presence bit is NULL and forces the value to 0 (the atom set excludes a value without presence), which leaves exactly three values: TRUE `(1,1)`, FALSE `(0,1)`, NULL `(0,0)`. (#1676 used `is_t`/`is_u`, an UNKNOWN bit Quack does not have; #1679 replaced it.)
 - A K3 guard reaches a Boolean test only through a declared projection:
-  - `Where` = `{T}` = `T`
-  - `Check` = `{T,U}` = `¬F`
+  - `Where` = `{T}` = `value`
+  - `Check` = `{T,U}` = `value ∨ ¬valid`
   - `Is` applies to Boolean observables only.
 - Any other pairing of projection and observable is refused.
 

From 169647cd5119cb97325533583e7cf6eacf60ed23 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:38:44 +0000
Subject: [PATCH 5/6] gkat-probe: a K3 leaf never reads the payload of a NULL

A K3 observable is now two tests, the leaf and validity, with no
constraint between them. The leaf is the Boolean read off the stored value:
the bit itself for a BOOLEAN column, a comparison for a numeric or text one.
Under a cleared validity bit the payload is arbitrary (Quack
Filter::sql_where; PostgreSQL stores no value), so all four pairs are atoms
and NULL is the two with valid = 0.

The previous encoding forced the payload to 0 under NULL and lowered Where
as the bare leaf, so it read the payload wherever that assumption failed.
Where is now valid AND leaf, Check is NOT valid OR leaf, matching
sql_where's T and NOT F.

New test a_k3_guard_never_reads_the_payload_of_a_null failed before the fix.
Rubicon has 64 atoms; every equivalence and safety verdict is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 crates/gkat-probe/src/flow.rs       | 53 ++++++++++++-----------------
 crates/gkat-probe/src/rubicon.rs    |  2 +-
 crates/gkat-probe/tests/g5_atoms.rs |  5 +--
 crates/gkat-probe/tests/rubicon.rs  | 48 ++++++++++++++++----------
 4 files changed, 56 insertions(+), 52 deletions(-)

diff --git a/crates/gkat-probe/src/flow.rs b/crates/gkat-probe/src/flow.rs
index 23ce8c240..e35605162 100644
--- a/crates/gkat-probe/src/flow.rs
+++ b/crates/gkat-probe/src/flow.rs
@@ -24,17 +24,22 @@
 //! ## Guards and projections
 //!
 //! An observable is declared as Boolean or as three-valued (K3: T, F, U). A
-//! K3 observable is a Quack nullable column (`crates/lance-graph-quack`,
-//! `Filter::sql_where`): a **value** bit and a **presence** (validity) bit,
-//! and nothing else. A cleared presence bit is NULL; the atom set excludes a
-//! set value without presence, so a NULL's value is deterministically 0. The
-//! three atoms are `value 1, valid 1` = TRUE, `value 0, valid 1` = FALSE and
-//! `value 0, valid 0` = NULL (UNKNOWN). A K3 observable reaches a Boolean
-//! guard only through a declared projection:
+//! K3 observable is a leaf over a nullable column (`crates/lance-graph-quack`,
+//! `Filter::sql_where`): the column's stored value plus its validity plane.
+//! The leaf is the Boolean read off the stored value, and what that means
+//! depends on the column's type. For a `BOOLEAN` column the leaf is the stored
+//! bit itself (in Quack, a mask plane). For a numeric or text column it is a
+//! comparison such as `rev = 5`, and 0 and 1 in the lane are ordinary
+//! numbers. Either way the observable occupies two tests: `leaf` and `valid`.
+//! Under `valid = 0` no value is stored (PostgreSQL) or the payload is
+//! arbitrary (Quack), so the leaf there reads nothing meaningful. There is no
+//! constraint between the two tests: all four pairs are atoms, and NULL is the
+//! two with `valid = 0`. A K3 observable reaches a Boolean guard only through
+//! a declared projection, and neither projection reads the leaf under a NULL:
 //!
-//! * [`Cond::Where`]: designated `{T}`, i.e. `value` — what Quack's `WHERE`
-//!   keeps, since a set value implies presence;
-//! * [`Cond::Check`]: designated `{T, U}`, i.e. `value ∨ ¬valid`.
+//! * [`Cond::Where`]: designated `{T}`, i.e. `T(φ) = valid ∧ leaf`, what
+//!   Quack's `WHERE` keeps;
+//! * [`Cond::Check`]: designated `{T, U}`, i.e. `¬F(φ) = ¬valid ∨ leaf`.
 //!
 //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a
 //! Boolean observable, or `Is` on a K3 one, is refused.
@@ -118,8 +123,8 @@ pub struct Signature {
 }
 
 impl Signature {
-    /// The first primitive test of an observable: the value bit for K3
-    /// (followed by its presence bit), or the only test of a Boolean.
+    /// The first primitive test of an observable: the leaf for K3
+    /// (followed by its validity bit), or the only test of a Boolean.
     fn tests_of(&self, name: &'static str) -> Result<(Kind, u8), Refusal> {
         let mut next = 0u8;
         for (n, k) in &self.observables {
@@ -155,23 +160,9 @@ impl Signature {
                 max: crate::expr::MAX_TESTS,
             });
         }
-        // Each K3 observable excludes a set value without presence: NULL is 0.
-        let mut constraint = BExp::True;
-        let mut next = 0u8;
-        for (_, k) in &self.observables {
-            match k {
-                Kind::Bool => next += 1,
-                Kind::K3 => {
-                    constraint = constraint.and(
-                        BExp::Test(next)
-                            .and(BExp::Test(next + 1).negated())
-                            .negated(),
-                    );
-                    next += 2;
-                }
-            }
-        }
-        Atoms::new(tests, &constraint)
+        // No constraint: under a NULL the stored payload, and so the leaf, is
+        // arbitrary. The guards, not the atom set, make NULL one value.
+        Atoms::new(tests, &BExp::True)
     }
 
     /// Lowers a condition to a Boolean test.
@@ -187,7 +178,7 @@ impl Signature {
                 }
             },
             Cond::Where(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t),
+                (Kind::K3, t) => BExp::Test(t + 1).and(BExp::Test(t)),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,
@@ -196,7 +187,7 @@ impl Signature {
                 }
             },
             Cond::Check(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t).or(BExp::Test(t + 1).negated()),
+                (Kind::K3, t) => BExp::Test(t + 1).negated().or(BExp::Test(t)),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,
diff --git a/crates/gkat-probe/src/rubicon.rs b/crates/gkat-probe/src/rubicon.rs
index 63df8d974..b78a18294 100644
--- a/crates/gkat-probe/src/rubicon.rs
+++ b/crates/gkat-probe/src/rubicon.rs
@@ -39,7 +39,7 @@ pub const DELIBERATE_NEEDED: &str = "deliberate";
 /// Whether external input is ready at resume.
 pub const INPUT_READY: &str = "input";
 
-/// 6 primitive tests: rev (2), mul (2), deliberate (1), input (1); 36 atoms.
+/// 6 primitive tests: rev (2), mul (2), deliberate (1), input (1); 64 atoms.
 pub fn signature() -> Signature {
     Signature {
         observables: vec![
diff --git a/crates/gkat-probe/tests/g5_atoms.rs b/crates/gkat-probe/tests/g5_atoms.rs
index cf84d49e5..dfe7416d1 100644
--- a/crates/gkat-probe/tests/g5_atoms.rs
+++ b/crates/gkat-probe/tests/g5_atoms.rs
@@ -9,13 +9,14 @@ fn atom_counts_are_exact() {
     for k in 0..=MAX_TESTS as usize {
         assert_eq!(Atoms::new(k, &BExp::True).unwrap().len(), 1 << k);
     }
-    // A K3 observable occupies two tests and has three values.
+    // A K3 observable occupies two tests (leaf, valid) with no constraint:
+    // four atoms, of which the two with valid = 0 are one value, NULL.
     let sig = |n: usize| Signature {
         observables: (0..n).map(|_| ("x", Kind::K3)).collect(),
         actions: vec![],
     };
     for n in 0..=4 {
-        assert_eq!(sig(n).atoms().unwrap().len(), 3usize.pow(n as u32));
+        assert_eq!(sig(n).atoms().unwrap().len(), 4usize.pow(n as u32));
     }
 }
 
diff --git a/crates/gkat-probe/tests/rubicon.rs b/crates/gkat-probe/tests/rubicon.rs
index 0a2b02b11..669894467 100644
--- a/crates/gkat-probe/tests/rubicon.rs
+++ b/crates/gkat-probe/tests/rubicon.rs
@@ -7,7 +7,7 @@ use gkat_probe::rubicon::{self, REQUEST_COMMIT};
 use gkat_probe::{Refusal, commit_safe};
 
 /// Oracle bound: two actions covers Deliberate or one Suspend, followed by
-/// the decision. With 36 atoms that is 36^3 runs per flow.
+/// the decision. With 64 atoms that is 64^3 runs per flow.
 const BOUND: usize = 2;
 
 fn safe(flow: &gkat_probe::flow::Flow) -> bool {
@@ -42,8 +42,9 @@ fn equivalent(a: &gkat_probe::flow::Flow, b: &gkat_probe::flow::Flow) -> bool {
 }
 
 #[test]
-fn the_signature_declares_36_atoms() {
-    assert_eq!(rubicon::signature().atoms().unwrap().len(), 36);
+fn the_signature_declares_64_atoms() {
+    // Two K3 observables (4 atoms each) and two Booleans.
+    assert_eq!(rubicon::signature().atoms().unwrap().len(), 64);
 }
 
 #[test]
@@ -107,8 +108,8 @@ fn the_check_counterexample_has_an_unknown() {
     let auth = rubicon::authorized().unwrap();
     match commit_safe(&e, &atoms, REQUEST_COMMIT, &auth).unwrap() {
         gkat_probe::Safety::Unsafe { atom, .. } => {
-            // rev is tests 0 (value) and 1 (presence); mul is tests 2 and 3.
-            // UNKNOWN is a cleared presence bit.
+            // rev is tests 0 (leaf) and 1 (valid); mul is tests 2 and 3.
+            // UNKNOWN is a cleared validity bit.
             let unknown = |t: u8| !atom.holds(t + 1);
             assert!(unknown(0) || unknown(2), "{atom:?}");
         }
@@ -150,28 +151,39 @@ fn undeclared_projections_are_refused() {
     ));
 }
 
-/// A K3 observable is a Quack nullable column: a value bit and a presence
-/// (validity) bit, and nothing else. A cleared presence bit forces the value
-/// to 0, so `value 0, valid 0` is NULL (UNKNOWN), `value 0, valid 1` is FALSE
-/// and `value 1, valid 1` is TRUE. WHERE keeps TRUE; CHECK rejects only FALSE.
+/// A K3 observable is a leaf over a nullable column: the Boolean read off the
+/// stored value (the bit itself for a `BOOLEAN` column, a comparison for a
+/// numeric one) and the validity bit. Under `valid = 0` the payload is
+/// arbitrary (Quack, `Filter::sql_where`), so the leaf there reads nothing.
+/// All four `(leaf, valid)` pairs are atoms, NULL is the two with `valid = 0`,
+/// and no guard may tell those two apart.
 #[test]
-fn a_k3_observable_is_a_value_bit_and_a_presence_bit() {
+fn a_k3_guard_never_reads_the_payload_of_a_null() {
     use gkat_probe::Atom;
     use gkat_probe::flow::Cond;
     let sig = rubicon::signature();
     let atoms = sig.atoms().unwrap();
-    // rev occupies tests 0 (value) and 1 (presence): no value without presence.
-    assert!(atoms.iter().all(|a| !a.holds(0) || a.holds(1)));
-    assert!(atoms.iter().any(|a| !a.holds(1)), "NULL must be an atom");
+    // rev occupies tests 0 (leaf) and 1 (valid). A NULL with either payload
+    // is an atom: nothing forces the lane to 0.
+    assert!(atoms.iter().any(|a| a.holds(0) && !a.holds(1)));
+    assert!(atoms.iter().any(|a| !a.holds(0) && !a.holds(1)));
+    for g in [Cond::Where(rubicon::REV), Cond::Check(rubicon::REV)] {
+        let b = sig.guard(&g).unwrap();
+        for a in atoms.iter().filter(|a| !a.holds(1)) {
+            let flipped = Atom(a.0 ^ 1);
+            assert_eq!(b.eval(a), b.eval(flipped), "{g:?} reads a NULL payload");
+        }
+    }
     let r#where = sig.guard(&Cond::Where(rubicon::REV)).unwrap();
     let check = sig.guard(&Cond::Check(rubicon::REV)).unwrap();
-    let (t, f, null) = (Atom(0b11), Atom(0b10), Atom(0b00));
+    // (leaf, valid): TRUE = (1,1), FALSE = (0,1), NULL = (_,0).
+    let (t, f, null0, null1) = (Atom(0b11), Atom(0b10), Atom(0b00), Atom(0b01));
     assert_eq!(
-        (r#where.eval(t), r#where.eval(f), r#where.eval(null)),
-        (true, false, false)
+        [t, f, null0, null1].map(|a| r#where.eval(a)),
+        [true, false, false, false]
     );
     assert_eq!(
-        (check.eval(t), check.eval(f), check.eval(null)),
-        (true, false, true)
+        [t, f, null0, null1].map(|a| check.eval(a)),
+        [true, false, true, true]
     );
 }

From 515a3997a4e08723989d8168fe0ee31d0e04d00d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 21 Oct 2026 20:40:01 +0000
Subject: [PATCH 6/6] board: D-GKAT-0 K3 leaf is payload-blind under NULL

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
---
 .claude/board/STATUS_BOARD.md                  |  2 +-
 .../board/entries/2026-10-21-d-gkat-0-probe.md | 18 +++++++++++-------
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md
index 750bb3f7f..ac73bbf2d 100644
--- a/.claude/board/STATUS_BOARD.md
+++ b/.claude/board/STATUS_BOARD.md
@@ -8,7 +8,7 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac
 | **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) |
 | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
 | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed |
-| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards are a value bit plus a presence bit, as Quack's nullable columns (#1679) | 3 flow disables + 12 checker disables red; independent bounded oracle; not a production verifier |
+| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards are a leaf plus a validity bit and never read the payload of a NULL, as Quack's `sql_where` (#1679) | 3 flow disables + 15 checker disables red; independent bounded oracle; not a production verifier |
 
 ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20)
 
diff --git a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
index 6e35386dd..e63c073ba 100644
--- a/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
+++ b/.claude/board/entries/2026-10-21-d-gkat-0-probe.md
@@ -26,10 +26,13 @@
 | choice without a condition | `Refusal::UnguardedChoice` |
 
 **K3 guards.**
-- A K3 observable is a Quack nullable column: a value bit and a presence (validity) bit, nothing else. A cleared presence bit is NULL and forces the value to 0 (the atom set excludes a value without presence), which leaves exactly three values: TRUE `(1,1)`, FALSE `(0,1)`, NULL `(0,0)`. (#1676 used `is_t`/`is_u`, an UNKNOWN bit Quack does not have; #1679 replaced it.)
+- A K3 observable is a leaf over a nullable column, and it occupies two tests: `leaf` and `valid`.
+  - The leaf is the Boolean read off the stored value: the bit itself for a `BOOLEAN` column, a comparison such as `rev = 5` for a numeric one.
+  - Under `valid = 0` the payload is arbitrary (Quack `Filter::sql_where`; PostgreSQL stores none). There is no constraint between the two tests, so NULL is two atoms.
+  - History: #1676 used `is_t`/`is_u`, an UNKNOWN bit Quack does not have. #1679 first replaced it with a value bit forced to 0 under NULL; that assumption is also false, and it was dropped.
 - A K3 guard reaches a Boolean test only through a declared projection:
-  - `Where` = `{T}` = `value`
-  - `Check` = `{T,U}` = `value ∨ ¬valid`
+  - `Where` = `{T}` = `valid ∧ leaf`
+  - `Check` = `{T,U}` = `¬valid ∨ leaf`; neither reads the leaf under a NULL
   - `Is` applies to Boolean observables only.
 - Any other pairing of projection and observable is refused.
 
@@ -47,7 +50,7 @@
 - **Oracle** (`oracle.rs`): an independent operational interpreter of the expression AST that shares no code with the automaton. It explores every run exhaustively up to a stated action bound.
   Divergence is detected exactly, by a repeated continuation stack at a loop head, not by a step budget. The first version used a fixed budget, which Codex showed misclassifies a terminating run of 2^14 silent steps.
 
-## Measured (`cargo test`, 28 tests)
+## Measured (`cargo test`, 29 tests)
 
 - **G1.** `if b then {p;q} else {q}` ≡ `(if b then {p} else {skip}); q`. The oracle agrees at bounds 0–4. A changed action label is rejected, a reversed guard is rejected, and a different tail is rejected. `p·0 ≡ 0` (normalization).
 - **G2.** Rejections:
@@ -57,11 +60,11 @@
 
   So does the union of `skip` and `p`: on one atom it may either accept or act. The admitted Rubicon flows are deterministic.
 - **G5.**
-  - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `3^n` atoms exactly.
+  - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `4^n` atoms exactly (three values each).
   - `k = 9` is refused (`AtomBound`). A DR64-shaped signature (64 Boolean lanes) is refused, as is one with 5 K3 observables (10 tests).
   - On a chain of `k` guards, the automaton has `2k` states while the atom count is `2^k`. Measured (k, atoms, states, merged pairs): (1,2,2,3) … (8,256,16,17).
   - Counts only, no timings (the workspace's no-ms rule).
-- **Rubicon** (11 tests, 36 atoms).
+- **Rubicon** (12 tests, 64 atoms).
   - The reference flow has the decision tail written out twice; the optimized flow factors it out (G1) and reorders the decision. The two are **equivalent**, and both are **safe**.
   - Disable runs on the flows:
     - reversed authorization polarity → equivalence fails;
@@ -85,7 +88,8 @@
   - atom bound raised to 64;
   - uniform sequence continuation not patched;
   - signature mismatch not refused;
-  - K3 exclusion dropped.
+  - K3 `Where` ungated (only the payload test catches it: flow and authorization share the lowering);
+  - K3 `Check` lowered as the leaf, `Where` as validity, `Check` as `Where`.
 
   The first normalization disable stayed green because no test compared a step into a dead state with a rejection. `a_step_into_a_dead_state_is_a_rejection` was added to close that gap.