From 584a49d0bbb0ae7b2bf3e8e17211d6b6958083ac Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Sat, 19 Sep 2026 10:14:26 -0400
Subject: [PATCH 1/5] feat(semantics): give settlement binding kind executed
 production evidence

``settlement_binding_kind`` was one of the twenty cross-runtime vocabularies
with documented values and no production evidence at all: F1/F2 verified
6 of 26 vocabularies, all kernel tier. Its values are decided inside the
TypeScript builder, so enumerating an owner would prove nothing about which
values a legal input can actually produce.

The evidence is now an executed witness. ``scripts/settlement_binding_witness.mts``
imports the shipped ``settlementIdentity`` builder and runs the four inputs
that make up its whole binding domain: a todo binding, a replan binding,
neither, and the pair it must refuse. The same inputs are re-checked through
the Python bridge that reaches the same code, so a broken adapter is a
failure rather than an unobserved difference. The wire payload shape is
recorded rather than assumed: ``binding_kind`` is present on v1 replan
payloads and absent on v0 todo/unbound payloads, and the test pins that
distinction.

The witness refuses to run against a registry that points it at a different
builder or gives it a value set it does not cover, so registry data cannot
silently widen the credited domain. The module and function are fixed in
tracked code; the registry names the site, it does not select a callable.

F1/F2 quantify over the vocabularies the producer check actually walks, and
that predicate is no longer "kernel tier". The domain selector and its
anchor now name the predicate itself -- ``vocabularies[producers].producers``
-- rather than a tier the first cross-runtime production evidence has
already outgrown. Verified 6 -> 7 of 26; ``cross_runtime_unverified``
20 -> 19.

Mutation-checked: swapping the todo/replan branches in the builder fails 4
tests; removing the adapter or widening the value set each fail their
dedicated refusal tests.

Gates: drift smoke ok (109 passed), architecture 632 passed, premerge
0 failures, node witness via --experimental-strip-types against the tracked
builder at scripts/settlement_binding_witness.mts.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 examples/semantic-vocabulary-drift-smoke.py   |  21 ++-
 loopx/semantics/production.py                 |  70 ++++++++++
 loopx/semantics/vocabulary_v0.json            |  12 +-
 scripts/settlement_binding_witness.mts        |  40 ++++++
 ...est_semantic_settlement_binding_witness.py | 129 ++++++++++++++++++
 .../test_semantic_vocabulary_drift.py         |   8 +-
 6 files changed, 267 insertions(+), 13 deletions(-)
 create mode 100644 scripts/settlement_binding_witness.mts
 create mode 100644 tests/architecture/test_semantic_settlement_binding_witness.py

diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index 77700d9d84..112ecedf3b 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -99,11 +99,12 @@
 FORMAL_DOMAIN_KEYS = {"quantifies_over", "verified", "registered", "evidence_bound"}
 FORMAL_DOMAIN_SELECTORS: dict[str, Callable[[dict[str, Any]], tuple[int, int]]] = {
     # ``check_producers`` walks exactly the vocabularies that declare producers.
-    # Today that predicate selects the kernel tier and nothing else, so F1/F2
-    # quantify over 6 of 26 vocabularies, not over V.
-    "vocabularies[tier=kernel].producers": lambda registry: (
-        sum(1 for entry in registry["vocabularies"].values()
-            if entry["tier"] == "kernel" and "producers" in entry),
+    # That predicate used to select the kernel tier and nothing else; it no
+    # longer does, so the selector names the predicate itself. Writing it as a
+    # tier would quietly stop describing the set the check walks the first time
+    # a cross-runtime vocabulary earns production evidence.
+    "vocabularies[producers].producers": lambda registry: (
+        sum(1 for entry in registry["vocabularies"].values() if "producers" in entry),
         len(registry["vocabularies"]),
     ),
     "vocabularies[*]": lambda registry: (
@@ -152,8 +153,8 @@
 # in a data-only edit. Restating an invariant over a different domain is a
 # normative change and edits this literal in the same diff.
 FORMAL_DOMAIN_ANCHOR = {
-    "F1_producer_closedness": ("vocabularies[tier=kernel].producers", "producer_scan_reach"),
-    "F2_canonical_value_liveness": ("vocabularies[tier=kernel].producers", "producer_scan_reach"),
+    "F1_producer_closedness": ("vocabularies[producers].producers", "producer_scan_reach"),
+    "F2_canonical_value_liveness": ("vocabularies[producers].producers", "producer_scan_reach"),
     "F3_consumer_domain_closedness": ("vocabularies[*]", "inventory_only"),
     "F4_scope_separation": ("scope_declarations[*].contexts", "declared_defining_modules"),
     "F5_projection_totality": ("projections[*]", "executable_owner_function"),
@@ -192,9 +193,15 @@
 INPUT_PRODUCER_ANCHOR = {
     "turn_result_kind": "loopx/control_plane/turn_driver/transaction.py::_result_kind",
     "loop_disposition": "loopx/control_plane/turn_driver/loop_controller.py::decide_loop_disposition",
+    # The settlement binding kind is decided inside the TypeScript builder, so
+    # the witness executes it rather than reading a literal out of the owner.
+    "settlement_binding_kind": "loopx/control_plane/effect_program.ts::settlementIdentity",
 }
 PRODUCER_VOCABULARY_ANCHOR = {
     "effective_action", "turn_route", "loop_disposition", "agent_scope_frontier_action", "turn_result_kind", "lease_action",
+    # First cross-runtime vocabulary carrying executed production evidence. One
+    # named boundary, not a claim about the rest of the cross-runtime set.
+    "settlement_binding_kind",
 }
 RETURN_PRODUCER_ANCHOR = {
     "turn_route": {"loopx/control_plane/turn_driver/driver.py::_typed_route", "loopx/control_plane/turn_driver/loop_controller.py::_envelope_route", "loopx/control_plane/turn_driver/driver.py::build_loopx_turn_plan"},
diff --git a/loopx/semantics/production.py b/loopx/semantics/production.py
index ea0686202c..0116c1ff42 100644
--- a/loopx/semantics/production.py
+++ b/loopx/semantics/production.py
@@ -234,6 +234,71 @@ def probe_turn_result_input_domain(vocabulary: dict[str, Any]) -> list[Productio
     return rows
 
 
+def probe_settlement_binding_production(vocabulary: dict[str, Any]) -> list[Production]:
+    """Witness the real settlement identity builder's binding-kind domain.
+
+    This executes the shipped TypeScript builder and reports what it returns,
+    then re-checks the same inputs through the Python bridge that reaches it.
+    Enumerating the owner would prove nothing about which values a legal input
+    can actually produce; a successful call does.
+
+    The module and the function are fixed here rather than named by registry
+    data, so the registry cannot select an arbitrary callable. The four cases
+    are the builder's whole binding domain: a todo binding, a replan binding,
+    neither, and the pair it must refuse.
+    """
+    from pathlib import Path as _Path
+
+    from ..control_plane.effect_program import SettlementBindingKind, SettlementIdentity
+
+    site = 'loopx/control_plane/effect_program.ts::settlementIdentity'
+    if vocabulary.get('input_producer') != site:
+        raise ValueError('settlement_binding_kind: input_producer must name the anchored builder')
+
+    expected = {
+        'todo': {'todo_id': 't1'},
+        'autonomous_replan': {'replan_obligation_id': 'r1'},
+        'unbound': {},
+    }
+    if set(expected) != set(vocabulary['values']):
+        raise ValueError('settlement_binding_kind: witness does not cover the registered values')
+
+    root = _Path(__file__).resolve().parents[2]
+    probes = [expected[value] for value in vocabulary['values']]
+    probes.append({'todo_id': 't1', 'replan_obligation_id': 'r1'})
+    completed = subprocess.run(
+        ['node', '--no-warnings', '--experimental-strip-types',
+         str(root / 'scripts/settlement_binding_witness.mts')],
+        input=json.dumps({'probes': probes}), capture_output=True, text=True, check=False,
+    )
+    if completed.returncode != 0:
+        raise ValueError(f'settlement_binding_kind: witness probe failed: {completed.stderr.strip()[:300]}')
+    observed = json.loads(completed.stdout)
+
+    rows: list[Production] = []
+    for value, result in zip(vocabulary['values'], observed, strict=False):
+        if not result.get('ok') or result.get('binding_kind') != value:
+            raise ValueError(
+                f'settlement_binding_kind: builder does not produce registered value {value}')
+        # The same input through the Python bridge has to agree, so a broken
+        # adapter is a failure rather than an unobserved difference.
+        bridged = SettlementIdentity(
+            goal_id='g', agent_id='a', turn_instance_id='t',
+            todo_id=expected[value].get('todo_id'),
+            replan_obligation_id=expected[value].get('replan_obligation_id'),
+        )
+        if bridged.binding_kind is not SettlementBindingKind(value):
+            raise ValueError(
+                f'settlement_binding_kind: the Python bridge disagrees for {value}')
+        rows.append(Production(site, SETTLEMENT_IDENTITY_LINE, 'input_witness',
+                               frozenset({value}), False))
+
+    refused = observed[-1]
+    if refused.get('ok'):
+        raise ValueError('settlement_binding_kind: builder accepted both bindings at once')
+    return rows
+
+
 def _probe_controller_domain(vocabulary: dict[str, Any]) -> list[Production]:
     from .turn_contract_witness import probe_controller_production, probe_projection_production
     return probe_controller_production() + probe_projection_production()
@@ -241,7 +306,12 @@ def _probe_controller_domain(vocabulary: dict[str, Any]) -> list[Production]:
 
 # Executable input witnesses are fixed in code and selected only by the
 # registered ``input_producer`` site; registry data cannot import a callable.
+# Line of ``settlementIdentity`` in the tracked builder, so the witness row
+# points at the function it executed.
+SETTLEMENT_IDENTITY_LINE = 408
+
 INPUT_WITNESSES: dict[str, Callable[[dict[str, Any]], list[Production]]] = {
     'loopx/control_plane/turn_driver/transaction.py::_result_kind': probe_turn_result_input_domain,
     'loopx/control_plane/turn_driver/loop_controller.py::decide_loop_disposition': _probe_controller_domain,
+    'loopx/control_plane/effect_program.ts::settlementIdentity': probe_settlement_binding_production,
 }
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index 9ce1406301..2270dbea29 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -77,8 +77,8 @@
         "enforcement": "m0_5",
         "evidence": "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES reach in loopx/semantics/production.py; check_producers visits only vocabularies that declare producers, and validate_production claims no whole-program closedness; unresolved dynamic sites are reported, not treated as proven safe",
         "domain": {
-          "quantifies_over": "vocabularies[tier=kernel].producers",
-          "verified": 6,
+          "quantifies_over": "vocabularies[producers].producers",
+          "verified": 7,
           "registered": 26,
           "evidence_bound": "producer_scan_reach"
         }
@@ -89,8 +89,8 @@
         "enforcement": "m0_5",
         "evidence": "every kernel value has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted",
         "domain": {
-          "quantifies_over": "vocabularies[tier=kernel].producers",
-          "verified": 6,
+          "quantifies_over": "vocabularies[producers].producers",
+          "verified": 7,
           "registered": 26,
           "evidence_bound": "producer_scan_reach"
         }
@@ -558,6 +558,10 @@
         "autonomous_replan",
         "unbound"
       ],
+      "input_producer": "loopx/control_plane/effect_program.ts::settlementIdentity",
+      "producers": [
+        "loopx/control_plane/effect_program.ts::settlementIdentity"
+      ],
       "value_notes": {
         "todo": "Chosen by settlementIdentity when the todo id is non-blank after trimming; supplying both a todo id and a replan obligation id throws before this point. It fixes the effect id to the goal, agent, todo and turn instance form, and is re-derived when a persisted identity payload is decoded.",
         "autonomous_replan": "Chosen when the todo id is blank and the replan obligation id is non-blank after trimming, so the turn settles a replan obligation rather than a selected Todo. The effect id gains an explicit autonomous_replan segment instead of a Todo segment.",
diff --git a/scripts/settlement_binding_witness.mts b/scripts/settlement_binding_witness.mts
new file mode 100644
index 0000000000..e3de4cf188
--- /dev/null
+++ b/scripts/settlement_binding_witness.mts
@@ -0,0 +1,40 @@
+// Execute the real settlement identity builder against given inputs.
+//
+// This is a witness, not a reimplementation: it imports the shipped module and
+// reports what the builder actually returns, including the rejection. The probe
+// inputs arrive on stdin so the registry cannot select an arbitrary callable --
+// the module and the function are fixed here, in tracked code.
+import {settlementIdentity, settlementIdentityPayload} from "../loopx/control_plane/effect_program.ts";
+
+type Probe = {
+  todo_id?: string | null;
+  replan_obligation_id?: string | null;
+};
+
+const request = JSON.parse(await new Response(process.stdin).text()) as {probes: Probe[]};
+const results = request.probes.map(probe => {
+  const input = {
+    goal_id: "g",
+    agent_id: "a",
+    turn_instance_id: "t",
+    todo_id: probe.todo_id ?? null,
+    replan_obligation_id: probe.replan_obligation_id ?? null,
+  };
+  try {
+    const identity = settlementIdentity(input);
+    const payload = settlementIdentityPayload(input);
+    return {
+      ok: true,
+      binding_kind: identity.binding_kind,
+      binding_id: identity.binding_id,
+      effect_id: identity.effect_id,
+      // The wire payload does not always carry binding_kind; reporting the key
+      // presence keeps a later change to that shape visible.
+      payload_has_binding_kind: Object.hasOwn(payload, "binding_kind"),
+      payload_schema_version: payload.schema_version,
+    };
+  } catch (error) {
+    return {ok: false, error: error instanceof Error ? error.message : String(error)};
+  }
+});
+process.stdout.write(JSON.stringify(results));
diff --git a/tests/architecture/test_semantic_settlement_binding_witness.py b/tests/architecture/test_semantic_settlement_binding_witness.py
new file mode 100644
index 0000000000..3ee4af7fbf
--- /dev/null
+++ b/tests/architecture/test_semantic_settlement_binding_witness.py
@@ -0,0 +1,129 @@
+"""The settlement binding kind is proved by executing its builder.
+
+Enumerating an owner proves that a value is spelled somewhere. It does not
+prove a legal input can make the runtime emit it. This vocabulary's evidence
+is the shipped TypeScript builder run against the four inputs that make up
+its whole binding domain, re-checked through the Python bridge that reaches
+the same code.
+
+These tests fail when the witness stops executing the real builder, when the
+builder's branches change meaning, or when it can emit a value outside the
+registered domain -- and the report must not keep crediting a check that no
+longer runs.
+"""
+
+from __future__ import annotations
+
+import json
+import subprocess
+from pathlib import Path
+
+import pytest
+
+from loopx.control_plane.effect_program import SettlementBindingKind, SettlementIdentity
+from loopx.semantics.production import INPUT_WITNESSES, probe_settlement_binding_production
+
+ROOT = Path(__file__).resolve().parents[2]
+REGISTRY = ROOT / "loopx" / "semantics" / "vocabulary_v0.json"
+SITE = "loopx/control_plane/effect_program.ts::settlementIdentity"
+PROBE = ROOT / "scripts" / "settlement_binding_witness.mts"
+
+# The builder's whole binding domain, given as input rather than derived from
+# the owner, so a swapped branch shows up as a disagreement.
+CASES = (
+    ({"todo_id": "t1"}, "todo"),
+    ({"replan_obligation_id": "r1"}, "autonomous_replan"),
+    ({}, "unbound"),
+)
+
+
+def _vocabulary() -> dict:
+    registry = json.loads(REGISTRY.read_text(encoding="utf-8"))
+    return registry["vocabularies"]["settlement_binding_kind"]
+
+
+def _run_probe(probes: list[dict]) -> list[dict]:
+    completed = subprocess.run(
+        ["node", "--no-warnings", "--experimental-strip-types", str(PROBE)],
+        input=json.dumps({"probes": probes}),
+        capture_output=True,
+        text=True,
+        check=True,
+        cwd=ROOT,
+    )
+    return json.loads(completed.stdout)
+
+
+def test_the_registry_anchors_the_builder_as_the_input_producer() -> None:
+    assert _vocabulary()["input_producer"] == SITE
+    assert SITE in INPUT_WITNESSES, "the anchored site must have an executable witness"
+
+
+@pytest.mark.parametrize(("probe", "expected"), CASES)
+def test_the_real_builder_emits_the_registered_value(probe: dict, expected: str) -> None:
+    (result,) = _run_probe([probe])
+    assert result["ok"], result
+    assert result["binding_kind"] == expected
+    assert expected in _vocabulary()["values"]
+
+
+@pytest.mark.parametrize(("probe", "expected"), CASES)
+def test_the_python_bridge_reaches_the_same_builder(probe: dict, expected: str) -> None:
+    identity = SettlementIdentity(
+        goal_id="g",
+        agent_id="a",
+        turn_instance_id="t",
+        todo_id=probe.get("todo_id"),
+        replan_obligation_id=probe.get("replan_obligation_id"),
+    )
+    assert identity.binding_kind is SettlementBindingKind(expected)
+
+
+def test_binding_both_at_once_is_refused_by_the_builder() -> None:
+    (result,) = _run_probe([{"todo_id": "t1", "replan_obligation_id": "r1"}])
+    assert not result["ok"]
+    assert "cannot bind both" in result["error"]
+
+
+def test_binding_both_at_once_is_refused_through_the_bridge() -> None:
+    with pytest.raises(ValueError):
+        SettlementIdentity(
+            goal_id="g", agent_id="a", turn_instance_id="t",
+            todo_id="t1", replan_obligation_id="r1",
+        )
+
+
+def test_the_builder_emits_nothing_outside_the_registered_domain() -> None:
+    registered = set(_vocabulary()["values"])
+    observed = {
+        result["binding_kind"]
+        for result in _run_probe([probe for probe, _ in CASES])
+        if result["ok"]
+    }
+    assert observed <= registered
+    assert observed == registered, "the witness must cover every registered value"
+
+
+def test_the_witness_refuses_a_vocabulary_it_is_not_anchored_to() -> None:
+    """Registry data cannot point the witness at a different builder."""
+    with pytest.raises(ValueError, match="must name the anchored builder"):
+        probe_settlement_binding_production({"input_producer": "elsewhere::f", "values": []})
+
+
+def test_the_witness_refuses_a_value_set_it_does_not_cover() -> None:
+    """Adding a value without extending the witness must fail, not pass silently."""
+    vocabulary = dict(_vocabulary())
+    vocabulary["values"] = [*vocabulary["values"], "a_new_binding_kind"]
+    with pytest.raises(ValueError, match="does not cover the registered values"):
+        probe_settlement_binding_production(vocabulary)
+
+
+def test_the_wire_payload_shape_is_recorded_rather_than_assumed() -> None:
+    """``binding_kind`` is not on every payload; changing that must be visible."""
+    todo, replan, unbound = _run_probe([probe for probe, _ in CASES])
+    assert todo["payload_schema_version"] == "quota_settlement_identity_v0"
+    assert todo["payload_has_binding_kind"] is False
+    assert unbound["payload_schema_version"] == "quota_settlement_identity_v0"
+    assert unbound["payload_has_binding_kind"] is False
+    assert replan["payload_schema_version"] == "quota_settlement_identity_v1"
+    assert replan["payload_has_binding_kind"] is True
diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py
index 212b1db2a5..1e68c4d69a 100644
--- a/tests/architecture/test_semantic_vocabulary_drift.py
+++ b/tests/architecture/test_semantic_vocabulary_drift.py
@@ -505,12 +505,16 @@ def test_f1_f2_domain_names_exactly_the_vocabularies_the_producer_check_walks()
     registry = smoke["load_registry"]()
     vocabularies = registry["vocabularies"]
     walked = {name for name, entry in vocabularies.items() if "producers" in entry}
-    assert walked == {name for name, entry in vocabularies.items() if entry["tier"] == "kernel"}
+    # The domain was the kernel tier while that happened to be the set the
+    # check walked. It is no longer: a cross-runtime vocabulary carrying
+    # executed production evidence is walked too, so the selector names the
+    # predicate rather than a tier it no longer matches.
+    assert walked >= {name for name, entry in vocabularies.items() if entry["tier"] == "kernel"}
     skipped = {entry["tier"] for name, entry in vocabularies.items() if name not in walked}
     assert skipped == {"cross_runtime"}
     for invariant_id in ("F1_producer_closedness", "F2_canonical_value_liveness"):
         domain = _invariant(registry, invariant_id)["domain"]
-        assert domain["quantifies_over"] == "vocabularies[tier=kernel].producers"
+        assert domain["quantifies_over"] == "vocabularies[producers].producers"
         assert domain["verified"] == len(walked)
         assert domain["registered"] == len(vocabularies)
         assert domain["evidence_bound"] == "producer_scan_reach"

From 9560dcb4b12ba40ce2b966758f4e5ed4f1eb08e7 Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Sat, 19 Sep 2026 19:19:55 -0400
Subject: [PATCH 2/5] fix(semantics): pin UTF-8 when the witness reads the
 builder probe

The witness subprocess read the builder's stdout in text mode without an
explicit codec, so `tests/test_runtime_subprocess_utf8.py` refused it. That
guard exists for a concrete reason: on a zh-CN Windows host the child's
UTF-8 JSON would decode as gbk, the reader thread would die on the first
non-ASCII byte, and `stdout` would come back None with returncode 0 -- the
witness would then report a parse error instead of a decode error.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 loopx/semantics/production.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/loopx/semantics/production.py b/loopx/semantics/production.py
index 0116c1ff42..be065237c9 100644
--- a/loopx/semantics/production.py
+++ b/loopx/semantics/production.py
@@ -269,7 +269,8 @@ def probe_settlement_binding_production(vocabulary: dict[str, Any]) -> list[Prod
     completed = subprocess.run(
         ['node', '--no-warnings', '--experimental-strip-types',
          str(root / 'scripts/settlement_binding_witness.mts')],
-        input=json.dumps({'probes': probes}), capture_output=True, text=True, check=False,
+        input=json.dumps({'probes': probes}), capture_output=True, text=True,
+        encoding='utf-8', check=False,
     )
     if completed.returncode != 0:
         raise ValueError(f'settlement_binding_kind: witness probe failed: {completed.stderr.strip()[:300]}')

From b4d91adacba0ded827bd5c9eed4c5ce9be7f1c83 Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Sat, 19 Sep 2026 20:54:43 -0400
Subject: [PATCH 3/5] fix(semantics): state the producer domain over the set
 the checks walk

Giving ``settlement_binding_kind`` an executed witness made it the first
cross_runtime vocabulary to declare producers, so ``check_producers`` walks
it and F1/F2 report 7/26. The canonical statements were not restated with
it: the registry still called ``Kernel(V)`` the only tier declaring
producers, F1 still quantified over ``Kernel(V)``, and F2 still said in
words that the cross_runtime tier declares none. A machine reader and a
human reader got different answers about what F1 and F2 prove, and every
check passed under both.

The gap was structural. ``check_invariant_domain`` pins ``quantifies_over``,
``verified`` and ``registered`` against counts derived from the registry, so
the machine domain could not rot; ``statement`` and ``evidence`` were free
text nothing read. Widening the walked set was a one-diff failure on the
numbers and a silent one on the claim.

The domain is now named for the predicate rather than a tier. ``Producers(V)``
is the subset that declares producers -- every tier=kernel vocabulary plus any
vocabulary of another tier carrying executed production evidence -- which is
exactly what ``check_producers`` visits. F1 and F2 also name what stays
outside, the 19 cross_runtime vocabularies still declaring no producer,
because stating only the verified half lets the unverified remainder shrink
out of the text without a diff saying so.

``check_domain_prose`` makes the agreement checkable: no producer-domain
statement or evidence may bound the claim by ``Kernel(V)`` once a non-kernel
vocabulary is walked, none may say a tier declares no producers while one of
its members does, and each statement must name the count left outside.
Verified by mutation: restoring the Kernel-only universe, re-adding the
cross-runtime denial to F2, and replacing F1's ``19 cross_runtime`` with a
vague phrase each turn the smoke red; two regressions in
``tests/architecture/test_semantic_vocabulary_drift.py`` pin all three.

The RFC carried the same contradiction in both language editions, so its
formal-model section is restated over ``Producers(V)`` as well. The
2026-09-17 appendix entry that first bounded the invariants to ``Kernel(V)``
stays as written: it is append-only history and was accurate when recorded.

No check changes its verdict on the current tree. ``tests/architecture`` 685
passed; the drift smoke reports F1/F2 7/26 with cross_runtime_unverified
19/20, and the docs governance smoke accepts the new ledger entry and its
Chinese mirror. Ruff on the changed files reports one finding fewer than the
same files on main.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 ...cer-domain-prose-follows-the-walked-set.md | 42 +++++++++++++
 ...main-prose-follows-the-walked-set.zh-CN.md | 31 ++++++++++
 .../semantic-vocabulary-convergence-v0.md     | 31 ++++++----
 ...emantic-vocabulary-convergence-v0.zh-CN.md | 25 ++++----
 examples/semantic-vocabulary-drift-smoke.py   | 60 ++++++++++++++++++-
 loopx/semantics/vocabulary_v0.json            | 10 ++--
 .../test_semantic_vocabulary_drift.py         | 49 +++++++++++++++
 7 files changed, 216 insertions(+), 32 deletions(-)
 create mode 100644 docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.md
 create mode 100644 docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.zh-CN.md

diff --git a/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.md b/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.md
new file mode 100644
index 0000000000..8ee7ab04bf
--- /dev/null
+++ b/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.md
@@ -0,0 +1,42 @@
+# The producer domain's prose follows the walked set
+
+Normative for what F1 and F2 claim; no check changes its verdict on the current
+tree. What changes is that the sentence a reader audits and the set the checker
+walks can no longer disagree.
+
+- **Two answers were both green.** Giving `settlement_binding_kind` an executed
+  witness made it the first `cross_runtime` vocabulary to declare producers, so
+  `check_producers` walks it and F1/F2 report `7/26`. The same registry still
+  said `Kernel(V)` was the only tier declaring producers, and F2 still said in
+  words that the `cross_runtime` tier declares none. A machine reader and a
+  human reader got different answers about what F1 and F2 prove, and 122
+  focused tests plus 25 CI checks passed either way.
+- **The gap was structural, not an oversight.** `check_invariant_domain` pins
+  `quantifies_over`, `verified` and `registered` against counts derived from the
+  registry, so the machine domain could not rot. `statement` and `evidence` were
+  free text that nothing read. Widening the walked set was therefore a one-diff
+  failure on the numbers and a silent one on the claim.
+- **The domain is named for the predicate, not a tier.** `Producers(V)` is the
+  subset that declares producers: every `tier: kernel` vocabulary plus any
+  vocabulary of another tier carrying executed production evidence. That is the
+  set `check_producers` visits, so the name no longer has to be restated when a
+  vocabulary outside the kernel tier earns its way in.
+- **The claim states its own boundary.** F1 and F2 name what stays outside —
+  the 19 `cross_runtime` vocabularies still declaring no producer — rather than
+  only the seven verified. Stating the verified half alone lets the unverified
+  remainder shrink out of the text without any diff saying so.
+- **The agreement is checked.** `check_domain_prose` in
+  `examples/semantic-vocabulary-drift-smoke.py` derives the walked set and
+  refuses prose that contradicts it: no producer-domain statement or evidence
+  line may bound the claim by `Kernel(V)` once a non-kernel vocabulary is
+  walked, none may say a tier declares no producers while one of its members
+  does, and each statement must name the count left outside. Verified by
+  mutation: restoring the `Kernel(V)` universe, re-adding the cross-runtime
+  denial to F2, and replacing F1's `19 cross_runtime` with a vague phrase each
+  turn the smoke red, and two regressions in
+  `tests/architecture/test_semantic_vocabulary_drift.py` pin all three.
+- **The RFC's own statement was carrying the same contradiction.** The formal
+  model section in both language editions stated F1 and F2 over `Kernel(V)` and
+  repeated the cross-runtime denial. Both are restated over `Producers(V)`. The
+  2026-09-17 appendix entry that first bounded the invariants to `Kernel(V)`
+  stays as written: it is append-only history and was accurate when recorded.
diff --git a/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.zh-CN.md b/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.zh-CN.md
new file mode 100644
index 0000000000..ae838bf1ff
--- /dev/null
+++ b/docs/architecture/rfcs/ledger/semantic-vocabulary-convergence-v0/2026-09-19-producer-domain-prose-follows-the-walked-set.zh-CN.md
@@ -0,0 +1,31 @@
+# 生产者值域的文字跟随实际走过的集合
+
+对 F1/F2 所声称的内容属规范性变更；当前源码树上没有任何检查的判定改变。改变的是：
+人所审计的那句话，与检查器实际走过的集合，不能再各说各话。
+
+- **两个答案同时为绿。** 给 `settlement_binding_kind` 配上可执行 witness 后，它成为
+  第一个声明 producers 的 `cross_runtime` 词表，`check_producers` 会走它，F1/F2 报
+  `7/26`。而同一份注册表仍写着 `Kernel(V)` 是唯一声明 producers 的层，F2 的正文也
+  仍说 `cross_runtime` 层不声明 producers。机器读者与人类读者对"F1/F2 证明了什么"
+  得到两个不同答案，而 122 个焦点测试与 25 个 CI 检查在两种说法下都通过。
+- **这是结构性缺口，不是疏忽。** `check_invariant_domain` 会把 `quantifies_over`、
+  `verified`、`registered` 钉在由注册表推导出的计数上，机器域因此不会腐化；
+  `statement` 与 `evidence` 却是没有任何检查读取的自由文本。于是扩大走过的集合，
+  在数字上是一次性失败，在声明上却是静默的。
+- **值域按谓词命名，不按层命名。** `Producers(V)` 是声明了 producers 的子集：所有
+  `tier: kernel` 词表，加上其他层中携带可执行生产证据的词表。这正是
+  `check_producers` 访问的集合，因此当非 kernel 层的词表凭证据进入时，名字不必
+  重写。
+- **声明自带边界。** F1/F2 明确写出留在域外的部分——仍未声明任何 producer 的 19 个
+  `cross_runtime` 词表——而不是只写已验证的 7 个。只陈述已验证的一半，会让未验证的
+  余量在没有任何 diff 说明的情况下悄悄缩水。
+- **这种一致性是被检查的。** `examples/semantic-vocabulary-drift-smoke.py` 中的
+  `check_domain_prose` 推导出走过的集合，并拒绝与之矛盾的文字：一旦有非 kernel 词表
+  被走过，生产者值域的 statement/evidence 就不得再以 `Kernel(V)` 为界；也不得在某层
+  已有成员声明 producers 时宣称该层不声明 producers；每条 statement 还必须写出留在
+  域外的数量。已用突变验证：恢复 `Kernel(V)` 的 universe、把跨运行时否认句加回 F2、
+  把 F1 的 `19 cross_runtime` 换成含糊措辞，三者都会让冒烟变红，
+  `tests/architecture/test_semantic_vocabulary_drift.py` 中的两条回归把它们钉住。
+- **RFC 正文自身也带着同一条矛盾。** 两个语言版本的形式模型章节都把 F1/F2 写在
+  `Kernel(V)` 上，并重复了跨运行时否认句，现已改写到 `Producers(V)`。2026-09-17 那条
+  最早把不变量收敛到 `Kernel(V)` 的附录条目保持原样：它是只追加的历史，记录当时准确。
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 54aaee1764..5fbe427152 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -560,19 +560,24 @@ R ⊆ L × V × Version               persists a value durably
 ```
 
 Each obligation is stated over the domain it is actually checked on, not over
-`V`. `Kernel(V) ⊆ V` is the `tier: kernel` subset, the only tier that declares
-producers; `Produced_scan(v)` is the production the fixed forms observe inside
-the code-owned scan reach; `ScopeDeclarations` are the forked names the registry
-declares as bounded contexts.
-
-1. **Producer closedness (kernel tier):** `∀v ∈ Kernel(V): Produced_scan(v) ⊆
-   S(v) ⊆ U(v)`. A recognised producer cannot write a value outside the
-   registered set. Production outside the scan reach, and the whole
-   `cross_runtime` tier, is unverified rather than proven closed.
-2. **Canonical liveness (kernel tier):** `∀v ∈ Kernel(V): Canonical(v) ⊆
-   Produced_scan(v) ∪ CompatibilityOnly(v)`. A value that is only compared is
-   dead or compatibility-only, never canonical. The `cross_runtime` tier
-   declares no producers, so liveness there is unverified.
+`V`. `Producers(V) ⊆ V` is the subset that declares producers — every
+`tier: kernel` vocabulary, plus any vocabulary of another tier that carries
+executed production evidence; `Produced_scan(v)` is the production the fixed
+forms observe inside the code-owned scan reach; `ScopeDeclarations` are the
+forked names the registry declares as bounded contexts.
+
+1. **Producer closedness (vocabularies declaring producers):** `∀v ∈
+   Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v)`. A recognised producer cannot
+   write a value outside the registered set. `Producers(V)` is currently the six
+   `tier: kernel` vocabularies plus `settlement_binding_kind`, the one
+   `cross_runtime` vocabulary carrying an executed witness. Production outside
+   the scan reach, and the 19 `cross_runtime` vocabularies still outside
+   `Producers(V)`, are unverified rather than proven closed.
+2. **Canonical liveness (vocabularies declaring producers):** `∀v ∈
+   Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v)`. A
+   value that is only compared is dead or compatibility-only, never canonical.
+   The 19 `cross_runtime` vocabularies outside `Producers(V)` are never walked,
+   so liveness there is unverified.
 3. **Consumer domain closedness:** `Accepted(c) ⊆ S(v)`, unless the consumer
    explicitly declares an external or partial domain.
 4. **Scope enumeration completeness:** `∀n ∈ ScopeDeclarations`, the declared
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
index 4cdf94f39f..25307306ad 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -447,17 +447,20 @@ G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) 做投影
 R ⊆ L × V × Version               将值持久化
 ```
 
-每条义务都按它实际被检查的值域陈述，而不是泛指 `V`。`Kernel(V) ⊆ V` 是
-`tier: kernel` 子集，也是唯一声明了 producers 的层；`Produced_scan(v)` 是固定形式
-在代码所有的扫描范围内观察到的生产；`ScopeDeclarations` 是注册表声明为有界上下文
-的那些分叉名字。
-
-1. **生产闭包（仅 kernel 层）：** `∀v ∈ Kernel(V): Produced_scan(v) ⊆ S(v) ⊆ U(v)`。
-   被识别的生产者不能写入注册集合之外的值。扫描范围之外的生产，以及整个
-   `cross_runtime` 层，是未验证，而不是已证明闭合。
-2. **规范值存活（仅 kernel 层）：** `∀v ∈ Kernel(V): Canonical(v) ⊆ Produced_scan(v) ∪
-   CompatibilityOnly(v)`。只被比较、没有生产来源的值是死值或兼容值，不能是
-   canonical。`cross_runtime` 层不声明 producers，因此该层的存活性未被验证。
+每条义务都按它实际被检查的值域陈述，而不是泛指 `V`。`Producers(V) ⊆ V` 是
+声明了 producers 的子集：所有 `tier: kernel` 词表，再加上其他层中携带了可执行
+生产证据的词表；`Produced_scan(v)` 是固定形式在代码所有的扫描范围内观察到的
+生产；`ScopeDeclarations` 是注册表声明为有界上下文的那些分叉名字。
+
+1. **生产闭包（声明了 producers 的词表）：** `∀v ∈ Producers(V): Produced_scan(v) ⊆
+   S(v) ⊆ U(v)`。被识别的生产者不能写入注册集合之外的值。`Producers(V)` 目前是
+   6 个 `tier: kernel` 词表，加上 `settlement_binding_kind`——唯一携带可执行 witness 的
+   `cross_runtime` 词表。扫描范围之外的生产，以及仍在 `Producers(V)` 之外的 19 个
+   `cross_runtime` 词表，是未验证，而不是已证明闭合。
+2. **规范值存活（声明了 producers 的词表）：** `∀v ∈ Producers(V): Canonical(v) ⊆
+   Produced_scan(v) ∪ CompatibilityOnly(v)`。只被比较、没有生产来源的值是死值或
+   兼容值，不能是 canonical。仍在 `Producers(V)` 之外的 19 个 `cross_runtime` 词表从未
+   被走过，因此该层的存活性未被验证。
 3. **消费者定义域闭包：** `Accepted(c) ⊆ S(v)`，除非消费者显式声明外部定义域或部分定义域。
 4. **作用域枚举完备性：** `∀n ∈ ScopeDeclarations`，声明的上下文 owner 模块集合
    恰好等于定义 `n` 的模块集合，每个模块一个上下文，且每个上下文的 owner 符号
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index 112ecedf3b..224e700cd0 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -152,6 +152,11 @@
 # an invariant cannot quietly widen its own claim by choosing a looser selector
 # in a data-only edit. Restating an invariant over a different domain is a
 # normative change and edits this literal in the same diff.
+# The invariants whose prose describes which vocabularies declare producers.
+# check_domain_prose reads their statement and evidence, so an invariant added
+# to this set has its free text held to the walked set as well.
+PRODUCER_DOMAIN_INVARIANTS = ("F1_producer_closedness", "F2_canonical_value_liveness")
+
 FORMAL_DOMAIN_ANCHOR = {
     "F1_producer_closedness": ("vocabularies[producers].producers", "producer_scan_reach"),
     "F2_canonical_value_liveness": ("vocabularies[producers].producers", "producer_scan_reach"),
@@ -398,6 +403,7 @@ def check_formal_model(model: dict[str, Any], registry: dict[str, Any]) -> None:
         require(item["statement"].strip() and item["evidence"].strip(),
                 f"formal invariant {item['id']} needs a statement and evidence boundary")
         check_invariant_domain(item, registry)
+    check_domain_prose(model, registry)
     policy = model["enforcement_policy"]
     require(set(policy) == FORMAL_POLICY_KEYS,
             "formal_model enforcement_policy must separate current, next, advisory, and unproved checks")
@@ -430,6 +436,53 @@ def check_formal_model(model: dict[str, Any], registry: dict[str, Any]) -> None:
                 f"formal_model proof_boundary.{key} must contain non-empty claim names")
 
 
+def check_domain_prose(model: dict[str, Any], registry: dict[str, Any]) -> None:
+    """Forbid prose that denies a producer the producer check actually walks.
+
+    ``check_invariant_domain`` pins the machine domain, but ``statement`` and
+    ``evidence`` are free text and nothing tied them to the same set. That
+    split was reachable: the registry counted a cross-runtime producer into
+    F1/F2 and reported 7/26 while this same file still said the kernel tier was
+    the only one declaring producers, and every check stayed green because no
+    check read both. The walked set is derived here, so a claim that contradicts
+    it fails in the diff that widens the set rather than outliving it.
+    """
+    vocabularies = registry["vocabularies"]
+    walked = {name for name, entry in vocabularies.items() if "producers" in entry}
+    kernel = {name for name, entry in vocabularies.items() if entry["tier"] == "kernel"}
+    outside = {name for name in vocabularies if name not in walked}
+    prose = {"universes.vocabularies": model["universes"]["vocabularies"]}
+    for item in model["invariants"]:
+        if item["id"] in PRODUCER_DOMAIN_INVARIANTS:
+            prose[f"{item['id']}.statement"] = item["statement"]
+            prose[f"{item['id']}.evidence"] = item["evidence"]
+    require(len(prose) == 1 + 2 * len(PRODUCER_DOMAIN_INVARIANTS),
+            "formal_model must state each producer-domain invariant exactly once for prose review")
+    beyond_kernel = sorted(walked - kernel)
+    for tier in sorted({vocabularies[name]["tier"] for name in beyond_kernel}):
+        denial = f"the {tier} tier declares no producers"
+        for where, text in prose.items():
+            require(denial not in text.lower(),
+                    f"formal_model {where} says {denial!r} while {beyond_kernel} declare "
+                    "producers and are walked by the producer check")
+    if beyond_kernel:
+        for where, text in prose.items():
+            require("Kernel(V)" not in text,
+                    f"formal_model {where} bounds the claim by Kernel(V) while the producer "
+                    f"check walks {len(walked)} vocabularies, including {beyond_kernel} "
+                    "outside the kernel tier")
+    # The size left outside is the honest half of the boundary: stating only
+    # what is verified lets the unverified remainder shrink out of the text.
+    for tier in sorted({vocabularies[name]["tier"] for name in outside}):
+        remaining = sum(1 for name in outside if vocabularies[name]["tier"] == tier)
+        fragment = f"{remaining} {tier}"
+        for invariant_id in PRODUCER_DOMAIN_INVARIANTS:
+            where = f"{invariant_id}.statement"
+            require(fragment in prose[where],
+                    f"formal_model {where} must name the {remaining} {tier} vocabularies left "
+                    f"outside the walked set; it does not say {fragment!r}")
+
+
 def check_invariant_domain(invariant: dict[str, Any], registry: dict[str, Any]) -> None:
     """Require a declared invariant domain to match the set actually walked.
 
@@ -703,9 +756,10 @@ def check_producers(registry: dict[str, Any], sources: list[SourceFile]) -> list
     unknown: list[str] = []
     for name, vocabulary in registry['vocabularies'].items():
         if 'producers' not in vocabulary:
-            # Skipped: the whole cross_runtime tier, which declares no producers.
-            # F1/F2 therefore hold over the kernel tier only, which is the domain
-            # the registry's formal_model states -- not an unconditional claim.
+            # Skipped: a vocabulary that declares no producers. That is every
+            # cross_runtime vocabulary except the ones carrying an executed
+            # witness. F1/F2 therefore hold over the walked set the registry's
+            # formal_model names Producers(V) -- not an unconditional claim.
             continue
         try:
             rows = collect_production(REPO_ROOT, vocabulary, sources)
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index a53d2ff069..af8336a08f 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -13,7 +13,7 @@
   "formal_model": {
     "schema_version": "loopx_semantic_formal_model_v0",
     "universes": {
-      "vocabularies": "V: registered vocabulary identifiers; Kernel(V) ⊆ V is the tier=kernel subset, the only tier that declares producers",
+      "vocabularies": "V: registered vocabulary identifiers; Producers(V) ⊆ V is the subset that declares producers: every tier=kernel vocabulary, plus any vocabulary of another tier that carries executed production evidence",
       "values": "U(v): ambient runtime values; S(v): registered admitted values",
       "sites": "L: source locations that define, produce, consume, interpret, pass through, project, or persist values",
       "scopes": "Scope: global or bounded_context(context_id); ScopeDeclarations are the forked names the registry declares as bounded contexts",
@@ -73,7 +73,7 @@
     "invariants": [
       {
         "id": "F1_producer_closedness",
-        "statement": "∀v ∈ Kernel(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Production outside that reach, and the whole cross_runtime tier, is unverified rather than proven closed.",
+        "statement": "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Producers(V) is currently the six tier=kernel vocabularies plus settlement_binding_kind, the one cross_runtime vocabulary carrying an executed witness. Production outside that reach, and the 19 cross_runtime vocabularies still outside Producers(V), are unverified rather than proven closed.",
         "enforcement": "m0_5",
         "evidence": "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES reach in loopx/semantics/production.py; check_producers visits only vocabularies that declare producers, and validate_production claims no whole-program closedness; unresolved dynamic sites are reported, not treated as proven safe",
         "domain": {
@@ -85,9 +85,9 @@
       },
       {
         "id": "F2_canonical_value_liveness",
-        "statement": "∀v ∈ Kernel(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). The cross_runtime tier declares no producers, so liveness there is unverified rather than proven.",
+        "statement": "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). The 19 cross_runtime vocabularies outside Producers(V) are never walked, so liveness there is unverified rather than proven.",
         "enforcement": "m0_5",
-        "evidence": "every kernel value has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted",
+        "evidence": "every value of a vocabulary in Producers(V) has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted",
         "domain": {
           "quantifies_over": "vocabularies[producers].producers",
           "verified": 7,
@@ -597,7 +597,7 @@
         "writeback_rejected": "Raised when the durable_writeback callback ran and returned a payload that is not a committed result, and in the task-lease verbs when a failure arose past the validation stage with a code outside the identity and permission sets. The writeback was attempted and refused, as opposed to writeback_missing where it was never observed.",
         "quota_spend_rejected": "Raised when a settlement callback returned a non-committed payload on a step that is neither durable_writeback nor terminal_closeout, and the rejection reason text does not contain the word budget. It is the same branch as budget_rejected, separated only by that substring test.",
         "terminal_closeout_rejected": "Raised on three branches: the terminal_closeout callback returned a non-committed payload; closeout was required but the turn's result kind is set and is not validated_completion, so there is no completed turn to close out; or a closeout payload was supplied when closeout was not required at all.",
-        "cancelled": "Unresolved: the value is declared in both owner modules and admitted by the decoders, but no branch under loopx/ selects it. A search of the literal, the enum member form and member value reads finds only the two definition sites; every other occurrence of the token in the tree belongs to an unrelated vocabulary such as the chat proposal status, the subagent execution status or a CI conclusion, and the only settlement-shaped uses are tests that fabricate it to check a failure is not erased. Missing evidence: a producing branch, or a compatibility_only declaration saying it is reserved for an external or future canceller. Because the cross_runtime tier declares no producers and is outside the F2 liveness check, a dead value here is not caught by the drift smoke, so whether this is reserved or actually dead is an open question for a maintainer.",
+        "cancelled": "Unresolved: the value is declared in both owner modules and admitted by the decoders, but no branch under loopx/ selects it. A search of the literal, the enum member form and member value reads finds only the two definition sites; every other occurrence of the token in the tree belongs to an unrelated vocabulary such as the chat proposal status, the subagent execution status or a CI conclusion, and the only settlement-shaped uses are tests that fabricate it to check a failure is not erased. Missing evidence: a producing branch, or a compatibility_only declaration saying it is reserved for an external or future canceller. Because this vocabulary declares no producers and is therefore outside the F2 liveness check, a dead value here is not caught by the drift smoke, so whether this is reserved or actually dead is an open question for a maintainer.",
         "permission_denied": "Raised when a task-lease verb was refused by an authority check before any durable write: the failure code is corrupt_lease or one of the registered owner and Todo eligibility codes, or a promoted-authority fence rejected a legacy writer. The invariant is that it was denied at the validation stage and nothing was written. These sites emit the bare string rather than a typed member, so the value is only checked when a decoder parses the envelope.",
         "budget_rejected": "Raised on the same branch as quota_spend_rejected, a non-committed callback payload on a step that is neither durable_writeback nor terminal_closeout, and separated from it only by the derived reason text containing the word budget, case-insensitively. That is a substring test on free-form callback text, not a structured budget signal, so a budget refusal phrased without the word is reported as quota_spend_rejected instead.",
         "effect_outcome_unknown": "Raised when the effect was prepared and dispatched but its outcome cannot be decided either way: the provider's observation for the step is explicitly unknown, or an observation exists that is neither unknown nor a committed payload, meaning the adapter never durably checkpointed it. It is the only failure kind asserting no outcome; every other kind asserts a known one, which is why it must neither be retried nor declared done."
diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py
index 1e68c4d69a..8a056c235f 100644
--- a/tests/architecture/test_semantic_vocabulary_drift.py
+++ b/tests/architecture/test_semantic_vocabulary_drift.py
@@ -520,6 +520,55 @@ def test_f1_f2_domain_names_exactly_the_vocabularies_the_producer_check_walks()
         assert domain["evidence_bound"] == "producer_scan_reach"
 
 
+def test_prose_may_not_deny_a_producer_the_check_walks() -> None:
+    """The statement a human reads is held to the set the checker walks.
+
+    The machine domain and the prose were independent: the registry counted a
+    cross-runtime producer into F1/F2 and reported 7/26 while the same file
+    still called the kernel tier the only one declaring producers. Nothing was
+    red, because no check read both. Each mutation below restores one half of
+    that contradiction.
+    """
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke["load_registry"]())
+    model = registry["formal_model"]
+    smoke["check_formal_model"](model, registry)
+
+    kernel_only = copy.deepcopy(registry)
+    kernel_only["formal_model"]["universes"]["vocabularies"] = (
+        "V: registered vocabulary identifiers; Kernel(V) \u2286 V is the tier=kernel "
+        "subset, the only tier that declares producers"
+    )
+    with pytest.raises(smoke["Drift"], match="Kernel\\(V\\)"):
+        smoke["check_formal_model"](kernel_only["formal_model"], kernel_only)
+
+    denial = copy.deepcopy(registry)
+    _invariant(denial, "F2_canonical_value_liveness")["statement"] += (
+        " The cross_runtime tier declares no producers."
+    )
+    with pytest.raises(smoke["Drift"], match="declares no producers"):
+        smoke["check_formal_model"](denial["formal_model"], denial)
+
+
+def test_prose_must_keep_naming_what_stays_outside_the_walked_set() -> None:
+    """Stating only the verified half lets the unverified remainder go quiet."""
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke["load_registry"]())
+    vocabularies = registry["vocabularies"]
+    outside = [name for name, entry in vocabularies.items() if "producers" not in entry]
+    tiers = {vocabularies[name]["tier"] for name in outside}
+    assert tiers == {"cross_runtime"}, tiers
+
+    statement = _invariant(registry, "F1_producer_closedness")["statement"]
+    fragment = f"{len(outside)} cross_runtime"
+    assert fragment in statement, statement
+    _invariant(registry, "F1_producer_closedness")["statement"] = statement.replace(
+        fragment, "the remaining cross_runtime"
+    )
+    with pytest.raises(smoke["Drift"], match="left outside the walked set"):
+        smoke["check_formal_model"](registry["formal_model"], registry)
+
+
 @pytest.mark.parametrize("invariant_id", sorted({
     "F1_producer_closedness",
     "F2_canonical_value_liveness",

From 3b21a9cebbba851b5bbcd455956685b27e3df80e Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Sat, 19 Sep 2026 23:20:59 -0400
Subject: [PATCH 4/5] fix(semantics): derive canonical producer claims from
 domain facts

Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 examples/semantic-vocabulary-drift-smoke.py   | 123 +++++++++++-------
 loopx/semantics/vocabulary_v0.json            |   6 +-
 .../test_semantic_vocabulary_drift.py         |  70 +++++-----
 3 files changed, 115 insertions(+), 84 deletions(-)

diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index 224e700cd0..03f16cc4ad 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -15,6 +15,7 @@
 import json
 import re
 import sys
+from dataclasses import dataclass
 from pathlib import Path
 from typing import Any, Callable
 
@@ -104,7 +105,7 @@
     # tier would quietly stop describing the set the check walks the first time
     # a cross-runtime vocabulary earns production evidence.
     "vocabularies[producers].producers": lambda registry: (
-        sum(1 for entry in registry["vocabularies"].values() if "producers" in entry),
+        len(ProducerDomain.from_registry(registry).walked),
         len(registry["vocabularies"]),
     ),
     "vocabularies[*]": lambda registry: (
@@ -152,9 +153,8 @@
 # an invariant cannot quietly widen its own claim by choosing a looser selector
 # in a data-only edit. Restating an invariant over a different domain is a
 # normative change and edits this literal in the same diff.
-# The invariants whose prose describes which vocabularies declare producers.
-# check_domain_prose reads their statement and evidence, so an invariant added
-# to this set has its free text held to the walked set as well.
+# F1/F2 statements are canonical projections of the producer domain, not
+# arbitrary prose classified by keyword rules.
 PRODUCER_DOMAIN_INVARIANTS = ("F1_producer_closedness", "F2_canonical_value_liveness")
 
 FORMAL_DOMAIN_ANCHOR = {
@@ -436,51 +436,82 @@ def check_formal_model(model: dict[str, Any], registry: dict[str, Any]) -> None:
                 f"formal_model proof_boundary.{key} must contain non-empty claim names")
 
 
+@dataclass(frozen=True)
+class ProducerDomain:
+    """Finite facts behind the canonical F1/F2 statements."""
+
+    walked: frozenset[str]
+    kernel: frozenset[str]
+    outside_by_tier: tuple[tuple[str, int], ...]
+
+    @classmethod
+    def from_registry(cls, registry: dict[str, Any]) -> ProducerDomain:
+        vocabularies = registry["vocabularies"]
+        walked = frozenset(name for name, entry in vocabularies.items() if "producers" in entry)
+        kernel = frozenset(name for name, entry in vocabularies.items() if entry["tier"] == "kernel")
+        outside = [entry for name, entry in vocabularies.items() if name not in walked]
+        return cls(walked, kernel, tuple(
+            (tier, sum(entry["tier"] == tier for entry in outside))
+            for tier in sorted({entry["tier"] for entry in outside})
+        ))
+
+
+def producer_domain_prose(registry: dict[str, Any]) -> dict[str, str]:
+    """Render normalized claims; no free-text semantic inference is attempted."""
+    domain = ProducerDomain.from_registry(registry)
+    comparison = (
+        "Kernel(V) ⊆ Producers(V)." if domain.kernel <= domain.walked
+        else "Kernel(V) is not a subset of Producers(V)."
+    )
+    outside = ", ".join(f"{count} {tier}" for tier, count in domain.outside_by_tier) or "0"
+    boundary = (
+        f"Producers(V) contains {len(domain.walked)} vocabularies: "
+        f"{len(domain.walked & domain.kernel)} kernel and "
+        f"{len(domain.walked - domain.kernel)} outside the kernel tier. "
+        f"The {outside} vocabularies outside Producers(V) are unverified."
+    )
+    return {
+        "universes.vocabularies": (
+            "V: registered vocabulary identifiers; Producers(V) ⊆ V is exactly "
+            "the subset declaring a producers key (including compatibility-only "
+            f"entries with an empty list). {comparison} {boundary}"
+        ),
+        "F1_producer_closedness.statement": (
+            "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where "
+            "Produced_scan(v) is the production the fixed forms observe inside "
+            f"the code-owned scan reach. {boundary} Production outside the scan "
+            "reach is unverified rather than proven closed."
+        ),
+        "F1_producer_closedness.evidence": (
+            "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES "
+            "reach in loopx/semantics/production.py; check_producers visits only "
+            "vocabularies that declare producers, and validate_production claims no "
+            "whole-program closedness; unresolved dynamic sites are reported, not "
+            "treated as proven safe"
+        ),
+        "F2_canonical_value_liveness.statement": (
+            "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). "
+            f"{boundary} Liveness outside the walked set is not proven."
+        ),
+        "F2_canonical_value_liveness.evidence": (
+            "every value of a vocabulary in Producers(V) has a producer recognised "
+            "inside the scan reach, an executable input witness, or an explicit "
+            "compatibility-only reason; a value whose only producer lies outside "
+            "the reach would be reported as dead, not silently accepted"
+        ),
+    }
+
+
 def check_domain_prose(model: dict[str, Any], registry: dict[str, Any]) -> None:
-    """Forbid prose that denies a producer the producer check actually walks.
-
-    ``check_invariant_domain`` pins the machine domain, but ``statement`` and
-    ``evidence`` are free text and nothing tied them to the same set. That
-    split was reachable: the registry counted a cross-runtime producer into
-    F1/F2 and reported 7/26 while this same file still said the kernel tier was
-    the only one declaring producers, and every check stayed green because no
-    check read both. The walked set is derived here, so a claim that contradicts
-    it fails in the diff that widens the set rather than outliving it.
-    """
-    vocabularies = registry["vocabularies"]
-    walked = {name for name, entry in vocabularies.items() if "producers" in entry}
-    kernel = {name for name, entry in vocabularies.items() if entry["tier"] == "kernel"}
-    outside = {name for name in vocabularies if name not in walked}
-    prose = {"universes.vocabularies": model["universes"]["vocabularies"]}
+    """Require generated canonical statements, not keyword-based prose approval."""
+    actual = {"universes.vocabularies": model["universes"]["vocabularies"]}
     for item in model["invariants"]:
         if item["id"] in PRODUCER_DOMAIN_INVARIANTS:
-            prose[f"{item['id']}.statement"] = item["statement"]
-            prose[f"{item['id']}.evidence"] = item["evidence"]
-    require(len(prose) == 1 + 2 * len(PRODUCER_DOMAIN_INVARIANTS),
-            "formal_model must state each producer-domain invariant exactly once for prose review")
-    beyond_kernel = sorted(walked - kernel)
-    for tier in sorted({vocabularies[name]["tier"] for name in beyond_kernel}):
-        denial = f"the {tier} tier declares no producers"
-        for where, text in prose.items():
-            require(denial not in text.lower(),
-                    f"formal_model {where} says {denial!r} while {beyond_kernel} declare "
-                    "producers and are walked by the producer check")
-    if beyond_kernel:
-        for where, text in prose.items():
-            require("Kernel(V)" not in text,
-                    f"formal_model {where} bounds the claim by Kernel(V) while the producer "
-                    f"check walks {len(walked)} vocabularies, including {beyond_kernel} "
-                    "outside the kernel tier")
-    # The size left outside is the honest half of the boundary: stating only
-    # what is verified lets the unverified remainder shrink out of the text.
-    for tier in sorted({vocabularies[name]["tier"] for name in outside}):
-        remaining = sum(1 for name in outside if vocabularies[name]["tier"] == tier)
-        fragment = f"{remaining} {tier}"
-        for invariant_id in PRODUCER_DOMAIN_INVARIANTS:
-            where = f"{invariant_id}.statement"
-            require(fragment in prose[where],
-                    f"formal_model {where} must name the {remaining} {tier} vocabularies left "
-                    f"outside the walked set; it does not say {fragment!r}")
+            for field in ("statement", "evidence"):
+                actual[f"{item['id']}.{field}"] = item[field]
+    for field, expected in producer_domain_prose(registry).items():
+        require(actual.get(field) == expected,
+                f"formal_model {field} must equal its canonical producer-domain projection: {expected}")
 
 
 def check_invariant_domain(invariant: dict[str, Any], registry: dict[str, Any]) -> None:
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index 7958e5be20..f800f8e64b 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -13,7 +13,7 @@
   "formal_model": {
     "schema_version": "loopx_semantic_formal_model_v0",
     "universes": {
-      "vocabularies": "V: registered vocabulary identifiers; Producers(V) ⊆ V is the subset that declares producers: every tier=kernel vocabulary, plus any vocabulary of another tier that carries executed production evidence",
+      "vocabularies": "V: registered vocabulary identifiers; Producers(V) ⊆ V is exactly the subset declaring a producers key (including compatibility-only entries with an empty list). Kernel(V) ⊆ Producers(V). Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified.",
       "values": "U(v): ambient runtime values; S(v): registered admitted values",
       "sites": "L: source locations that define, produce, consume, interpret, pass through, project, or persist values",
       "scopes": "Scope: global or bounded_context(context_id); ScopeDeclarations are the forked names the registry declares as bounded contexts",
@@ -73,7 +73,7 @@
     "invariants": [
       {
         "id": "F1_producer_closedness",
-        "statement": "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Producers(V) is currently the six tier=kernel vocabularies plus settlement_binding_kind, the one cross_runtime vocabulary carrying an executed witness. Production outside that reach, and the 19 cross_runtime vocabularies still outside Producers(V), are unverified rather than proven closed.",
+        "statement": "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified. Production outside the scan reach is unverified rather than proven closed.",
         "enforcement": "m0_5",
         "evidence": "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES reach in loopx/semantics/production.py; check_producers visits only vocabularies that declare producers, and validate_production claims no whole-program closedness; unresolved dynamic sites are reported, not treated as proven safe",
         "domain": {
@@ -85,7 +85,7 @@
       },
       {
         "id": "F2_canonical_value_liveness",
-        "statement": "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). The 19 cross_runtime vocabularies outside Producers(V) are never walked, so liveness there is unverified rather than proven.",
+        "statement": "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified. Liveness outside the walked set is not proven.",
         "enforcement": "m0_5",
         "evidence": "every value of a vocabulary in Producers(V) has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted",
         "domain": {
diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py
index 8a056c235f..6509d62086 100644
--- a/tests/architecture/test_semantic_vocabulary_drift.py
+++ b/tests/architecture/test_semantic_vocabulary_drift.py
@@ -520,53 +520,53 @@ def test_f1_f2_domain_names_exactly_the_vocabularies_the_producer_check_walks()
         assert domain["evidence_bound"] == "producer_scan_reach"
 
 
-def test_prose_may_not_deny_a_producer_the_check_walks() -> None:
-    """The statement a human reads is held to the set the checker walks.
-
-    The machine domain and the prose were independent: the registry counted a
-    cross-runtime producer into F1/F2 and reported 7/26 while the same file
-    still called the kernel tier the only one declaring producers. Nothing was
-    red, because no check read both. Each mutation below restores one half of
-    that contradiction.
-    """
+@pytest.mark.parametrize("denial", [
+    " The cross_runtime tier declares no producers.",
+    " No vocabulary in the cross_runtime tier has any producer.",
+])
+def test_canonical_producer_statement_rejects_contradictory_paraphrases(denial: str) -> None:
     smoke = runpy.run_path(str(SMOKE))
     registry = copy.deepcopy(smoke["load_registry"]())
+    _invariant(registry, "F2_canonical_value_liveness")["statement"] += denial
+    with pytest.raises(smoke["Drift"], match="canonical producer-domain projection"):
+        smoke["check_formal_model"](registry["formal_model"], registry)
+
+
+def test_generated_domain_accepts_true_kernel_comparison() -> None:
+    smoke = runpy.run_path(str(SMOKE))
+    registry = smoke["load_registry"]()
     model = registry["formal_model"]
+    assert "Kernel(V) ⊆ Producers(V)." in model["universes"]["vocabularies"]
     smoke["check_formal_model"](model, registry)
+    domain = smoke["ProducerDomain"].from_registry(registry)
+    assert domain.kernel < domain.walked
+    assert domain.walked - domain.kernel == {"settlement_binding_kind"}
+    assert domain.outside_by_tier == (("cross_runtime", 19),)
 
-    kernel_only = copy.deepcopy(registry)
-    kernel_only["formal_model"]["universes"]["vocabularies"] = (
-        "V: registered vocabulary identifiers; Kernel(V) \u2286 V is the tier=kernel "
-        "subset, the only tier that declares producers"
-    )
-    with pytest.raises(smoke["Drift"], match="Kernel\\(V\\)"):
-        smoke["check_formal_model"](kernel_only["formal_model"], kernel_only)
 
-    denial = copy.deepcopy(registry)
-    _invariant(denial, "F2_canonical_value_liveness")["statement"] += (
-        " The cross_runtime tier declares no producers."
+def test_canonical_domain_rejects_old_kernel_only_universe() -> None:
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke["load_registry"]())
+    registry["formal_model"]["universes"]["vocabularies"] = (
+        "V: registered vocabulary identifiers; Kernel(V) is the only producer domain"
     )
-    with pytest.raises(smoke["Drift"], match="declares no producers"):
-        smoke["check_formal_model"](denial["formal_model"], denial)
+    with pytest.raises(smoke["Drift"], match="canonical producer-domain projection"):
+        smoke["check_formal_model"](registry["formal_model"], registry)
 
 
-def test_prose_must_keep_naming_what_stays_outside_the_walked_set() -> None:
-    """Stating only the verified half lets the unverified remainder go quiet."""
+def test_domain_membership_change_requires_regenerated_prose() -> None:
     smoke = runpy.run_path(str(SMOKE))
     registry = copy.deepcopy(smoke["load_registry"]())
-    vocabularies = registry["vocabularies"]
-    outside = [name for name, entry in vocabularies.items() if "producers" not in entry]
-    tiers = {vocabularies[name]["tier"] for name in outside}
-    assert tiers == {"cross_runtime"}, tiers
-
-    statement = _invariant(registry, "F1_producer_closedness")["statement"]
-    fragment = f"{len(outside)} cross_runtime"
-    assert fragment in statement, statement
-    _invariant(registry, "F1_producer_closedness")["statement"] = statement.replace(
-        fragment, "the remaining cross_runtime"
-    )
-    with pytest.raises(smoke["Drift"], match="left outside the walked set"):
+    # A membership change must not leave yesterday's tier/count claim green,
+    # even if the independent numeric domain entries were already updated.
+    registry["vocabularies"]["settlement_binding_kind"].pop("producers")
+    for invariant_id in ("F1_producer_closedness", "F2_canonical_value_liveness"):
+        _invariant(registry, invariant_id)["domain"]["verified"] = 6
+    with pytest.raises(smoke["Drift"], match="canonical producer-domain projection"):
         smoke["check_formal_model"](registry["formal_model"], registry)
+    projected = smoke["producer_domain_prose"](registry)
+    assert "20 cross_runtime" in projected["F1_producer_closedness.statement"]
+    assert "6 kernel and 0 outside" in projected["universes.vocabularies"]
 
 
 @pytest.mark.parametrize("invariant_id", sorted({

From e7ea7ec1ebf108654dfb0606ea7810ed4d24286f Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Sat, 19 Sep 2026 23:20:59 -0400
Subject: [PATCH 5/5] docs(semantics): explain canonical domain statement
 validation

Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 .../rfcs/semantic-vocabulary-convergence-v0.md            | 8 ++++++++
 .../rfcs/semantic-vocabulary-convergence-v0.zh-CN.md      | 6 ++++++
 2 files changed, 14 insertions(+)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 5fbe427152..8740a867d3 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -566,6 +566,14 @@ executed production evidence; `Produced_scan(v)` is the production the fixed
 forms observe inside the code-owned scan reach; `ScopeDeclarations` are the
 forked names the registry declares as bounded contexts.
 
+The machine-readable universe and F1/F2 statement/evidence fields are canonical
+projections of `ProducerDomain`: the walked vocabulary names, kernel membership,
+and outside counts by tier. The drift smoke requires exact agreement with that
+projection, including the valid `Kernel(V) ⊆ Producers(V)` comparison. These
+fields are generated statements, not free-form prose checked for forbidden
+phrases; arbitrary paraphrases are not interpreted as formal evidence. The RFC
+explanation remains subject to human review.
+
 1. **Producer closedness (vocabularies declaring producers):** `∀v ∈
    Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v)`. A recognised producer cannot
    write a value outside the registered set. `Producers(V)` is currently the six
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
index 25307306ad..489d7e40f6 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -452,6 +452,12 @@ R ⊆ L × V × Version               将值持久化
 生产证据的词表；`Produced_scan(v)` 是固定形式在代码所有的扫描范围内观察到的
 生产；`ScopeDeclarations` 是注册表声明为有界上下文的那些分叉名字。
 
+机器可读的 universe 和 F1/F2 statement/evidence 字段是 `ProducerDomain` 的规范化
+投影：被检查的词表名字、kernel 成员关系，以及按 tier 划分的域外数量。漂移检查要求
+这些字段与投影完全一致，其中包含合法的 `Kernel(V) ⊆ Producers(V)` 集合关系。
+这些字段是生成的陈述，不是通过禁用短语来检查的自由文本；任意改写不被推断为
+形式化证据。RFC 的解释文字仍需人工评审。
+
 1. **生产闭包（声明了 producers 的词表）：** `∀v ∈ Producers(V): Produced_scan(v) ⊆
    S(v) ⊆ U(v)`。被识别的生产者不能写入注册集合之外的值。`Producers(V)` 目前是
    6 个 `tier: kernel` 词表，加上 `settlement_binding_kind`——唯一携带可执行 witness 的