feat(semantics): give settlement binding kind executed production evidence

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.

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)` 的附录条目保持原样：它是只追加的历史，记录当时准确。

docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md

@@ -560,19 +560,32 @@ 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.
+
+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
+   `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

docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md

@@ -447,17 +447,26 @@ 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` 是注册表声明为有界上下文的那些分叉名字。
+
+机器可读的 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 的
+   `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 符号