@@ -1,11 +1,13 @@
 ## D-RFT / D-QSP — ClassView × Quack semantic substrate (2026-10-21)
 
-Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`; docs, not yet on main). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them.
+Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`, `d-lfa-lance-graph-flow-rubicon-assimilation-v1.md`; merged). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them.
 
 | D-id | scope | status | gate / falsifier |
 |---|---|---|---|
-| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | In PR (EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` |
+| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | Shipped (#1668; EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` |
 | **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 | Queued, unclaimed (research only; no runtime, dependency or executor) | the three fixtures in the D-LFA plan amendment |
 
 ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20)
 
 
@@ -70,6 +70,8 @@ All probes compare counts or scalar folds.
 | P-ABA-MODDEL | Modify on one side and delete on the other is a named refusal | It resolves silently |
 | P-REFUSAL-KIND | A RouteRefusal is retried on another route. A SemanticRefusal is never retried. | A semantic refusal is retried |
 | P-TLP-COUNT | The counts for P, NOT P and P IS NULL sum to the table's row count | The sum differs |
+| D-GKAT-0 (added 2026-10-21, after #1670) | GKAT fixtures: G1 guarded factoring, G2 refusal of genuine nondeterminism, G5 a declared atom bound. No runtime, dependency or executor. | A G1 rewrite with a changed label or polarity is accepted; nondeterminism is encoded as an `if` |
+| P-GKAT-RUBICON (D-LFA-1) | A Rubicon reference flow and its optimized variant are GKAT-equivalent. Separately, no `RequestCommit` trace exists without a valid revision and MUL authorization. Guards are projected WHERE-style `{T}`, never CHECK-style `{T,U}`. | Any disable stays green: reversed polarity, commit moved ahead of its guard, or unguarded choice. A `GoTo`/`GoBack` flow is translated instead of refused. |
 
 Bridge findings worth a probe:
 - `JoinExec::bag_count` sums `u64` without an overflow check (`mork-pathmap-probe/src/join.rs:653-659`). The contract should be exact below a stated row bound and refused above it.
 
@@ -48,6 +48,56 @@ The z8run adapter is a **host** of flow graphs; Quack remains the evaluator. No
 
 **Stop conditions:** new execution loop or SQL evaluator, checkpointer becoming authoritative storage, conflicting Kanban transition owner, workflow graph identity becoming row identity, missing generation refusal, non-equivalent replay, or requiring pre-existing data materialization in Context. Halt runtime assimilation rather than papering over with adapters.
 
+## Amendment 2026-10-21: guarded-control verification (GKAT)
+
+**Status:** approved by the operator 2026-10-21. Docs and probes only; no implementation is claimed, no owner is assigned. Source: [.arxiv/1907.05920 GKAT excerpt](../../.arxiv/1907.05920_guarded_kleene_algebra_verified_control_flow_excerpt.md) (#1670); [co-research map](../board/entries/2026-10-21-coresearch-plans-mapping-foresight.md).
+
+This amendment replaces the D-LFA-1 and D-LFA-2 contracts above where they differ; D-LFA-0 and D-LFA-3 are unchanged. D-RFT-2 is unchanged. D-RFT-4 keeps versioned thought binding and frontier behaviour; it does not own guarded workflow verification.
+
+### Guard projection (applies to D-LFA-1 and D-LFA-2)
+
+GKAT tests are Boolean. A K3 predicate becomes a GKAT test only through a **declared projection** of its designated truth values:
+
+- WHERE-style: designated `{T}` (UNKNOWN and FALSE do not pass);
+- CHECK-style: designated `{T, U}` (only FALSE fails).
+
+The two are never interchanged. **Commit authorization uses `{T}` and must never inherit CHECK semantics:** an UNKNOWN revision or authorization does not authorize.
+
+### D-LFA-1: one Rubicon reference flow and one optimized variant
+
+- **Flows.** One structured Rubicon reference flow, and one optimized variant of it. Both use only sequence, guarded choice (`if b then e else f`) and guarded iteration (`while b do e`).
+- **Equivalence.** The two are GKAT-equivalent, checked by bisimulation of their guarded automata. Conditions:
+  - both use the same action alphabet;
+  - both use the same declared guards, each with its declared projection.
+- **Safety, checked separately.** No trace of the reference flow contains `RequestCommit` unless both a valid revision and MUL authorization precede it. Equivalence alone does not establish this: it only says the variant behaves like the reference.
+- **`RequestCommit` is an intent, not a Lance write.** It proposes; the existing supervisor and `cycle_driver` seal. No flow step moves a dataset version.
+- **Disable runs.** Each must fail the check named:
+  1. Reverse a guard's polarity: the equivalence check fails.
+  2. Move `RequestCommit` ahead of its guard: the equivalence check and the safety check both fail.
+  3. Introduce an unguarded nondeterministic choice: the flow is refused as outside GKAT; it is never encoded as an `if` under an invented predicate.
+- **Unstructured jumps are refused.** A flow that uses `GoTo` or `GoBack` is refused, never translated into an unsupported GKAT fragment.
+- **`WaitForInput`.** It is modelled as an observation of external state at resume, i.e. a test, not an autonomous state transition.
+- **Runtime gate.** Snapshot and codebook generation validation stays an independent runtime gate: a stale source refuses at resume. GKAT does not model versions and is not that gate.
+
+### D-LFA-2: integration with existing drivers
+
+- **Scope.** Exercise the existing pieces together:
+  - the graph-flow driver;
+  - thought-git verbs;
+  - Kanban/Rubicon transitions (`kanban.rs` `next_phases`);
+  - authorized action proposals.
+- **Oracle.** Compare deterministic replay results and receipts against the independent from-scratch oracle (`thought-git-probe::oracle::next_version`). The D-TGB-4 receipt is a prerequisite; it does not exist in code yet.
+- **Nothing new beside the existing pieces.** There is no second scheduler, evaluator, state store or commit owner.
+
+### D-GKAT-0: independent fixture probe
+
+- **Status.** Independent and unclaimed; a research and fixture probe only.
+- **Checks.** The numbering follows the #1670 excerpt:
+  - **G1:** guarded factoring and equivalence. The paper's example: `if b then {p; q} else {q}` ≡ `(if b then {p} else {skip}); q` for identical pure `q`. Changing one action label or guard polarity must be rejected.
+  - **G2:** genuine nondeterminism is rejected rather than encoded.
+  - **G5:** the Boolean atom set is explicitly bounded and declared. Beyond the bound the probe refuses; it never enumerates silently.
+- **Exclusions.** No production runtime, no dependency and no executor. A DR64 or DR256 mask is a physical lane set, never a set of GKAT tests.
+
 ## Coordination
 
 Main PR: [ClassView/Quack PostgreSQL parity plan](d-qsp-classview-quack-postgresql-parity-v1.md). Priority companion: [relalg × thought-git frontier](d-rft-relalg-thought-git-frontier-v1.md). Existing source: '.claude/plans/thought-git-basics-v1.md' and EXO-98; '.claude/plans/relalg-v1.md' and EXO-86; EXO-50 messages. Any code handoff needs an explicit owner/claim and separate implementation PR. This PR changes plans only.