From 5eed237ef71310b8026c22f2bf492c4bc5555c72 Mon Sep 17 00:00:00 2001
From: song <liusongstep@gmail.com>
Date: Tue, 15 Sep 2026 20:08:40 +0800
Subject: [PATCH 1/5] docs(rfc): pin the semantics scan root, record the
 merge-order hazard, and add a target state

A fourth review of the M0 slice found three gaps in the RFC rather than
in the guard. The RFC said repository-wide while the inventory root and
every literal scan read loopx/ only; Section 3 now says so and lists
apps/ and examples/ as non-goals. Merging twelve upstream commits staled
the committed inventory, and replaying the scanner over the last twenty
upstream merges showed eight would do the same, so Section 10 records the
merge-order hazard and the interim regenerate rule, and Section 12 gains
Q9 for the maintainers' policy choice. The plan had ratchets but no
definition of done; Section 11 gains a target-state table and Section 12
gains Q10 (Turn vocabulary end state) and Q11 (identifier-counted
retirement budgets). SOURCE_SURFACES is recorded as bounded-context reuse
of one name, not a fork, in Section 5 and in the registry note, so nobody
lowers the budget by renaming it. No code path, budget, or anchor changes.

The premerge planner keeps python3 on purpose: every fleet command is
spelled that way and the runner smoke asserts the text; the interpreter
requirement is documented in Section 10 instead.

(cherry picked from commit 2099ea39e288a471d090da128cdcc6747174dc0a)
Signed-off-by: song <liusongstep@gmail.com>
---
 .../semantic-vocabulary-convergence-v0.md     | 142 +++++++++++++++++-
 ...emantic-vocabulary-convergence-v0.zh-CN.md | 109 +++++++++++++-
 loopx/semantics/vocabulary_v0.json            |   1 +
 3 files changed, 250 insertions(+), 2 deletions(-)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 17a18ab371..ee3a6e16b3 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -214,10 +214,19 @@ the TypeScript runtime each own one spelling of the same idea.
 - The later milestones that turn `effective_action` into a typed enum, split
   its three slots, publish the projection through the contract, and retire
   legacy fields and twins under existing repository rules.
+- The scan root is the `loopx/` package. "Repository-wide" in this RFC means
+  every carrier under `loopx/`, in both runtimes, not every file in the git
+  tree. The inventory `root` and every `literal_scan.roots` entry say `loopx`
+  and the smoke reads nothing else.
 
 ### Non-goals
 
 - Changing any runtime decision, payload shape, or wire format.
+- Scanning `apps/` (about 90 TypeScript files on the baseline) or `examples/`
+  (a dozen `effective_action` assertions in smokes). Those are consumers and
+  test doubles, not producers; a smoke that asserts an unregistered value is
+  invisible to M0 and is accepted as such until a milestone widens the root,
+  which would also raise the merge-order cost in Section 10.
 - Curating every closed set by hand. The inventory maps all of them; only
   vocabularies that cross a module or runtime boundary and are dispatched on
   are curated with owners, values, and relations.
@@ -275,6 +284,19 @@ Forbidden alternate authorities: a second registry, a per-module list that
 restates registered values, or a prose table that claims to be normative for a
 registered vocabulary.
 
+**Scope of a name (planned for M0.5, not in M0).** The collision rules are
+keyed by name, so they cannot tell a fork from four bounded contexts that
+happen to reuse one identifier. `SOURCE_SURFACES` is the first case: its four
+definitions in `global_risks.py`, `global_todos.py`, `summary_all.py`, and
+`pr_review.py` each list the data sources of that one CLI command, and the
+value sets are meant to differ. It is counted in `multi_value_forks` today and
+must not be "fixed" by renaming, because a rename lowers the number without
+changing the code's meaning. M0.5 adds a `scope` field to the registry with at
+least `global` and `bounded_context`, lets a bounded-context name be declared
+once with its owning contexts, and removes declared names from the fork
+budget. Until then the fork budget is a ceiling that contains this one known
+misclassification, recorded in the registry's `inventory_ratchets` note.
+
 ### State model and schema
 
 `loopx/semantics/vocabulary_v0.json`, `schema_version`
@@ -400,6 +422,9 @@ inventory in the same PR.
 | Measurement covers both carrier shapes and filters local naming | `pytest tests/architecture/test_semantic_inventory.py` | pass, including the collision and module-local-convention fixtures | Rules come from this RFC, not from scanner output |
 | No behavior change from the two owner fixes | `pytest tests/test_loopx_turn_transaction.py tests/test_loop_turn_loop_controller.py tests/test_turn_loop_disposition.py tests/test_loopx_turn_managed_step.py tests/control_plane -k authority` and `loopx canary premerge --from-git-diff` | pass | Environment failures already present on `main` are excluded when reproduced on a clean tree |
 | Docs governance accepts the RFC pair | `python3 examples/docs-governance-smoke.py` | pass | Checks mirror, links, index |
+| Retirement budgets count substrings, not identifiers | `goal_boundary` counted with `in file.text` and with `\bgoal_boundary\b` | 35 vs 30 Python modules on the baseline | Known boundary; M3's zero-reader gate needs the identifier count, tracked in Section 12 |
+| The module-local convention filter is a code edit | Widen `MODULE_LOCAL_CONVENTION` in `inventory.py` and regenerate | `*_semantic` budgets fall with no code change elsewhere | Known boundary; the regex is in code so the widening is a reviewed diff, and the unfiltered totals stay budgeted |
+| An upstream merge can stale the committed inventory | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Measured cost of committing a snapshot; the handling rule is Section 10 and Section 12 Q9 |
 
 Known limits, stated so the check is not over-trusted:
 
@@ -446,6 +471,28 @@ for a diff touching `loopx/control_plane/` alone, and the fleet workflow is
 deliberately not a PR-required check. A fleet-discovered smoke is not a
 commit-time check until a required PR job collects it.
 
+**Merge-order hazard.** `inventory_v0.json` is a committed snapshot of the
+whole `loopx/` tree, and the smoke fails when the tree and the snapshot differ.
+Two pull requests that each add a carrier and each regenerate the inventory are
+both green against the `main` they were built on; whichever merges second
+leaves `main` with a snapshot missing the first one's entries, and the sweep on
+`main` is red until someone regenerates. On the last twenty merges to
+`upstream/main`, eight changed at least one carrier, so this is a weekly event,
+not a corner case. The first upstream sync of this branch reproduced it: twelve
+merged commits added one enum and three closed sets and the check failed
+until regenerated. The handling rule is Section 12 Q9; until it is decided, the
+rule is that the person who merges a PR after a red `main` regenerates the
+inventory in a follow-up commit that touches only `inventory_v0.json`, and the
+smoke's failure text names that command.
+
+**Interpreter.** The smoke, the generator, and the scanner require the
+project's Python (`>=3.11` in `pyproject.toml`); `zip(strict=True)` fails on
+3.9. Fleet and premerge commands are spelled `python3` by repository convention
+and run under the CI interpreter. A macOS system `python3` is 3.9, so local
+premerge runs need a 3.11 environment on `PATH`; the docs spell the direct
+commands as `python3.11` for that reason, and the planner entry is left as
+`python3` on purpose.
+
 ## 11. Normative delivery plan
 
 | Milestone | Shipped behavior | Entry gate | Exit evidence | Rollback |
@@ -456,6 +503,24 @@ commit-time check until a required PR job collects it.
 | M3 | Per-field retirement of legacy should-run fields, one field per PR, budgets lowered to zero and the field removed | Field has zero external readers proven by producer/reader research | Schema-reduction record per `AGENTS.md`; Appendix B entry | Restore field from the last writer |
 | M4 | Twin budget lowered with each replacement-first cutover from the migration RFC | Each cutover PR | Budget edit in the same diff | None needed; budget follows code |
 
+A ratchet without a target is a direction, not a plan. The table below is the
+state at which this RFC is complete; each row is a registry budget or a
+vocabulary property the smoke can check. Rows marked *open* wait on a Section
+12 decision and are the reason the plan is a skeleton until those are recorded.
+
+| Surface | Baseline (`1dc6ad8d8`) | Target when this RFC closes | Reached by |
+| --- | --- | --- | --- |
+| `effective_action` values | 33 literals, no owner symbol | one enum owner; `skip`, `observe_replay`, `block_replay`, and the two `quota_action_selection_*` codes gone from the decision slot; about 28 values | M1 |
+| `effective_action` slots in one envelope | 3 vocabularies under one field name | 1, or a registered union if Q6 keeps the field | M1 (Q6) |
+| Turn vocabularies | 3 sets, 28 values, 21 distinct, 7 redundant spellings | 3 sets kept; projection and decision table generated and checked; spellings unchanged unless Q10 sets a merge | M2 (Q2, Q10 *open*) |
+| Same-runtime forks, semantic | 18 names | 0 | baseline PRs |
+| Conflicting values, semantic | 2 names | 0 | baseline PRs |
+| Multi-value forks | 4 (1 misclassified) | 0 after `scope` declares bounded-context names | M0.5 + baseline PRs |
+| Multi-value twins | 19 | 0 | baseline PRs |
+| Legacy should-run fields | 6 fields, 124 py / 10 ts module mentions | 0 fields | M3, identifier-counted |
+| Merge-candidate groups | 32 unreviewed | every group classified; only `same_semantics` groups merged | classification PR, then per-group PRs |
+| Control-plane py/ts twins | 43 | follows the TypeScript migration RFC; no target here | M4 |
+
 ## 12. Open decisions
 
 1. **Registry location.** Owner: kernel maintainers. M0 implements
@@ -468,7 +533,12 @@ commit-time check until a required PR job collects it.
    `wait`), and `stop`, `terminal`, `contract_error` exist on one side only.
    The `same_concept` relations record the four shared verdicts.
    Recommendation: keep both, publish the projection in M2, revisit after the
-   managed-step consumer matures. Needed before M2.
+   managed-step consumer matures. Needed before M2. The stated reason for
+   keeping both is that merging would touch persisted Turn records; that
+   premise is unverified. Before deciding, a producer check should establish
+   whether `turn_route` is ever written to the journal or a receipt, or only
+   flows in-process; if the latter, the cost of a merge is far lower than this
+   RFC assumes and Q10 applies.
 3. **Owner module for `EffectiveAction`.** The registry declares no owner
    today because no symbol exists; the literal scan is the only check.
    Options: `quota/should_run_packet.py` (largest producer), a new
@@ -499,6 +569,30 @@ commit-time check until a required PR job collects it.
    with three or more external consumer modules or a cross-runtime twin must be
    curated. Recommendation: yes as a review rule now, enforced by the smoke
    only after a quarter of inventory history exists. Owner: kernel maintainers.
+9. **Inventory freshness across merges.** The committed snapshot goes stale
+   when two carrier-adding PRs merge in sequence (Section 10, eight of the last
+   twenty upstream merges). Options: (a) branch protection requires the PR to
+   be up to date with `main`, which removes the hazard and slows every PR;
+   (b) the merger owns a regenerate-only follow-up commit, which keeps the
+   snapshot in git history and accepts a red `main` for minutes; (c) the
+   inventory is not committed and CI generates it for the PR diff only, which
+   loses `git blame` on carriers. Recommendation: (b) now, (a) if red `main`
+   exceeds once a week. Owner: repository maintainers. This is an operations
+   decision, not a code change; it belongs in the tracking issue's decision
+   list, not its task list.
+10. **Target state for the Turn vocabularies.** Section 11's target table
+   keeps three sets and seven redundant spellings by default because Q2
+   recommends keeping both. If the producer check in Q2 shows `turn_route` is
+   not persisted, the maintainers should choose between (a) three sets with a
+   generated projection, the current plan, and (b) a two-phase merge (dual-
+   write, then retire) to one spelling per concept. Without this decision the
+   RFC has budgets but no definition of done for its headline problem.
+   Owner: Turn driver owner. Needed before M2 closes.
+11. **Retirement budgets by identifier.** The six legacy-field budgets count
+   `field in file.text`; `goal_boundary` matches `goal_boundary_repair`. M3's
+   zero-external-reader gate needs word-boundary counting, which lowers all six
+   anchors in one diff. Recommendation: do it before the first M3 PR.
+   Owner: kernel maintainers.
 
 ## Appendix A: Execution ledger (non-normative)
 
@@ -599,6 +693,37 @@ commit-time check until a required PR job collects it.
   departing from the precedent; I10 added; Section 9 gains three rows; Section
   10 rewritten from one sentence to a surface table.
 
+### 2026-09-15 — M0 reviewed a fourth time: scope, merge order, target state
+
+- **Baseline:** `503991dd2` merged; `upstream/main` at `2f84af990`, twelve
+  commits ahead of the branch.
+- **Trigger:** a fourth review asked what the guard's inputs depend on and
+  what "repository-wide" covers. Merging the twelve upstream commits into a
+  scratch tree staled the inventory (one enum, three closed sets); replaying
+  the scanner over the last twenty upstream merges showed eight would have
+  done the same. The RFC said repository-wide while the inventory root and
+  every literal scan said `loopx/`; `examples/` holds a dozen
+  `effective_action` assertions and `apps/` about ninety TypeScript files the
+  smoke never reads.
+- **Also found:** `SOURCE_SURFACES` is four CLI commands each listing its own
+  data sources, not a fork; the name-keyed rule cannot express that. Retirement
+  budgets count substrings (35 vs 30 identifier modules for `goal_boundary`).
+  The plan had budgets but no target state, and its four entry decisions had
+  no owner deadline.
+- **Delivered:** Section 3 fixes the scan root to `loopx/` and names `apps/`
+  and `examples/` as non-goals; Section 5 previews the M0.5 `scope` field with
+  `SOURCE_SURFACES` as the first case; Section 9 gains three known-boundary
+  rows; Section 10 gains the merge-order hazard and interpreter paragraphs;
+  Section 11 gains the target-state table; Section 12 gains Q9 to Q11 and a
+  verification note on Q2; the registry's `inventory_ratchets` gains a note on
+  the misclassified fork. No code or budget changed.
+- **Not done on purpose:** the premerge planner keeps `python3`, because every
+  fleet command is spelled that way and the runner smoke asserts the text; the
+  interpreter requirement is documented instead.
+- **Evidence:** Appendix C, E17 to E20.
+- **Effect on normative design:** Section 3 scope narrowed to match the code;
+  Section 11 now has a definition of done; Section 12 gains three decisions.
+
 ## Appendix B: Decision log
 
 | Date | Decision | Owner / approval | Alternatives | Normative sections changed |
@@ -624,6 +749,10 @@ commit-time check until a required PR job collects it.
 | E14 | The smoke was not on the pull-request path | `1dc6ad8d8` + M0 | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py --changed-file loopx/control_plane/quota/turn_envelope.ts`; `.github/workflows/full-public-smokes.yml` triggers | 32 commands planned, smoke absent; fleet runs on push to `main` and schedule only | Selection by path token; CI wiring read from the workflow files |
 | E15 | A tightened budget could drift back to its anchor | `1dc6ad8d8` + M0 | `ratchets[key] <= BUDGET_ANCHOR[key]` and `floor[key] >= anchored` in the smoke | any value between the tightened budget and the anchor passed | Code reading; the precedent uses the same comparison |
 | E16 | Equality closes the stall and the wrapper reaches the sweep | `1dc6ad8d8` + M0 | lower one `inventory_ratchets` entry with the anchor untouched, then `pytest tests/architecture/test_semantic_vocabulary_drift.py` on the clean tree | the mutation fails naming both values; the wrapper passes in about three seconds | Local exercise plus committed test |
+| E17 | Upstream merges stale the committed inventory | `upstream/main` `2f84af990`, last 20 first-parent merges | scanner facts of every changed `loopx/**/*.{py,ts}` compared between first parent and merge | 8 of 20 merges change at least one carrier; the branch's own upstream sync added 1 enum and 3 closed sets | Facts-level comparison, equivalent to a full regenerate |
+| E18 | Declared scope exceeded the scan root | `503991dd2` + M0 | `literal_scan.roots` and inventory `root` read from the registry; `grep` for `effective_action` dispatch literals under `examples/`; count of `.ts`/`.tsx` under `apps/` | roots are `loopx` only; 12+ assertions in `examples/`; 90 files in `apps/` | Consumers and test doubles, not producers |
+| E19 | `SOURCE_SURFACES` is four bounded contexts, not a fork | `503991dd2` | the four `multi_value_forks` definitions read from the inventory | each module lists the data sources of its own CLI command with disjoint values | Judgement from reading the values; the rule cannot make it |
+| E20 | Retirement budgets over-count by substring | `503991dd2` | `'goal_boundary' in text` vs `\bgoal_boundary\b` over `loopx/**/*.py` | 35 vs 30 modules | Identifier count is the M3 gate's measure |
 | E13 | The conflict budget mostly measured local naming | `1dc6ad8d8` | `MODULE_LOCAL_CONVENTION` applied to `conflicting_values` and `same_runtime_forks` names | 16 of 18 conflicts and 7 of 25 forks are module-local conventions; the semantic subsets are 2 and 18 | Classification is a name pattern, documented in the scanner and pinned by a fixture test |
 
 ## Appendix D: Rejected or superseded alternatives
@@ -662,3 +791,14 @@ projection proven to be a bijection after M2.
 - One field name can carry several vocabularies inside one envelope; a scan
   that sees the field cannot see the slot. Record the slots as a relation so
   the ambiguity is a registered fact, not an accident the registry blesses.
+- A committed snapshot of the whole tree makes the guard's input depend on
+  other people's merges. Measure how often the tree changes under it before
+  committing it, and write down who regenerates when `main` goes red.
+- A name-keyed collision rule needs a way to say "these are different things
+  that share a name". Without it the honest fix and the dishonest fix (a
+  rename) lower the same number, and reviewers cannot tell them apart.
+- When a document widens its scope faster than the code, the two must be
+  reconciled in whichever direction is cheaper, but they must match. A scope
+  claim the scanner does not implement is a false invariant.
+- Budgets that only go down describe a direction. Write the target table
+  before the second milestone, or nobody can say when the work is done.
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 10d46ce690..6d58815482 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -180,10 +180,17 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
   版本；六个旧 should-run 字段；控制面孪生数量；清单的分叉与冲突预算。
 - 后续里程碑：把 `effective_action` 变成类型化枚举、拆分其三个槽位、通过契约
   发布投影、按现有仓库规则退休旧字段与孪生模块。
+- 扫描根是 `loopx/` 包。本 RFC 说的"全仓库"指 `loopx/` 下两个运行时的全部
+  载体，不是 git 树里的每个文件。清单的 `root` 与每条 `literal_scan.roots`
+  都写 `loopx`，smoke 不读其他目录。
 
 ### 非目标
 
 - 改变任何运行时决策、载荷形状或线上格式。
+- 扫描 `apps/`（基线约 90 个 TypeScript 文件）或 `examples/`（十余处 smoke 里
+  的 `effective_action` 断言）。它们是消费者与测试替身，不是生产者；一个断言
+  了未注册值的 smoke 对 M0 不可见，在某个里程碑扩根之前接受这一点，扩根也会
+  抬高第 10 节的合并序成本。
 - 手工策展每个闭集。清单映射全部闭集；只有跨模块或跨运行时边界并被分发的
   词表才带 owner、值与关系进入策展层。
 - 取代 `turn_transaction_contract.json` 或
@@ -230,6 +237,16 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 禁止的替代权威：第二份注册表、复述已注册值的模块内列表，或宣称对已注册词表
 具有规范性的散文表格。
 
+**名字的作用域（计划在 M0.5，不在 M0）。** 碰撞规则按名字归组，因此分不清
+"一个分叉"与"四个恰好复用同一标识符的有界上下文"。`SOURCE_SURFACES` 是第一
+个案例：它在 `global_risks.py`、`global_todos.py`、`summary_all.py`、
+`pr_review.py` 的四处定义各自列出那一个 CLI 命令的数据来源，值集本来就该不
+同。它今天被计入 `multi_value_forks`，且不得用改名来"修"，因为改名只让数字
+下降、不改变代码含义。M0.5 给注册表加 `scope` 字段，至少含 `global` 与
+`bounded_context`，允许一个有界上下文名字连同其所属上下文声明一次，并把已
+声明的名字从分叉预算移出。在此之前分叉预算是一个包含这一处已知误分类的上
+限，记在注册表 `inventory_ratchets` 的备注里。
+
 ### 状态模型与 schema
 
 `loopx/semantics/vocabulary_v0.json`，`schema_version` 为
@@ -338,6 +355,9 @@ PR 中重新生成清单。
 | 度量覆盖两种载体形状并过滤局部命名 | `pytest tests/architecture/test_semantic_inventory.py` | 通过，含冲突与模块局部约定两组夹具 | 规则来自本 RFC 而非扫描输出 |
 | 两处 owner 修正不改变行为 | `pytest tests/test_loopx_turn_transaction.py tests/test_loop_turn_loop_controller.py tests/test_turn_loop_disposition.py tests/test_loopx_turn_managed_step.py tests/control_plane -k authority` 与 `loopx canary premerge --from-git-diff` | 通过 | 在干净树上可复现的 `main` 既有环境失败除外 |
 | 文档治理接受这对 RFC | `python3 examples/docs-governance-smoke.py` | 通过 | 检查镜像、链接、索引 |
+| 退休预算按子串而非标识符计数 | 分别以 `in file.text` 与 `\bgoal_boundary\b` 统计 `goal_boundary` | 基线上 35 对 30 个 Python 模块 | 已知边界；M3 的零读者门需要标识符计数，见第 12 节 |
+| 模块局部约定过滤器是一次代码修改 | 扩宽 `inventory.py` 的 `MODULE_LOCAL_CONVENTION` 并重新生成 | `*_semantic` 预算下降而别处无代码改动 | 已知边界；正则在代码里，扩宽是可评审的 diff，未过滤总数仍在预算内 |
+| 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 |
 
 已知边界，写明是为了不让这个检查被过度信任：
 
@@ -376,6 +396,22 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
 工作流被刻意设为非 PR 必需检查。舰队能发现的 smoke 不是提交时检查，除非某个
 必需的 PR 作业收集它。
 
+**合并序风险。** `inventory_v0.json` 是整个 `loopx/` 树的已提交快照，树与快照
+不一致时 smoke 失败。两个各自新增载体、各自正确再生成清单的 PR，对着它们
+各自基于的 `main` 都是绿的；后合并的那个会让 `main` 的快照缺少先合并者的
+条目，`main` 上的扫描在有人再生成之前是红的。对 `upstream/main` 最近二十次
+合并的重放显示有八次至少改变一个载体，所以这是每周会发生的事，不是边角。
+本分支第一次同步上游就复现了它：合入的十二个提交新增一个枚举与三个闭集，
+检查失败直到重新生成。处理规则是第 12 节 Q9；在其决定之前的规则是：在
+`main` 变红之后合并 PR 的人负责跟一个只改 `inventory_v0.json` 的再生成提交，
+smoke 的失败文本会点名那条命令。
+
+**解释器。** smoke、生成器与扫描器要求项目声明的 Python（`pyproject.toml`
+中 `>=3.11`）；`zip(strict=True)` 在 3.9 上失败。舰队与 premerge 的命令按仓库
+约定写作 `python3`，在 CI 解释器下运行。macOS 系统 `python3` 是 3.9，本地
+premerge 需要 `PATH` 上有 3.11 环境；文档因此把直接命令写成 `python3.11`，
+planner 条目则有意保留 `python3`。
+
 ## 11. 规范性交付计划
 
 | 里程碑 | 交付行为 | 进入门 | 退出证据 | 回滚 |
@@ -386,6 +422,23 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
 | M3 | 逐字段退休旧 should-run 字段，每个 PR 一个字段，预算降到零并删除字段 | 经生产者/读者调研证明该字段外部读者为零 | 按 `AGENTS.md` 的 schema 缩减记录；附录 B 条目 | 从最后一个写方恢复字段 |
 | M4 | 随迁移 RFC 的每次 replacement-first 切换调低孪生预算 | 每个切换 PR | 同 diff 中的预算修改 | 无需；预算跟随代码 |
 
+没有目标的棘轮只是方向，不是计划。下表是本 RFC 完成时的状态；每一行都是一个
+注册表预算或 smoke 可检查的词表属性。标为*未决*的行等待第 12 节的决策，这也
+是计划在那些决策记录之前只是骨架的原因。
+
+| 表面 | 基线（`1dc6ad8d8`） | 本 RFC 关闭时的目标 | 由谁达成 |
+| --- | --- | --- | --- |
+| `effective_action` 取值 | 33 个字面量，无 owner 符号 | 一个枚举 owner；`skip`、`observe_replay`、`block_replay` 与两个 `quota_action_selection_*` 码从判定槽位移出；约 28 值 | M1 |
+| 同一 envelope 里的 `effective_action` 槽位 | 一个字段名下 3 套词表 | 1，或在 Q6 保留字段时为一个已注册并集 | M1（Q6） |
+| Turn 词表 | 3 套、28 值、21 个不同值、7 个冗余拼法 | 保留 3 套；投影与决策表生成并校验；拼法不变，除非 Q10 决定合并 | M2（Q2、Q10 *未决*） |
+| 同运行时分叉（语义） | 18 个名字 | 0 | 基线窄 PR |
+| 冲突值（语义） | 2 个名字 | 0 | 基线窄 PR |
+| 多值分叉 | 4（1 个误分类） | `scope` 声明有界上下文名字后为 0 | M0.5 + 基线窄 PR |
+| 多值孪生 | 19 | 0 | 基线窄 PR |
+| 旧 should-run 字段 | 6 个字段，124 py / 10 ts 模块提及 | 0 个字段 | M3，按标识符计数 |
+| 合并候选组 | 32 组未评审 | 每组已分类；只合并 `same_semantics` 的组 | 分类表 PR，随后逐组 PR |
+| 控制面 py/ts 孪生 | 43 | 跟随 TypeScript 迁移 RFC；本 RFC 不设目标 | M4 |
+
 ## 12. 未决决策
 
 1. **注册表位置。** Owner：内核维护者。M0 实现于 `loopx/semantics/`，因为范围是
@@ -396,7 +449,10 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
    投影覆盖全部输入但非单射（`blocked` 与 `wait` 都映到 `wait`），而 `stop`、
    `terminal`、`contract_error` 只在一侧存在。`same_concept` 关系记录了四个共享
    裁决。建议：两者都保留，M2 发布投影，待 managed-step 消费者成熟后再议。
-   M2 前需定。
+   M2 前需定。保留两者的理由是合并会触及已持久化的 Turn 记录；这个前提尚未
+   核实。决定之前应先用生产者检查确认 `turn_route` 是否曾写入 journal 或
+   receipt，还是只在进程内流转；若是后者，合并的代价远低于本 RFC 的假设，
+   适用 Q10。
 3. **`EffectiveAction` 的 owner 模块。** 注册表今天不声明 owner，因为不存在任何
    符号；字面量扫描是唯一检查。选项：`quota/should_run_packet.py`（最大生产者）、
    新建 `quota/effective_action.py`，或按迁移 RFC 以 TypeScript `turn_envelope.ts`
@@ -419,6 +475,22 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
 8. **从清单到注册表的晋升规则。** 外部消费者模块不少于三个或存在跨运行时孪生
    的已映射载体是否必须策展。建议：现在作为评审规则采用，待清单积累一个季度
    历史后再由 smoke 强制。Owner：内核维护者。
+9. **跨合并的清单新鲜度。** 两个新增载体的 PR 先后合并时，已提交快照会过期
+   （第 10 节；上游最近二十次合并中八次）。选项：(a) 分支保护要求 PR 与
+   `main` 同步，根除风险但拖慢所有 PR；(b) 合并者负责一个只再生成的后续提交，
+   快照留在 git 历史里，接受 `main` 红几分钟；(c) 清单不入库，CI 只对 PR diff
+   生成，失去对载体的 `git blame`。建议：现在用 (b)，若 `main` 变红超过每周
+   一次则改 (a)。Owner：仓库维护者。这是运维决策不是代码改动；应放在跟踪
+   issue 的决策清单里，而不是任务清单里。
+10. **Turn 词表的终态。** 第 11 节的目标表默认保留三套与七个冗余拼法，因为
+   Q2 建议保留两者。若 Q2 的生产者检查表明 `turn_route` 未被持久化，维护者
+   应在 (a) 三套加生成投影（现行计划）与 (b) 两阶段合并（先双写、后退休）到
+   每个概念一种拼法之间选择。没有这个决定，RFC 对其标题问题只有预算、没有
+   完成定义。Owner：Turn driver owner。M2 关闭前需定。
+11. **退休预算按标识符计数。** 六个旧字段预算用 `field in file.text` 统计；
+   `goal_boundary` 会匹配 `goal_boundary_repair`。M3 的零外部读者门需要词边界
+   计数，这会在一个 diff 里调低全部六个锚点。建议：在第一个 M3 PR 之前做。
+   Owner：内核维护者。
 
 ## 附录 A：执行账本（非规范）
 
@@ -502,6 +574,29 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
 - **对规范设计的影响：** I5 改述为相等并说明偏离先例的理由；新增 I10；第 9 节
   增三行；第 10 节从一句话改写为表面表格。
 
+### 2026-09-15 — 第四次评审 M0：范围、合并序、终态
+
+- **基线：** 已合入 `503991dd2`；`upstream/main` 在 `2f84af990`，领先分支十二
+  个提交。
+- **触发：** 第四次评审问守卫的输入依赖什么、"全仓库"覆盖什么。把十二个上游
+  提交合入临时树后清单过期（一个枚举、三个闭集）；对上游最近二十次合并重放
+  扫描器，八次会有同样结果。RFC 写全仓库，而清单根与每条字面量扫描都写
+  `loopx/`；`examples/` 有十余处 `effective_action` 断言，`apps/` 约九十个
+  TypeScript 文件，smoke 从不读取。
+- **同时发现：** `SOURCE_SURFACES` 是四个 CLI 命令各列自己的数据来源，不是分
+  叉；按名归组的规则无法表达这一点。退休预算按子串计数（`goal_boundary` 35
+  对 30 个标识符模块）。计划有预算但没有终态，四个入口决策没有 owner 期限。
+- **交付：** 第 3 节把扫描根固定为 `loopx/` 并把 `apps/` 与 `examples/` 列为
+  非目标；第 5 节预告 M0.5 的 `scope` 字段并以 `SOURCE_SURFACES` 为首例；第 9
+  节增三行已知边界；第 10 节增合并序风险与解释器两段；第 11 节增终态表；第
+  12 节增 Q9 到 Q11 并给 Q2 加核实说明；注册表 `inventory_ratchets` 增一条关于
+  误分类分叉的备注。代码与预算未变。
+- **有意不做：** premerge planner 保留 `python3`，因为舰队所有命令都这样拼写，
+  runner smoke 也断言了这段文本；改为记录解释器要求。
+- **证据：** 附录 C 的 E17 到 E20。
+- **对规范设计的影响：** 第 3 节范围收窄以匹配代码；第 11 节有了完成定义；第
+  12 节增三条决策。
+
 ## 附录 B：决策日志
 
 | 日期 | 决策 | Owner / 批准 | 备选 | 变更的规范章节 |
@@ -527,6 +622,10 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
 | E14 | smoke 不在 PR 路径上 | `1dc6ad8d8` + M0 | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py --changed-file loopx/control_plane/quota/turn_envelope.ts`；`.github/workflows/full-public-smokes.yml` 的触发条件 | 规划 32 条命令，smoke 缺席；舰队只在 push 到 `main` 与日程运行 | 按路径 token 选择；CI 接线读自工作流文件 |
 | E15 | 已收紧的预算可以漂回锚点 | `1dc6ad8d8` + M0 | smoke 中的 `ratchets[key] <= BUDGET_ANCHOR[key]` 与 `floor[key] >= anchored` | 收紧后的预算与锚点之间的任何值都能通过 | 代码阅读；先例用同样的比较 |
 | E16 | 相等性关闭停滞，包装进入扫描 | `1dc6ad8d8` + M0 | 只调低一个 `inventory_ratchets` 条目而不动锚点，然后在干净树上跑 `pytest tests/architecture/test_semantic_vocabulary_drift.py` | 突变失败并同时命名两个值；包装约 3 秒通过 | 本地练习加已提交测试 |
+| E17 | 上游合并会让已提交清单过期 | `upstream/main` `2f84af990`，最近 20 个 first-parent 合并 | 对每个改动的 `loopx/**/*.{py,ts}` 在第一父提交与合并结果之间比较扫描器事实 | 20 次合并中 8 次至少改变一个载体；本分支自己的上游同步新增 1 个枚举与 3 个闭集 | 事实级比较，等价于完整再生成 |
+| E18 | 声明范围超出扫描根 | `503991dd2` + M0 | 从注册表读 `literal_scan.roots` 与清单 `root`；在 `examples/` 下 `grep` `effective_action` 分发字面量；统计 `apps/` 下 `.ts`/`.tsx` | 根只有 `loopx`；`examples/` 12+ 处断言；`apps/` 90 个文件 | 消费者与测试替身，非生产者 |
+| E19 | `SOURCE_SURFACES` 是四个有界上下文，不是分叉 | `503991dd2` | 从清单读出四个 `multi_value_forks` 定义 | 每个模块列出自己 CLI 命令的数据来源，值互不相交 | 读值后的判断；规则本身做不出 |
+| E20 | 退休预算按子串高估 | `503991dd2` | 对 `loopx/**/*.py` 分别用 `'goal_boundary' in text` 与 `\bgoal_boundary\b` | 35 对 30 个模块 | 标识符计数才是 M3 门的度量 |
 | E13 | 冲突预算主要在度量局部命名 | `1dc6ad8d8` | 对 `conflicting_values` 与 `same_runtime_forks` 名字应用 `MODULE_LOCAL_CONVENTION` | 18 个冲突中 16 个、25 个分叉中 7 个是模块局部约定；语义子集分别为 2 与 18 | 分类是名字模式，已在扫描器中说明并由夹具测试钉住 |
 
 ## 附录 D：被否决或取代的方案
@@ -555,3 +654,11 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。
   挪锚点。用相等性比较，两个值就分不开。
 - 同一个字段名可以在一个 envelope 里承载多套词表；看得见字段的扫描看不见
   槽位。把槽位记为关系，让歧义成为已登记的事实，而不是注册表背书的意外。
+- 整棵树的已提交快照让守卫的输入依赖别人的合并。提交它之前先量一下树在它
+  之下变化的频率，并写下 `main` 变红时由谁再生成。
+- 按名归组的碰撞规则需要一种方式说"这些是共用一个名字的不同东西"。没有它，
+  诚实的修法与不诚实的修法（改名）降低的是同一个数字，评审者分不出来。
+- 文档比代码更快地扩大范围时，两者必须朝更便宜的那个方向对齐，但必须一致。
+  扫描器没有实现的范围声明是一条假不变量。
+- 只降不升的预算描述的是方向。在第二个里程碑之前写出目标表，否则没人能说
+  工作何时完成。
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index f571a16438..c5294ab70c 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -665,6 +665,7 @@
     "same_runtime_forks_semantic": 18,
     "conflicting_values_semantic": 2,
     "multi_value_meaning": "Enums, named closed sets, Literal aliases, and TypeScript as-const arrays are vocabulary exactly as a NAME = \"value\" constant is, so they get the same collision rule. One name defined in two modules with identical values is a twin; with different values it is a fork.",
+    "multi_value_forks_note": "The 4 counted forks include SOURCE_SURFACES, whose four definitions are four CLI commands each listing its own data sources; that is bounded-context reuse of one name, not drift. It stays in the budget until M0.5 adds a scope field (RFC Section 5) and must not be removed by renaming.",
     "semantic_meaning": "same_runtime_forks_semantic and conflicting_values_semantic exclude module-local convention names such as SCHEMA_VERSION, COMMAND, or *_LABEL, which every module legitimately names for itself. The remaining names are shared vocabulary, where a duplicate is real drift rather than local naming; the unfiltered totals stay visible in the generated inventory summary."
   }
 }

From 075f82d6b1fe857ad3d2223e973a234c06c41f70 Mon Sep 17 00:00:00 2001
From: song <liusongstep@gmail.com>
Date: Tue, 15 Sep 2026 20:20:49 +0800
Subject: [PATCH 2/5] docs(rfc): define vocabulary roles and scope, add
 I11-I14, and gate M1 on an M0.5 slice

The RFC used producer and consumer nineteen times without defining
either, Q2 and Q10 waited on a producer check the document never
specified, scope existed only as a preview paragraph, and Section 1 still
said the smoke ran on every premerge and fleet run after Section 10 made
the pytest sweep the obligation.

Section 5 gains a roles table (owner, producer, interpreter,
pass-through) with one check per role, the fixed production forms, and
which tiers must list producers; the schema table gains scope, producers,
and compatibility_only. Section 2 gains I11 to I14, each marked enforced
from M0.5 so the M0 smoke is not claimed to do what it does not. Section 9
gains three M0.5 rows including the expected first failure on skip.
Section 11 gains the M0.5 milestone and M1 now gates on it. Q2 and Q10
point at I12 instead of an undefined check. Both language versions move
together; docs governance, the drift smoke, and the architecture tests
stay green. No code, registry value, or budget changed.

(cherry picked from commit a8bf889c7bd3dd1ccd9ffb230482aba7d6e46276)
Signed-off-by: song <liusongstep@gmail.com>
---
 .../semantic-vocabulary-convergence-v0.md     | 102 +++++++++++++++++-
 ...emantic-vocabulary-convergence-v0.zh-CN.md |  86 +++++++++++++--
 2 files changed, 176 insertions(+), 12 deletions(-)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index ee3a6e16b3..26d2ebb7e3 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -43,7 +43,8 @@ not amend normative sections.
    string enums, `Literal` aliases, named closed sets, TypeScript `as const`
    arrays, and every constant name defined in more than one module. A public
    smoke, `examples/semantic-vocabulary-drift-smoke.py`, checks the code against
-   both on every premerge and full-public run. A change that widens a
+   both inside the default `pytest` sweep on every pull request; premerge and
+   the full-public fleet are additional surfaces (Section 10). A change that widens a
    vocabulary, forks a constant, adds a carrier, or weakens the registry must
    edit the registry or regenerate the inventory in the same diff, so the
    reviewer sees the semantic change as a change.
@@ -196,6 +197,29 @@ the TypeScript runtime each own one spelling of the same idea.
   discovery under `examples/` and the `repo-architecture-budget` premerge
   profile are additional surfaces, not the obligation: the fleet runs after
   merge and on a schedule, and premerge selects by changed-path tokens.
+- **I11 Roles are distinct.** A vocabulary has one owner, some producers, some
+  interpreters, and some pass-throughs (Section 5, "Roles of a vocabulary").
+  Only the owner defines the set and only producers write values. Mentioning,
+  comparing, serializing, or displaying a value confers no ownership. An
+  interpreter or pass-through that starts writing a value has become a
+  producer and must be registered as one. Enforced from M0.5.
+- **I12 Every kernel value is produced.** For a `kernel` vocabulary, every
+  value not listed under `compatibility_only` has at least one production site
+  the fixed production forms recognise or a `variable_sourced_values` entry. A
+  value that is only compared is dead or compatibility-only, never canonical.
+  `skip` in `effective_action` is the first expected failure. Enforced from
+  M0.5; at M0 the literal scan accepts a compared value as carried.
+- **I13 Producers write registered values only.** A production site that
+  writes a value outside the registered set fails closed, independently of
+  whether any consumer compares it. Production is stricter than comparison: a
+  consumer comparing an unregistered value is dead code, a producer writing one
+  is protocol drift. Enforced from M0.5; the M0 literal scan covers both forms
+  together.
+- **I14 Scope is declared, not inferred.** A name defined in several modules
+  is a fork unless the registry declares it `bounded_context` and lists the
+  contexts and one owner symbol per context. Declared names leave the fork
+  budget; a rename does not change the budget's meaning and is not a fix.
+  Enforced from M0.5; at M0 `SOURCE_SURFACES` is counted as a fork and noted.
 
 ## 3. Scope and non-goals
 
@@ -294,9 +318,45 @@ must not be "fixed" by renaming, because a rename lowers the number without
 changing the code's meaning. M0.5 adds a `scope` field to the registry with at
 least `global` and `bounded_context`, lets a bounded-context name be declared
 once with its owning contexts, and removes declared names from the fork
-budget. Until then the fork budget is a ceiling that contains this one known
+budget (I14, the schema rows below, and the M0.5 row in Section 11). Until
+then the fork budget is a ceiling that contains this one known
 misclassification, recorded in the registry's `inventory_ratchets` note.
 
+### Roles of a vocabulary
+
+A module that mentions a value is not its owner, and a vocabulary has more
+than one kind of participant. The registry distinguishes four roles because
+the check that makes sense differs by role:
+
+| Role | What it does | Registered | Check |
+| --- | --- | --- | --- |
+| Owner | Defines the closed set as one `module::Symbol` per runtime | Yes, since M0 | I1 to I3 |
+| Producer | Writes a value into the field: assignment, dict or object literal, constructor keyword, `return` of a literal inside a listed deciding function, enum member on the owner | Yes for `kernel` vocabularies, from M0.5 | I12, I13 |
+| Interpreter | Branches on the value: `if`, `match`, `switch`, membership test | No; found by the dispatch scan, ranked by `--report` | I2, no unregistered comparison |
+| Pass-through | Serializes, persists, forwards, or displays the value without branching on it | No | None; a pass-through never becomes an owner |
+
+Two rules follow. A value with no producer is dead or compatibility-only:
+`skip` is compared in `todos/user_gate.py` and written nowhere, so M0 passes
+it and M0.5 fails it until it is removed or listed under `compatibility_only`.
+Production is stricter than comparison: M0.5 scans production forms on their
+own and fails on an unregistered produced value (I13), while the M0 literal
+scan keeps catching unregistered comparisons (I2). Interpreters and
+pass-throughs are deliberately not registered; otherwise every consumer edit
+would touch the registry, the churn Section 6 rejected for consumer counts.
+Their relations to a vocabulary are advisory output of `--report`.
+
+Production forms are fixed in the smoke at M0.5, like the dispatch forms:
+Python `x["f"] = "v"`, `f="v"` as a constructor keyword of the envelope or
+packet type, `return "v"` inside a function the registry lists as a producer,
+and member access on the owner enum; TypeScript `f: "v"` in an object
+literal, `x.f = "v"`, and the conditional expression. `variable_sourced_values`
+stays for the values a producer builds from a variable the scan cannot follow.
+Which vocabularies must list producers: `kernel` at M0.5; `cross_runtime` only
+when a value is added or removed after M0.5; `cross_module` only if promoted
+(Q8). Persistence is a property the production scan can answer: a producer
+whose listed symbol is a journal or receipt writer marks the vocabulary
+`persisted`, which is the fact Q2 and Q10 wait on.
+
 ### State model and schema
 
 `loopx/semantics/vocabulary_v0.json`, `schema_version`
@@ -310,6 +370,9 @@ vocabulary key fails the smoke.
 | `vocabularies.<name>.tier`, `status` | `kernel`, `cross_runtime`, `cross_module`; `canonical`, `legacy`, `merge_candidate` | Closed enumerations |
 | `vocabularies.<name>.literal_scan` | `field`, roots, suffixes | Every literal the fixed dispatch forms capture is registered; every registered value is captured or variable-sourced (I2) |
 | `vocabularies.<name>.variable_sourced_values` | value to producer module | The producer still contains the quoted value |
+| `vocabularies.<name>.scope` (M0.5) | `global` or `bounded_context`; a `bounded_context` entry lists `contexts`, each with one owner symbol | Closed enumeration; declared bounded-context names are excluded from `multi_value_forks`; an undeclared multi-module name stays a fork (I14) |
+| `vocabularies.<name>.producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one site or a variable-sourced entry (I12, I13) |
+| `vocabularies.<name>.compatibility_only` (M0.5) | values kept so readers of persisted records still resolve them | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone |
 | `vocabularies.<name>.value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values |
 | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves |
 | `relations.shared_field_names` | one field name, its slots and the vocabulary or values each carries | Every slot resolves |
@@ -424,6 +487,9 @@ inventory in the same PR.
 | Docs governance accepts the RFC pair | `python3 examples/docs-governance-smoke.py` | pass | Checks mirror, links, index |
 | Retirement budgets count substrings, not identifiers | `goal_boundary` counted with `in file.text` and with `\bgoal_boundary\b` | 35 vs 30 Python modules on the baseline | Known boundary; M3's zero-reader gate needs the identifier count, tracked in Section 12 |
 | The module-local convention filter is a code edit | Widen `MODULE_LOCAL_CONVENTION` in `inventory.py` and regenerate | `*_semantic` budgets fall with no code change elsewhere | Known boundary; the regex is in code so the widening is a reviewed diff, and the unfiltered totals stay budgeted |
+| A registered value nobody produces fails (M0.5) | Run the production-form scan on the baseline | Fails naming `effective_action` and `skip`; passes after `skip` is removed or listed `compatibility_only` | First expected I12 failure; a compared-only value is not carried |
+| A producer of an unregistered value fails (M0.5) | Write `effective_action: "brand_new"` in a listed producer site | Fails naming the site and the value even though no consumer compares it | I13; production is stricter than comparison |
+| A bounded-context name leaves the fork budget only by declaration (M0.5) | Declare `SOURCE_SURFACES` with its four contexts; separately, rename one definition without declaring | The declaration lowers `multi_value_forks` to 3; the rename alone does not | I14; the honest fix is a registry edit a reviewer sees, the rename is code without registry change |
 | An upstream merge can stale the committed inventory | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Measured cost of committing a snapshot; the handling rule is Section 10 and Section 12 Q9 |
 
 Known limits, stated so the check is not over-trusted:
@@ -498,7 +564,8 @@ commands as `python3.11` for that reason, and the planner entry is left as
 | Milestone | Shipped behavior | Entry gate | Exit evidence | Rollback |
 | --- | --- | --- | --- | --- |
 | M0 | Registry with 26 vocabularies and 9 relations, generated inventory with `--check`, drift smoke with fixed dispatch forms and coverage floor, two owner forks removed, RFC index entry | This RFC opened | Section 9 rows green; 20 mutation classes fail closed | Delete the smoke, `loopx/semantics/`, the generator, and its test |
-| M1 | `EffectiveAction` typed enum in one owner module; the replay observation and frontier slots split off (Q6); producers and consumers import it; registry `literal_scan` tightened to the enum | M0 merged; owner module chosen (Q3); slot split decided (Q6) | Smoke green; zero bare `effective_action` literals outside the owner; parity fixtures for status/should-run unchanged | Revert to literals; registry keeps the set |
+| M0.5 | `scope` with `global` and `bounded_context` and per-context owners; `producers` and `compatibility_only` on `kernel` vocabularies; production-form scan with the two role checks (I12, I13); retirement budgets counted by identifier with all six anchors lowered in one diff (Q11); merge-order rule from Q9 written into Section 10 | M0 merged; Q9 decided or its interim rule accepted | Smoke green with I11 to I14 enforced; `skip` resolved; `multi_value_forks` at 3 by declaration; Section 9 role rows green; `turn_route` persistence answered for Q2 | Remove the three fields and the role checks; budgets return to the M0 anchors |
+| M1 | `EffectiveAction` typed enum in one owner module; the replay observation and frontier slots split off (Q6); producers and consumers import it; registry `literal_scan` tightened to the enum | M0.5 merged; owner module chosen (Q3); slot split decided (Q6) | Smoke green; zero bare `effective_action` literals outside the owner; parity fixtures for status/should-run unchanged | Revert to literals; registry keeps the set |
 | M2 | Route-to-disposition projection, the `decide_loop_disposition` decision table, and the cross-runtime sets published through a shared contract with generated Python and TypeScript bindings, following the coordination contract generator | M1 merged; Q2 and Q7 decided | Generator `--check` and smoke green; `settlement.ts` and `transaction.py` read the generated set | Regenerate from prior contract |
 | M3 | Per-field retirement of legacy should-run fields, one field per PR, budgets lowered to zero and the field removed | Field has zero external readers proven by producer/reader research | Schema-reduction record per `AGENTS.md`; Appendix B entry | Restore field from the last writer |
 | M4 | Twin budget lowered with each replacement-first cutover from the migration RFC | Each cutover PR | Budget edit in the same diff | None needed; budget follows code |
@@ -535,7 +602,8 @@ vocabulary property the smoke can check. Rows marked *open* wait on a Section
    Recommendation: keep both, publish the projection in M2, revisit after the
    managed-step consumer matures. Needed before M2. The stated reason for
    keeping both is that merging would touch persisted Turn records; that
-   premise is unverified. Before deciding, a producer check should establish
+   premise is unverified. Before deciding, the M0.5 production-form scan (I12,
+   Section 5) applied to `turn_route` should establish
    whether `turn_route` is ever written to the journal or a receipt, or only
    flows in-process; if the latter, the cost of a merge is far lower than this
    RFC assumes and Q10 applies.
@@ -582,7 +650,7 @@ vocabulary property the smoke can check. Rows marked *open* wait on a Section
    list, not its task list.
 10. **Target state for the Turn vocabularies.** Section 11's target table
    keeps three sets and seven redundant spellings by default because Q2
-   recommends keeping both. If the producer check in Q2 shows `turn_route` is
+   recommends keeping both. If the M0.5 production-form scan in Q2 shows `turn_route` is
    not persisted, the maintainers should choose between (a) three sets with a
    generated projection, the current plan, and (b) a two-phase merge (dual-
    write, then retire) to one spelling per concept. Without this decision the
@@ -724,6 +792,24 @@ vocabulary property the smoke can check. Rows marked *open* wait on a Section
 - **Effect on normative design:** Section 3 scope narrowed to match the code;
   Section 11 now has a definition of done; Section 12 gains three decisions.
 
+### 2026-09-15 — Role and scope models written into the contract
+
+- **Trigger:** the RFC used "producer" and "consumer" nineteen times without
+  defining either, Q2 and Q10 depended on "a producer check" the document
+  never specified, `scope` existed only as a preview paragraph, and Section 1
+  still said the smoke ran "on every premerge and full-public run" after
+  Section 10 had made the pytest sweep the obligation.
+- **Delivered:** Section 5 gains "Roles of a vocabulary" (owner, producer,
+  interpreter, pass-through) and three schema rows (`scope`, `producers`,
+  `compatibility_only`); Section 2 gains I11 to I14, each marked as enforced
+  from M0.5; Section 9 gains three M0.5 rows; Section 11 gains the M0.5
+  milestone and M1 now gates on it; Q2 and Q10 point at I12 instead of an
+  undefined check; Section 1 matches Section 10. No code, registry value, or
+  budget changed; the M0 smoke does not yet enforce I11 to I14.
+- **Effect on normative design:** four invariants added with an explicit
+  enforcement milestone; the plan gains a definition of "produced" that M3's
+  zero-reader gate and Q2's persistence question can both use.
+
 ## Appendix B: Decision log
 
 | Date | Decision | Owner / approval | Alternatives | Normative sections changed |
@@ -802,3 +888,9 @@ projection proven to be a bijection after M2.
   claim the scanner does not implement is a false invariant.
 - Budgets that only go down describe a direction. Write the target table
   before the second milestone, or nobody can say when the work is done.
+- A decision that waits on "a check" the RFC never defines is a dangling
+  reference dressed as prudence. Name the invariant and the milestone that
+  delivers the check, or the decision has no input and never closes.
+- Using a role word (producer, consumer) nineteen times is not defining it.
+  Until the roles are a table with a check per role, "who writes this value"
+  is a question every reviewer answers differently.
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 6d58815482..1e0e71e239 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -37,8 +37,9 @@ RFC 成熟度与交付成熟度彼此独立。带日期的进度条目不修改
    以及仓库同意只降不升的预算。生成清单 `inventory_v0.json` 映射 `loopx/` 下
    每一个闭集载体：字符串枚举、`Literal` 别名、命名闭集、TypeScript `as const`
    数组，以及在多个模块中定义的每个常量名。一支公共 smoke
-   `examples/semantic-vocabulary-drift-smoke.py` 在每次 premerge 与 full-public
-   运行时用两份文件核对代码。任何扩宽词表、分叉常量、新增载体或削弱注册表的
+   `examples/semantic-vocabulary-drift-smoke.py` 在每个 PR 的默认 `pytest` 扫描
+   里用两份文件核对代码；premerge 与 full-public 舰队是附加表面（第 10 节）。
+   任何扩宽词表、分叉常量、新增载体或削弱注册表的
    改动，必须在同一个 diff 里修改注册表或重新生成清单，评审者因此能把语义
    变化当作变化看见。
 2. **什么不变。** 运行时行为、线上格式、枚举类本身。每个枚举继续住在自己的
@@ -165,6 +166,23 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
   扫描里，因此在每个运行 Python 测试的 PR 上失败即关闭。`examples/` 下的舰队
   发现与 `repo-architecture-budget` premerge profile 是附加表面，不是义务：
   舰队在合并后和按日程运行，premerge 按改动路径的 token 选择。
+- **I11 角色互异。** 一个词表有一个 owner、若干生产者、若干解释者与若干透传者
+  （第 5 节"词表的角色"）。只有 owner 定义集合，只有生产者写入值。提及、
+  比较、序列化或展示一个值不带来任何所有权。开始写入值的解释者或透传者已经
+  变成生产者，必须登记为生产者。自 M0.5 起强制。
+- **I12 每个内核值都被生产。** 对 `kernel` 词表，未列入 `compatibility_only`
+  的每个值至少有一个固定生产形式能识别的生产位点，或一条
+  `variable_sourced_values`。只被比较的值是死值或兼容值，绝不是 canonical。
+  `effective_action` 的 `skip` 是第一个预期失败。自 M0.5 起强制；M0 的字面量
+  扫描把被比较的值当作已携带。
+- **I13 生产者只写注册值。** 写入注册集合之外值的生产位点失败即关闭，与是否
+  有消费者比较它无关。生产比比较更严：消费者比较一个未注册值是死代码，生产
+  者写一个未注册值是协议漂移。自 M0.5 起强制；M0 的字面量扫描把两种形式合在
+  一起覆盖。
+- **I14 作用域靠声明而非推断。** 在多个模块中定义的名字是分叉，除非注册表把它
+  声明为 `bounded_context` 并列出各上下文及每个上下文一个 owner 符号。已声明
+  的名字离开分叉预算；改名不改变预算的含义，不算修复。自 M0.5 起强制；M0 把
+  `SOURCE_SURFACES` 计为分叉并加备注。
 
 ## 3. 范围与非目标
 
@@ -244,9 +262,38 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 同。它今天被计入 `multi_value_forks`，且不得用改名来"修"，因为改名只让数字
 下降、不改变代码含义。M0.5 给注册表加 `scope` 字段，至少含 `global` 与
 `bounded_context`，允许一个有界上下文名字连同其所属上下文声明一次，并把已
-声明的名字从分叉预算移出。在此之前分叉预算是一个包含这一处已知误分类的上
+声明的名字从分叉预算移出（I14、下方 schema 表与第 11 节的 M0.5 行）。在此之
+前分叉预算是一个包含这一处已知误分类的上
 限，记在注册表 `inventory_ratchets` 的备注里。
 
+### 词表的角色
+
+提及一个值的模块不是它的 owner，一个词表也不止一种参与者。注册表区分四种角
+色，因为对每种角色有意义的检查不同：
+
+| 角色 | 做什么 | 是否登记 | 检查 |
+| --- | --- | --- | --- |
+| Owner | 以每个运行时一个 `module::Symbol` 定义闭集 | 是，自 M0 | I1 到 I3 |
+| 生产者 | 把值写入字段：赋值、dict 或对象字面量、构造函数关键字、在已登记判定函数内 `return` 字面量、访问 owner 枚举成员 | `kernel` 词表必须，自 M0.5 | I12、I13 |
+| 解释者 | 据值分支：`if`、`match`、`switch`、成员测试 | 否；由分发扫描发现，`--report` 排序 | I2，不得比较未注册值 |
+| 透传者 | 序列化、持久化、转发或展示值而不据其分支 | 否 | 无；透传者永不成为 owner |
+
+由此得到两条规则。没有生产者的值是死值或兼容值：`skip` 在 `todos/user_gate.py`
+被比较却无处写入，M0 放过它，M0.5 让它失败，直到被删除或列入
+`compatibility_only`。生产比比较更严：M0.5 单独扫描生产形式，对未注册的被生产
+值失败（I13），M0 的字面量扫描继续捕获未注册的比较（I2）。解释者与透传者刻意
+不登记；否则每次消费者改动都要碰注册表，正是第 6 节对消费者计数所拒绝的搅动。
+它们与词表的关系是 `--report` 的建议性输出。
+
+生产形式在 M0.5 固定在 smoke 里，与分发形式同理：Python 的 `x["f"] = "v"`、
+envelope 或 packet 类型构造函数的关键字 `f="v"`、注册表列为生产者的函数内的
+`return "v"`、对 owner 枚举的成员访问；TypeScript 对象字面量里的 `f: "v"`、
+`x.f = "v"` 与条件表达式。`variable_sourced_values` 保留给生产者从扫描无法跟随
+的变量构造的值。哪些词表必须列生产者：`kernel` 自 M0.5；`cross_runtime` 只在
+M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持久化是生产扫描能回
+答的属性：若某个已列生产者符号是 journal 或 receipt 的写方，该词表标为
+`persisted`，这正是 Q2 与 Q10 等待的事实。
+
 ### 状态模型与 schema
 
 `loopx/semantics/vocabulary_v0.json`，`schema_version` 为
@@ -260,6 +307,9 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 | `vocabularies.<name>.tier`、`status` | `kernel`、`cross_runtime`、`cross_module`；`canonical`、`legacy`、`merge_candidate` | 封闭枚举 |
 | `vocabularies.<name>.literal_scan` | `field`、根目录、后缀 | 固定分发形式捕获的每个字面量都已注册；每个注册值被捕获或来自变量（I2） |
 | `vocabularies.<name>.variable_sourced_values` | 值到生产者模块 | 生产者仍包含带引号的该值 |
+| `vocabularies.<name>.scope`（M0.5） | `global` 或 `bounded_context`；`bounded_context` 条目列出 `contexts`，每个含一个 owner 符号 | 封闭枚举；已声明的有界上下文名字从 `multi_value_forks` 排除；未声明的多模块名字仍是分叉（I14） |
+| `vocabularies.<name>.producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个位点或一条变量来源条目（I12、I13） |
+| `vocabularies.<name>.compatibility_only`（M0.5） | 为让已持久化记录的读者仍能解析而保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
 | `relations.shared_field_names` | 一个字段名、其槽位及各槽位承载的词表或值 | 每个槽位可解析 |
@@ -356,7 +406,10 @@ PR 中重新生成清单。
 | 两处 owner 修正不改变行为 | `pytest tests/test_loopx_turn_transaction.py tests/test_loop_turn_loop_controller.py tests/test_turn_loop_disposition.py tests/test_loopx_turn_managed_step.py tests/control_plane -k authority` 与 `loopx canary premerge --from-git-diff` | 通过 | 在干净树上可复现的 `main` 既有环境失败除外 |
 | 文档治理接受这对 RFC | `python3 examples/docs-governance-smoke.py` | 通过 | 检查镜像、链接、索引 |
 | 退休预算按子串而非标识符计数 | 分别以 `in file.text` 与 `\bgoal_boundary\b` 统计 `goal_boundary` | 基线上 35 对 30 个 Python 模块 | 已知边界；M3 的零读者门需要标识符计数，见第 12 节 |
-| 模块局部约定过滤器是一次代码修改 | 扩宽 `inventory.py` 的 `MODULE_LOCAL_CONVENTION` 并重新生成 | `*_semantic` 预算下降而别处无代码改动 | 已知边界；正则在代码里，扩宽是可评审的 diff，未过滤总数仍在预算内 |
+| 模块局部约定过滤器是一次代码修改 | 扩宽 `inventory.py` 的 `MODULE_LOCAL_CONVENTION` 并重新生成 | `*_semantic` 预算下降而别处无代码改动 | 已知边界；正则在代码里，扩宽是可评审的 diff，未过滤总数仍在预算内 || 无人生产的注册值失败（M0.5） | 在基线上运行生产形式扫描 | 失败并点名 `effective_action` 与 `skip`；删除 `skip` 或列入 `compatibility_only` 后通过 | 第一个预期的 I12 失败；只被比较的值不算已携带 |
+| 生产未注册值失败（M0.5） | 在某个已列生产位点写 `effective_action: "brand_new"` | 即使无消费者比较它也失败，并点名位点与值 | I13；生产比比较更严 |
+| 有界上下文名字只能靠声明离开分叉预算（M0.5） | 为 `SOURCE_SURFACES` 声明四个上下文；另行只改名其中一处定义而不声明 | 声明把 `multi_value_forks` 降到 3；单独改名不降 | I14；诚实的修法是评审者看得见的注册表修改，改名是不碰注册表的代码改动 |
+
 | 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 |
 
 已知边界，写明是为了不让这个检查被过度信任：
@@ -417,7 +470,8 @@ planner 条目则有意保留 `python3`。
 | 里程碑 | 交付行为 | 进入门 | 退出证据 | 回滚 |
 | --- | --- | --- | --- | --- |
 | M0 | 含 26 个词表与 9 条关系的注册表、带 `--check` 的生成清单、带固定分发形式与覆盖下限的漂移 smoke、删除两处 owner 分叉、RFC 索引条目 | 本 RFC 开启 | 第 9 节各行全绿；20 类突变失败关闭 | 删除 smoke、`loopx/semantics/`、生成器及其测试 |
-| M1 | 单一 owner 模块中的 `EffectiveAction` 类型化枚举；replay observation 与 frontier 槽位拆出（Q6）；生产者与消费者 import 它；注册表 `literal_scan` 收紧到枚举 | M0 合入；owner 模块已定（Q3）；槽位拆分已决（Q6） | smoke 绿；owner 之外零裸 `effective_action` 字面量；status/should-run 的 parity fixture 不变 | 回退为字面量；注册表保留集合 |
+| M0.5 | 含 `global` 与 `bounded_context` 及每上下文 owner 的 `scope`；`kernel` 词表上的 `producers` 与 `compatibility_only`；带两条角色检查（I12、I13）的生产形式扫描；退休预算改按标识符计数并在一个 diff 里调低全部六个锚点（Q11）；Q9 的合并序规则写入第 10 节 | M0 合入；Q9 已决或其临时规则被接受 | smoke 在 I11 到 I14 强制下全绿；`skip` 已处理；`multi_value_forks` 靠声明降到 3；第 9 节角色行全绿；为 Q2 回答 `turn_route` 是否持久化 | 删除三个字段与角色检查；预算回到 M0 锚点 |
+| M1 | 单一 owner 模块中的 `EffectiveAction` 类型化枚举；replay observation 与 frontier 槽位拆出（Q6）；生产者与消费者 import 它；注册表 `literal_scan` 收紧到枚举 | M0.5 合入；owner 模块已定（Q3）；槽位拆分已决（Q6） | smoke 绿；owner 之外零裸 `effective_action` 字面量；status/should-run 的 parity fixture 不变 | 回退为字面量；注册表保留集合 |
 | M2 | route 到 disposition 的投影、`decide_loop_disposition` 决策表与跨运行时集合通过共享契约发布，生成 Python 与 TypeScript 绑定，效仿协调契约生成器 | M1 合入；Q2 与 Q7 已决 | 生成器 `--check` 与 smoke 绿；`settlement.ts` 与 `transaction.py` 读取生成集合 | 从上一版契约重新生成 |
 | M3 | 逐字段退休旧 should-run 字段，每个 PR 一个字段，预算降到零并删除字段 | 经生产者/读者调研证明该字段外部读者为零 | 按 `AGENTS.md` 的 schema 缩减记录；附录 B 条目 | 从最后一个写方恢复字段 |
 | M4 | 随迁移 RFC 的每次 replacement-first 切换调低孪生预算 | 每个切换 PR | 同 diff 中的预算修改 | 无需；预算跟随代码 |
@@ -450,7 +504,8 @@ planner 条目则有意保留 `python3`。
    `terminal`、`contract_error` 只在一侧存在。`same_concept` 关系记录了四个共享
    裁决。建议：两者都保留，M2 发布投影，待 managed-step 消费者成熟后再议。
    M2 前需定。保留两者的理由是合并会触及已持久化的 Turn 记录；这个前提尚未
-   核实。决定之前应先用生产者检查确认 `turn_route` 是否曾写入 journal 或
+   核实。决定之前应先用 M0.5 的生产形式扫描（I12，第 5 节）确认 `turn_route`
+   是否曾写入 journal 或
    receipt，还是只在进程内流转；若是后者，合并的代价远低于本 RFC 的假设，
    适用 Q10。
 3. **`EffectiveAction` 的 owner 模块。** 注册表今天不声明 owner，因为不存在任何
@@ -483,7 +538,7 @@ planner 条目则有意保留 `python3`。
    一次则改 (a)。Owner：仓库维护者。这是运维决策不是代码改动；应放在跟踪
    issue 的决策清单里，而不是任务清单里。
 10. **Turn 词表的终态。** 第 11 节的目标表默认保留三套与七个冗余拼法，因为
-   Q2 建议保留两者。若 Q2 的生产者检查表明 `turn_route` 未被持久化，维护者
+   Q2 建议保留两者。若 Q2 的 M0.5 生产形式扫描表明 `turn_route` 未被持久化，维护者
    应在 (a) 三套加生成投影（现行计划）与 (b) 两阶段合并（先双写、后退休）到
    每个概念一种拼法之间选择。没有这个决定，RFC 对其标题问题只有预算、没有
    完成定义。Owner：Turn driver owner。M2 关闭前需定。
@@ -597,6 +652,19 @@ planner 条目则有意保留 `python3`。
 - **对规范设计的影响：** 第 3 节范围收窄以匹配代码；第 11 节有了完成定义；第
   12 节增三条决策。
 
+### 2026-09-15 — 角色与作用域模型写入契约
+
+- **触发：** RFC 使用"生产者"与"消费者"十九次却从未定义，Q2 与 Q10 依赖一个
+  文中从未说明的"生产者检查"，`scope` 只存在于一段预告，且第 1 节在第 10 节
+  把 pytest 扫描定为义务之后仍写 smoke "在每次 premerge 与 full-public 运行"。
+- **交付：** 第 5 节新增"词表的角色"（owner、生产者、解释者、透传者）与三行
+  schema（`scope`、`producers`、`compatibility_only`）；第 2 节新增 I11 到 I14，
+  每条标注自 M0.5 起强制；第 9 节新增三行 M0.5 验证；第 11 节新增 M0.5 里程碑，
+  M1 改为以它为门；Q2 与 Q10 指向 I12 而非未定义的检查；第 1 节与第 10 节一致。
+  代码、注册表值与预算未变；M0 的 smoke 尚未强制 I11 到 I14。
+- **对规范设计的影响：** 新增四条带明确强制里程碑的不变量；计划有了"被生产"
+  的定义，M3 的零读者门与 Q2 的持久化问题都能使用它。
+
 ## 附录 B：决策日志
 
 | 日期 | 决策 | Owner / 批准 | 备选 | 变更的规范章节 |
@@ -662,3 +730,7 @@ planner 条目则有意保留 `python3`。
   扫描器没有实现的范围声明是一条假不变量。
 - 只降不升的预算描述的是方向。在第二个里程碑之前写出目标表，否则没人能说
   工作何时完成。
+- 等待一个 RFC 从未定义的"检查"的决策，是披着审慎外衣的悬空引用。点名交付
+  该检查的不变量与里程碑，否则决策没有输入，永远关不掉。
+- 用了十九次角色词（生产者、消费者）不等于定义了它。在角色成为一张每行带检查
+  的表之前，"谁写入这个值"是每个评审者答案都不同的问题。

From 7fe9ff475d81dbe08b322714fe286a1713b454d3 Mon Sep 17 00:00:00 2001
From: song <liusongstep@gmail.com>
Date: Tue, 15 Sep 2026 20:34:38 +0800
Subject: [PATCH 3/5] docs(semantics): add formal proof boundary to vocabulary
 contract

Signed-off-by: song <liusongstep@gmail.com>
---
 .../semantic-vocabulary-convergence-v0.md     | 46 +++++++++++
 ...emantic-vocabulary-convergence-v0.zh-CN.md | 34 ++++++++
 examples/semantic-vocabulary-drift-smoke.py   | 46 +++++++++++
 loopx/semantics/vocabulary_v0.json            | 82 +++++++++++++++++++
 4 files changed, 208 insertions(+)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 26d2ebb7e3..11b55a2bdf 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -357,6 +357,50 @@ when a value is added or removed after M0.5; `cross_module` only if promoted
 whose listed symbol is a journal or receipt writer marks the vocabulary
 `persisted`, which is the fact Q2 and Q10 wait on.
 
+### Formal model and proof boundary
+
+The registry is a finite specification of a larger program semantics. Let
+`V` be the set of registered vocabularies, `Val(v)` the admitted values of a
+vocabulary `v`, and `S` the set of source sites. The model records relations,
+not just names:
+
+```text
+D ⊆ S × V                         defines
+P ⊆ S × V × Val(v)                produces
+C ⊆ S × V × Val(v)                consumes or branches on
+I ⊆ S × V × V                     interprets one vocabulary as another
+T ⊆ S × V                         passes through without changing meaning
+G ⊆ V × V × (Val ⇀ Val ∪ {reject}) projects
+R ⊆ S × V × Version               persists a value durably
+```
+
+The minimum semantic obligations are:
+
+1. **Producer closedness:** `Produced(v) ⊆ Val(v)`. A recognised producer
+   cannot write a value outside the registered set.
+2. **Canonical liveness:** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`.
+   A value that is only compared is dead or compatibility-only, never
+   canonical.
+3. **Consumer domain closedness:** `Accepted(c) ⊆ Val(v)`, unless the consumer
+   explicitly declares an external or partial domain.
+4. **Scope separation:** a name collision is a semantic conflict only when the
+   declared scopes overlap. Spelling alone cannot establish equivalence.
+5. **Projection totality:** for every source value, a projection maps to a
+   target value or explicit `reject`.
+6. **Persistence compatibility:** a persisted vocabulary change preserves all
+   readers or declares a versioned migration.
+
+These are different proof obligations. M0 establishes owner-set equality,
+cross-runtime parity, the declared executable projection, and inventory
+freshness. Fixed literal forms and closed-set carriers provide bounded evidence,
+not whole-program proof. M0.5 adds bounded producer and scope checks. Producer
+discovery over dynamic code, behavioural equivalence of `same_concept`, and
+persisted-reader compatibility remain unproved until their source-to-sink
+edges are modelled. The registry stores this proof boundary in
+`formal_model`; an `unproved` property is an explicit limitation, never an
+implicit pass.
+
+
 ### State model and schema
 
 `loopx/semantics/vocabulary_v0.json`, `schema_version`
@@ -373,6 +417,7 @@ vocabulary key fails the smoke.
 | `vocabularies.<name>.scope` (M0.5) | `global` or `bounded_context`; a `bounded_context` entry lists `contexts`, each with one owner symbol | Closed enumeration; declared bounded-context names are excluded from `multi_value_forks`; an undeclared multi-module name stays a fork (I14) |
 | `vocabularies.<name>.producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one site or a variable-sourced entry (I12, I13) |
 | `vocabularies.<name>.compatibility_only` (M0.5) | values kept so readers of persisted records still resolve them | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone |
+| `formal_model` | finite universes, role relations, semantic obligations, and established/bounded/unproved claims | Exact schema and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs |
 | `vocabularies.<name>.value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values |
 | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves |
 | `relations.shared_field_names` | one field name, its slots and the vocabulary or values each carries | Every slot resolves |
@@ -491,6 +536,7 @@ inventory in the same PR.
 | A producer of an unregistered value fails (M0.5) | Write `effective_action: "brand_new"` in a listed producer site | Fails naming the site and the value even though no consumer compares it | I13; production is stricter than comparison |
 | A bounded-context name leaves the fork budget only by declaration (M0.5) | Declare `SOURCE_SURFACES` with its four contexts; separately, rename one definition without declaring | The declaration lowers `multi_value_forks` to 3; the rename alone does not | I14; the honest fix is a registry edit a reviewer sees, the rename is code without registry change |
 | An upstream merge can stale the committed inventory | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Measured cost of committing a snapshot; the handling rule is Section 10 and Section 12 Q9 |
+| The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, or proof-boundary category from `formal_model` | The drift smoke fails on the exact formal-model shape | The model is a finite contract and proof ledger; it does not prove the listed properties by itself |
 
 Known limits, stated so the check is not over-trusted:
 
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 1e0e71e239..049e901d58 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -294,6 +294,38 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持
 答的属性：若某个已列生产者符号是 journal 或 receipt 的写方，该词表标为
 `persisted`，这正是 Q2 与 Q10 等待的事实。
 
+### 形式模型与证明边界
+
+注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`Val(v)` 为词表
+`v` 允许的值集合，`S` 为源码位点集合。模型记录的是关系，而不只是名称：
+
+```text
+D ⊆ S × V                         定义词表
+P ⊆ S × V × Val(v)                生产值
+C ⊆ S × V × Val(v)                消费或据值分支
+I ⊆ S × V × V                     将一个词表解释为另一个词表
+T ⊆ S × V                         不改变含义地透传
+G ⊆ V × V × (Val ⇀ Val ∪ {reject}) 做投影
+R ⊆ S × V × Version               将值持久化
+```
+
+最低语义义务如下：
+
+1. **生产闭包：** `Produced(v) ⊆ Val(v)`。被识别的生产者不能写入注册集合之外的值。
+2. **规范值存活：** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`。只被比较、
+   没有生产来源的值是死值或兼容值，不能是 canonical。
+3. **消费者定义域闭包：** `Accepted(c) ⊆ Val(v)`，除非消费者显式声明外部定义域或部分定义域。
+4. **作用域分离：** 只有声明作用域相交时，同名冲突才是语义冲突。拼写本身不能证明等价。
+5. **投影全性：** 每个源值都必须映射到目标值，或显式映射为 `reject`。
+6. **持久化兼容性：** 持久化词表改变时，必须保持所有读者可读，或声明带版本的迁移。
+
+这些是不同的证明义务。M0 已建立 owner 集合相等、跨运行时 parity、声明的可执行投影
+和 inventory 新鲜度。固定字面量形式与闭集载体只提供有界证据，不是全程序证明。M0.5
+增加有界的生产者和作用域检查。动态代码中的完整生产者发现、`same_concept` 的行为等价、
+以及持久化读者兼容性，在建模源码到结果的边之前仍然是未证明状态。注册表通过
+`formal_model` 保存这条证明边界；标记为 `unproved` 的性质是显式局限，不能被当作默认通过。
+
+
 ### 状态模型与 schema
 
 `loopx/semantics/vocabulary_v0.json`，`schema_version` 为
@@ -310,6 +342,7 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持
 | `vocabularies.<name>.scope`（M0.5） | `global` 或 `bounded_context`；`bounded_context` 条目列出 `contexts`，每个含一个 owner 符号 | 封闭枚举；已声明的有界上下文名字从 `multi_value_forks` 排除；未声明的多模块名字仍是分叉（I14） |
 | `vocabularies.<name>.producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个位点或一条变量来源条目（I12、I13） |
 | `vocabularies.<name>.compatibility_only`（M0.5） | 为让已持久化记录的读者仍能解析而保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 |
+| `formal_model` | 有限的集合、角色关系、语义义务，以及已建立/有界/未证明的声明 | 漂移 smoke 校验精确 schema 和不变量 ID；属性实施阶段不能冒充已完成证明 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
 | `relations.shared_field_names` | 一个字段名、其槽位及各槽位承载的词表或值 | 每个槽位可解析 |
@@ -411,6 +444,7 @@ PR 中重新生成清单。
 | 有界上下文名字只能靠声明离开分叉预算（M0.5） | 为 `SOURCE_SURFACES` 声明四个上下文；另行只改名其中一处定义而不声明 | 声明把 `multi_value_forks` 降到 3；单独改名不降 | I14；诚实的修法是评审者看得见的注册表修改，改名是不碰注册表的代码改动 |
 
 | 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 |
+| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 |
 
 已知边界，写明是为了不让这个检查被过度信任：
 
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index b5d3367778..b94a70c9f7 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -43,11 +43,26 @@
 REGISTRY_KEYS = {
     "schema_version", "rfc", "inventory", "policy", "coverage_floor", "vocabularies", "relations",
     "projections", "schema_versions", "retirement_ledger", "dual_runtime_twins", "inventory_ratchets",
+    "formal_model",
 }
 VOCABULARY_KEYS = {"meaning", "tier", "status", "owners", "values"}
 VOCABULARY_OPTIONAL_KEYS = {"literal_scan", "variable_sourced_values", "value_notes", "deprecated_values"}
 TIERS = {"kernel", "cross_runtime", "cross_module"}
 STATUSES = {"canonical", "legacy", "merge_candidate"}
+FORMAL_MODEL_KEYS = {"schema_version", "universes", "roles", "relations", "invariants", "proof_boundary"}
+FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0"
+FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"}
+FORMAL_ROLES = {"owner", "producer", "interpreter", "pass_through"}
+FORMAL_RELATIONS = {"defines", "produces", "consumes", "interprets", "passes_through", "projects", "persists"}
+FORMAL_INVARIANTS = {
+    "F1_producer_closedness",
+    "F2_canonical_value_liveness",
+    "F3_consumer_domain_closedness",
+    "F4_scope_separation",
+    "F5_projection_totality",
+    "F6_persistence_version_compatibility",
+}
+FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"}
 
 # Hard ceiling on the registry's own floors and budgets, kept in code rather than
 # in the registry so one single-diff edit to ``vocabulary_v0.json`` cannot relax
@@ -137,6 +152,7 @@ def load_registry() -> dict[str, Any]:
     registry = json.loads(REGISTRY_PATH.read_text(encoding="utf-8"))
     require(set(registry) == REGISTRY_KEYS, f"registry keys must be exactly {sorted(REGISTRY_KEYS)}")
     require(registry["schema_version"] == REGISTRY_SCHEMA_VERSION, f"registry schema_version must be {REGISTRY_SCHEMA_VERSION}")
+    check_formal_model(registry["formal_model"])
     require((REPO_ROOT / registry["rfc"]).is_file(), f"registry must point at an existing RFC: {registry['rfc']}")
     require((REPO_ROOT / registry["inventory"]).is_file(), f"registry must point at an existing inventory: {registry['inventory']}")
     for name, vocabulary in registry["vocabularies"].items():
@@ -170,6 +186,36 @@ def load_registry() -> dict[str, Any]:
     return registry
 
 
+def check_formal_model(model: dict[str, Any]) -> None:
+    """Validate the formal vocabulary model's finite signature and proof ledger.
+
+    This is deliberately a schema check, not a claim that the current scanner
+    proves every property. Each property carries an enforcement stage and the
+    proof boundary records what remains unproved.
+    """
+    require(set(model) == FORMAL_MODEL_KEYS, f"formal_model keys must be exactly {sorted(FORMAL_MODEL_KEYS)}")
+    require(model["schema_version"] == FORMAL_MODEL_SCHEMA_VERSION, "formal_model schema_version drift")
+    require(set(model["universes"]) == FORMAL_UNIVERSE_KEYS, "formal_model universes must name the declared sets")
+    require(set(model["roles"]) == FORMAL_ROLES, "formal_model roles must be the four vocabulary roles")
+    require(set(model["relations"]) == FORMAL_RELATIONS, "formal_model relations must be the declared edge kinds")
+    invariants = model["invariants"]
+    require(isinstance(invariants, list) and {item.get("id") for item in invariants} == FORMAL_INVARIANTS,
+            "formal_model invariants must cover exactly F1-F6")
+    for item in invariants:
+        require(set(item) == {"id", "statement", "enforcement", "evidence"},
+                f"formal invariant {item.get('id')} has an invalid shape")
+        require(item["enforcement"] in FORMAL_ENFORCEMENT,
+                f"formal invariant {item['id']} has unknown enforcement stage")
+        require(item["statement"].strip() and item["evidence"].strip(),
+                f"formal invariant {item['id']} needs a statement and evidence boundary")
+    boundary = model["proof_boundary"]
+    require(set(boundary) == {"established", "bounded", "unproved"},
+            "formal_model proof_boundary must separate established, bounded, and unproved claims")
+    for key in boundary:
+        require(isinstance(boundary[key], list) and all(isinstance(value, str) and value.strip() for value in boundary[key]),
+                f"formal_model proof_boundary.{key} must contain non-empty claim names")
+
+
 def check_coverage_floor(registry: dict[str, Any]) -> str:
     for vocabulary in registry["vocabularies"].values():
         if scan := vocabulary.get("literal_scan"):
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index c5294ab70c..b40f174c8e 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -11,6 +11,88 @@
     "value_shape": "Registered values are lower snake_case tokens (^[a-z][a-z0-9_]*$). The literal scan captures any quoted string so a malformed or versioned spelling is reported, not skipped.",
     "literal_scan_forms": "The dispatch forms the scan recognises are fixed in the smoke, not in this file: comparison or assignment against a literal (== != === !== : = is), a JS/TS ternary, membership in an inline collection, and a Python conditional expression."
   },
+  "formal_model": {
+    "schema_version": "loopx_semantic_formal_model_v0",
+    "universes": {
+      "vocabularies": "V: registered vocabulary identifiers",
+      "values": "Val(v): values admitted by vocabulary v",
+      "sites": "S: source locations that define, produce, consume, interpret, pass through, project, or persist values",
+      "scopes": "Scope: global or bounded_context(context_id)",
+      "roles": "Roles assigned to sites; a site may have more than one role only when each edge is explicit"
+    },
+    "roles": [
+      "owner",
+      "producer",
+      "interpreter",
+      "pass_through"
+    ],
+    "relations": {
+      "defines": "D ⊆ S × V: a site defines a vocabulary carrier",
+      "produces": "P ⊆ S × V × Val: a site writes or returns a vocabulary value",
+      "consumes": "C ⊆ S × V × Val: a site accepts or branches on a value",
+      "interprets": "I ⊆ S × V × V: a site maps one vocabulary into another",
+      "passes_through": "T ⊆ S × V: a site serializes, persists, forwards, or displays without changing meaning",
+      "projects": "G ⊆ V × V × (Val ⇀ Val ∪ {reject}): a declared partial or total projection",
+      "persists": "R ⊆ S × V × Version: a site writes a value to a durable representation"
+    },
+    "invariants": [
+      {
+        "id": "F1_producer_closedness",
+        "statement": "Produced(v) ⊆ Val(v)",
+        "enforcement": "m0_5",
+        "evidence": "bounded production-form AST scan; unknown dynamic producers are reported, not treated as proven safe"
+      },
+      {
+        "id": "F2_canonical_value_liveness",
+        "statement": "Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)",
+        "enforcement": "m0_5",
+        "evidence": "every kernel value has a recognised producer or an explicit compatibility-only reason"
+      },
+      {
+        "id": "F3_consumer_domain_closedness",
+        "statement": "Accepted(c) ⊆ Val(v), unless the consumer declares an external or partial domain",
+        "enforcement": "advisory",
+        "evidence": "consumer and interpreter edges are currently inventory evidence, not complete data-flow proof"
+      },
+      {
+        "id": "F4_scope_separation",
+        "statement": "A name collision is a semantic conflict only when its declared scopes overlap",
+        "enforcement": "m0_5",
+        "evidence": "scope declarations and per-context owners; scope is never inferred from spelling"
+      },
+      {
+        "id": "F5_projection_totality",
+        "statement": "For every source value, a projection maps to a target value or explicit reject",
+        "enforcement": "m0",
+        "evidence": "registry mapping is compared with the executable owner function"
+      },
+      {
+        "id": "F6_persistence_version_compatibility",
+        "statement": "A persisted vocabulary change preserves readers or declares a versioned migration",
+        "enforcement": "unproved",
+        "evidence": "requires producer, serializer, storage, reader, and migration edges not yet modeled"
+      }
+    ],
+    "proof_boundary": {
+      "established": [
+        "owner_carrier_set_equality",
+        "cross_runtime_owner_parity",
+        "declared_projection_mapping",
+        "inventory_snapshot_freshness"
+      ],
+      "bounded": [
+        "fixed_literal_forms",
+        "fixed_closed_set_carriers",
+        "declared_budget_monotonicity"
+      ],
+      "unproved": [
+        "all_runtime_trace_values_are_registered",
+        "all_producers_are_found",
+        "same_concept_behavioral_equivalence",
+        "persistence_reader_compatibility"
+      ]
+    }
+  },
   "coverage_floor": {
     "vocabularies": 26,
     "owner_symbols": 46,

From b0c68058affc79addf802038ed3ca30e09a3fefb Mon Sep 17 00:00:00 2001
From: song <liusongstep@gmail.com>
Date: Tue, 15 Sep 2026 20:47:55 +0800
Subject: [PATCH 4/5] docs(semantics): add governed convergence roadmap

Signed-off-by: song <liusongstep@gmail.com>
---
 .../semantic-vocabulary-convergence-v0.md     | 55 +++++++++++++++++++
 ...emantic-vocabulary-convergence-v0.zh-CN.md | 43 +++++++++++++++
 examples/semantic-vocabulary-drift-smoke.py   | 22 +++++++-
 loopx/semantics/vocabulary_v0.json            |  6 ++
 4 files changed, 125 insertions(+), 1 deletion(-)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 11b55a2bdf..155039a3cd 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -418,6 +418,7 @@ vocabulary key fails the smoke.
 | `vocabularies.<name>.producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one site or a variable-sourced entry (I12, I13) |
 | `vocabularies.<name>.compatibility_only` (M0.5) | values kept so readers of persisted records still resolve them | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone |
 | `formal_model` | finite universes, role relations, semantic obligations, and established/bounded/unproved claims | Exact schema and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs |
+| `formal_model.enforcement_policy` | blocking-now, blocking-next, advisory, and unproved lanes | Every formal invariant appears exactly once and its lane agrees with its enforcement stage |
 | `vocabularies.<name>.value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values |
 | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves |
 | `relations.shared_field_names` | one field name, its slots and the vocabulary or values each carries | Every slot resolves |
@@ -634,6 +635,60 @@ vocabulary property the smoke can check. Rows marked *open* wait on a Section
 | Merge-candidate groups | 32 unreviewed | every group classified; only `same_semantics` groups merged | classification PR, then per-group PRs |
 | Control-plane py/ts twins | 43 | follows the TypeScript migration RFC; no target here | M4 |
 
+### Two-track execution and enforcement lanes
+
+The roadmap separates repairing existing semantic debt from improving the
+measuring apparatus. Track A can proceed without waiting for a design decision:
+remove real forks, conflicts, twins, and legacy readers one narrow PR at a time.
+Track B improves what the guard can know: scope declarations, bounded producer
+analysis, identifier counting, and merge-order handling. Track A reduces the
+measured debt; Track B makes that measurement more faithful. M1 and later depend
+on Track B where the current measurement is known to be incomplete.
+
+```text
+Track A: baseline debt repairs ───────────────────────────────┐
+                                                               ├─> M1 typed slots
+Track B: scope + producer model + metric boundaries ──────────┘       │
+                                                                      ├─> M2 generated projections
+                                                                      ├─> M3 legacy retirement
+                                                                      └─> M4 runtime twin migration
+```
+
+The formal model uses four enforcement lanes so a difficult property does not
+become an accidental merge blocker:
+
+| Lane | Properties | Current meaning |
+| --- | --- | --- |
+| `blocking_now` | F5 projection totality | Enforced by the M0 smoke today |
+| `blocking_next` | F1 producer closedness, F2 canonical liveness, F4 scope separation | Planned blocking checks after M0.5; not claimed by M0 |
+| `advisory` | F3 consumer domain closedness | Reported evidence; it does not block ordinary consumer edits |
+| `unproved` | F6 persistence/version compatibility | An explicit proof gap; it cannot be reported as passed |
+
+The exit condition for a phase is its evidence row, not the existence of a
+formula or a registry entry. A property moves from `unproved` to `advisory` only
+when a bounded source-to-sink analysis exists, and moves to a blocking lane only
+after its false-negative boundary is documented and mutation tests cover the
+recognised forms. This keeps the contract strict about silent corruption while
+allowing incomplete analyses to remain useful without blocking unrelated work.
+
+The phases are therefore:
+
+1. **M0:** keep the current structural guard and make its proof boundary
+   explicit.
+2. **M0.5:** implement `scope`, producer forms for the four Turn kernel
+   vocabularies, and identifier-based retirement counts.
+3. **M1:** split the overloaded `effective_action` slots and introduce one typed
+   owner after Q3 and Q6 are decided.
+4. **M2:** publish the full decision table and both projection hops through a
+   generated cross-runtime contract.
+5. **M3/M4:** retire legacy fields and reduce Python/TypeScript twins only when
+   their reader and migration evidence is complete.
+
+This roadmap is normative for dependencies and exit evidence. Issue #4447 may
+carry owners, suggested dates, and operational checklists, but it must not
+introduce a competing target state.
+
+
 ## 12. Open decisions
 
 1. **Registry location.** Owner: kernel maintainers. M0 implements
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 049e901d58..ad6886841d 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -343,6 +343,7 @@ R ⊆ S × V × Version               将值持久化
 | `vocabularies.<name>.producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个位点或一条变量来源条目（I12、I13） |
 | `vocabularies.<name>.compatibility_only`（M0.5） | 为让已持久化记录的读者仍能解析而保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 |
 | `formal_model` | 有限的集合、角色关系、语义义务，以及已建立/有界/未证明的声明 | 漂移 smoke 校验精确 schema 和不变量 ID；属性实施阶段不能冒充已完成证明 |
+| `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
 | `relations.shared_field_names` | 一个字段名、其槽位及各槽位承载的词表或值 | 每个槽位可解析 |
@@ -527,6 +528,48 @@ planner 条目则有意保留 `python3`。
 | 合并候选组 | 32 组未评审 | 每组已分类；只合并 `same_semantics` 的组 | 分类表 PR，随后逐组 PR |
 | 控制面 py/ts 孪生 | 43 | 跟随 TypeScript 迁移 RFC；本 RFC 不设目标 | M4 |
 
+### 两条执行轨道与强制层级
+
+路线图把修复已有语义债务与完善度量工具分开。轨道 A 不等待设计决策：每个窄 PR
+逐步删除真实分叉、冲突、孪生和旧读者。轨道 B 改善守卫能够知道的内容：作用域声明、
+有界生产者分析、标识符计数和合并序处理。轨道 A 降低债务数量，轨道 B 让这个度量更
+接近真实语义。M1 及之后的阶段依赖轨道 B，因为当前度量已知并不完备。
+
+```text
+轨道 A：修复现有债务 ──────────────────────────────────────┐
+                                                               ├─> M1 类型化槽位
+轨道 B：作用域 + 生产者模型 + 度量边界 ─────────────────────┘       │
+                                                                      ├─> M2 生成式投影
+                                                                      ├─> M3 旧字段退休
+                                                                      └─> M4 运行时孪生迁移
+```
+
+形式模型使用四个强制层级，避免困难性质意外变成合并阻断：
+
+| 层级 | 性质 | 当前含义 |
+| --- | --- | --- |
+| `blocking_now` | F5 投影全性 | 当前 M0 smoke 已强制 |
+| `blocking_next` | F1 生产闭包、F2 规范值存活、F4 作用域分离 | M0.5 后计划强制；M0 不宣称已经做到 |
+| `advisory` | F3 消费者定义域闭包 | 只报告证据，不阻断普通消费者改动 |
+| `unproved` | F6 持久化/版本兼容性 | 明确的证明缺口，不能报告为已通过 |
+
+阶段完成条件是验收表中的证据，而不是出现一个公式或注册表条目。有界的源码到结果
+分析存在之后，性质才可从 `unproved` 移到 `advisory`；只有记录误报/漏报边界并用突变
+测试覆盖已识别形式后，才可移到阻断层。这样既严格防止静默破坏，也允许不完整的分析
+为无关改动提供信息而不阻断它们。
+
+阶段顺序如下：
+
+1. **M0：** 保留当前结构守卫，并明确其证明边界。
+2. **M0.5：** 为四个 Turn 内核词表实现 `scope`、生产形式和按标识符计算的退休预算。
+3. **M1：** 在 Q3、Q6 决定后拆开过载的 `effective_action` 槽位，并引入一个类型化 owner。
+4. **M2：** 通过生成的跨运行时契约发布完整决策表和两跳投影。
+5. **M3/M4：** 只有在读者与迁移证据完整后，才退休旧字段并减少 Python/TypeScript 孪生。
+
+这份路线图对依赖和退出证据具有规范效力。Issue #4447 可以承载 owner、建议日期和
+运维清单，但不能另立一套目标状态。
+
+
 ## 12. 未决决策
 
 1. **注册表位置。** Owner：内核维护者。M0 实现于 `loopx/semantics/`，因为范围是
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index b94a70c9f7..f3a9578f28 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -49,7 +49,10 @@
 VOCABULARY_OPTIONAL_KEYS = {"literal_scan", "variable_sourced_values", "value_notes", "deprecated_values"}
 TIERS = {"kernel", "cross_runtime", "cross_module"}
 STATUSES = {"canonical", "legacy", "merge_candidate"}
-FORMAL_MODEL_KEYS = {"schema_version", "universes", "roles", "relations", "invariants", "proof_boundary"}
+FORMAL_MODEL_KEYS = {
+    "schema_version", "universes", "roles", "relations", "invariants", "proof_boundary",
+    "enforcement_policy",
+}
 FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0"
 FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"}
 FORMAL_ROLES = {"owner", "producer", "interpreter", "pass_through"}
@@ -63,6 +66,7 @@
     "F6_persistence_version_compatibility",
 }
 FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"}
+FORMAL_POLICY_KEYS = {"blocking_now", "blocking_next", "advisory", "unproved"}
 
 # Hard ceiling on the registry's own floors and budgets, kept in code rather than
 # in the registry so one single-diff edit to ``vocabulary_v0.json`` cannot relax
@@ -208,6 +212,22 @@ def check_formal_model(model: dict[str, Any]) -> None:
                 f"formal invariant {item['id']} has unknown enforcement stage")
         require(item["statement"].strip() and item["evidence"].strip(),
                 f"formal invariant {item['id']} needs a statement and evidence boundary")
+    policy = model["enforcement_policy"]
+    require(set(policy) == FORMAL_POLICY_KEYS,
+            "formal_model enforcement_policy must separate current, next, advisory, and unproved checks")
+    policy_ids = [item_id for ids in policy.values() for item_id in ids]
+    require(set(policy_ids) == FORMAL_INVARIANTS and len(policy_ids) == len(set(policy_ids)),
+            "formal_model enforcement_policy must partition all invariants exactly once")
+    stage_for_policy = {
+        "blocking_now": "m0",
+        "blocking_next": "m0_5",
+        "advisory": "advisory",
+        "unproved": "unproved",
+    }
+    stages = {item["id"]: item["enforcement"] for item in invariants}
+    for policy_name, ids in policy.items():
+        require(all(stages[item_id] == stage_for_policy[policy_name] for item_id in ids),
+                f"formal_model policy lane {policy_name} disagrees with invariant enforcement stage")
     boundary = model["proof_boundary"]
     require(set(boundary) == {"established", "bounded", "unproved"},
             "formal_model proof_boundary must separate established, bounded, and unproved claims")
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index b40f174c8e..b652844e1d 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -26,6 +26,12 @@
       "interpreter",
       "pass_through"
     ],
+    "enforcement_policy": {
+      "blocking_now": ["F5_projection_totality"],
+      "blocking_next": ["F1_producer_closedness", "F2_canonical_value_liveness", "F4_scope_separation"],
+      "advisory": ["F3_consumer_domain_closedness"],
+      "unproved": ["F6_persistence_version_compatibility"]
+    },
     "relations": {
       "defines": "D ⊆ S × V: a site defines a vocabulary carrier",
       "produces": "P ⊆ S × V × Val: a site writes or returns a vocabulary value",

From 554248b2834ee052ba00b488c1b1d5da0c636f1d Mon Sep 17 00:00:00 2001
From: song <liusongstep@gmail.com>
Date: Tue, 15 Sep 2026 21:05:14 +0800
Subject: [PATCH 5/5] docs(semantics): model consumers as vocabulary subroles

Signed-off-by: song <liusongstep@gmail.com>
---
 .../rfcs/semantic-vocabulary-convergence-v0.md      | 13 ++++++++-----
 .../semantic-vocabulary-convergence-v0.zh-CN.md     | 12 +++++++-----
 examples/semantic-vocabulary-drift-smoke.py         |  8 +++++---
 loopx/semantics/vocabulary_v0.json                  |  4 ++++
 4 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 155039a3cd..51564280a3 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -325,15 +325,18 @@ misclassification, recorded in the registry's `inventory_ratchets` note.
 ### Roles of a vocabulary
 
 A module that mentions a value is not its owner, and a vocabulary has more
-than one kind of participant. The registry distinguishes four roles because
-the check that makes sense differs by role:
+than one kind of participant. Consumer is the umbrella role for code that reads
+or accepts a value; interpreter and pass-through are its two tracked subroles.
+The registry distinguishes these roles because the check that makes sense differs
+by role:
 
 | Role | What it does | Registered | Check |
 | --- | --- | --- | --- |
 | Owner | Defines the closed set as one `module::Symbol` per runtime | Yes, since M0 | I1 to I3 |
 | Producer | Writes a value into the field: assignment, dict or object literal, constructor keyword, `return` of a literal inside a listed deciding function, enum member on the owner | Yes for `kernel` vocabularies, from M0.5 | I12, I13 |
-| Interpreter | Branches on the value: `if`, `match`, `switch`, membership test | No; found by the dispatch scan, ranked by `--report` | I2, no unregistered comparison |
-| Pass-through | Serializes, persists, forwards, or displays the value without branching on it | No | None; a pass-through never becomes an owner |
+| Consumer | Reads or accepts a vocabulary value; this is the umbrella role for interpreters and pass-throughs | Usually no; relation is reported rather than curated | F3 |
+| Interpreter | Consumer that branches on or maps the value: `if`, `match`, `switch`, membership test | No; found by the dispatch scan, ranked by `--report` | I2, F3 |
+| Pass-through | Consumer that serializes, persists, forwards, or displays the value without changing its meaning | No | F3; persistence also needs F6 evidence |
 
 Two rules follow. A value with no producer is dead or compatibility-only:
 `skip` is compared in `todos/user_gate.py` and written nowhere, so M0 passes
@@ -417,7 +420,7 @@ vocabulary key fails the smoke.
 | `vocabularies.<name>.scope` (M0.5) | `global` or `bounded_context`; a `bounded_context` entry lists `contexts`, each with one owner symbol | Closed enumeration; declared bounded-context names are excluded from `multi_value_forks`; an undeclared multi-module name stays a fork (I14) |
 | `vocabularies.<name>.producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one site or a variable-sourced entry (I12, I13) |
 | `vocabularies.<name>.compatibility_only` (M0.5) | values kept so readers of persisted records still resolve them | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone |
-| `formal_model` | finite universes, role relations, semantic obligations, and established/bounded/unproved claims | Exact schema and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs |
+| `formal_model` | finite universes, role relations and hierarchy, semantic obligations, and established/bounded/unproved claims | Exact schema, role hierarchy, and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs |
 | `formal_model.enforcement_policy` | blocking-now, blocking-next, advisory, and unproved lanes | Every formal invariant appears exactly once and its lane agrees with its enforcement stage |
 | `vocabularies.<name>.value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values |
 | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves |
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 ad6886841d..cba3879ca0 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -268,15 +268,17 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 
 ### 词表的角色
 
-提及一个值的模块不是它的 owner，一个词表也不止一种参与者。注册表区分四种角
-色，因为对每种角色有意义的检查不同：
+提及一个值的模块不是它的 owner，一个词表也不止一种参与者。消费者是读取或接受
+值的上位角色，解释者和透传者是它的两个受跟踪子角色。注册表区分这些角色，因为
+对每种角色有意义的检查不同：
 
 | 角色 | 做什么 | 是否登记 | 检查 |
 | --- | --- | --- | --- |
 | Owner | 以每个运行时一个 `module::Symbol` 定义闭集 | 是，自 M0 | I1 到 I3 |
 | 生产者 | 把值写入字段：赋值、dict 或对象字面量、构造函数关键字、在已登记判定函数内 `return` 字面量、访问 owner 枚举成员 | `kernel` 词表必须，自 M0.5 | I12、I13 |
-| 解释者 | 据值分支：`if`、`match`、`switch`、成员测试 | 否；由分发扫描发现，`--report` 排序 | I2，不得比较未注册值 |
-| 透传者 | 序列化、持久化、转发或展示值而不据其分支 | 否 | 无；透传者永不成为 owner |
+| 消费者 | 读取或接受词表值；解释者和透传者都属于这个上位角色 | 通常不登记；只报告关系，不做策展 | F3 |
+| 解释者 | 消费者的一种，据值分支或映射：`if`、`match`、`switch`、成员测试 | 否；由分发扫描发现，`--report` 排序 | I2、F3 |
+| 透传者 | 消费者的一种，序列化、持久化、转发或展示值而不改变其含义 | 否 | F3；涉及持久化时还需 F6 证据 |
 
 由此得到两条规则。没有生产者的值是死值或兼容值：`skip` 在 `todos/user_gate.py`
 被比较却无处写入，M0 放过它，M0.5 让它失败，直到被删除或列入
@@ -342,7 +344,7 @@ R ⊆ S × V × Version               将值持久化
 | `vocabularies.<name>.scope`（M0.5） | `global` 或 `bounded_context`；`bounded_context` 条目列出 `contexts`，每个含一个 owner 符号 | 封闭枚举；已声明的有界上下文名字从 `multi_value_forks` 排除；未声明的多模块名字仍是分叉（I14） |
 | `vocabularies.<name>.producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个位点或一条变量来源条目（I12、I13） |
 | `vocabularies.<name>.compatibility_only`（M0.5） | 为让已持久化记录的读者仍能解析而保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 |
-| `formal_model` | 有限的集合、角色关系、语义义务，以及已建立/有界/未证明的声明 | 漂移 smoke 校验精确 schema 和不变量 ID；属性实施阶段不能冒充已完成证明 |
+| `formal_model` | 有限的集合、角色关系与层次、语义义务，以及已建立/有界/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次和不变量 ID；属性实施阶段不能冒充已完成证明 |
 | `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index f3a9578f28..d01dc46069 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -50,12 +50,12 @@
 TIERS = {"kernel", "cross_runtime", "cross_module"}
 STATUSES = {"canonical", "legacy", "merge_candidate"}
 FORMAL_MODEL_KEYS = {
-    "schema_version", "universes", "roles", "relations", "invariants", "proof_boundary",
+    "schema_version", "universes", "roles", "role_hierarchy", "relations", "invariants", "proof_boundary",
     "enforcement_policy",
 }
 FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0"
 FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"}
-FORMAL_ROLES = {"owner", "producer", "interpreter", "pass_through"}
+FORMAL_ROLES = {"owner", "producer", "consumer", "interpreter", "pass_through"}
 FORMAL_RELATIONS = {"defines", "produces", "consumes", "interprets", "passes_through", "projects", "persists"}
 FORMAL_INVARIANTS = {
     "F1_producer_closedness",
@@ -200,7 +200,9 @@ def check_formal_model(model: dict[str, Any]) -> None:
     require(set(model) == FORMAL_MODEL_KEYS, f"formal_model keys must be exactly {sorted(FORMAL_MODEL_KEYS)}")
     require(model["schema_version"] == FORMAL_MODEL_SCHEMA_VERSION, "formal_model schema_version drift")
     require(set(model["universes"]) == FORMAL_UNIVERSE_KEYS, "formal_model universes must name the declared sets")
-    require(set(model["roles"]) == FORMAL_ROLES, "formal_model roles must be the four vocabulary roles")
+    require(set(model["roles"]) == FORMAL_ROLES, "formal_model roles must include the consumer role and its subroles")
+    require(model["role_hierarchy"] == {"consumer": ["interpreter", "pass_through"]},
+            "formal_model role_hierarchy must classify interpreter and pass_through as consumers")
     require(set(model["relations"]) == FORMAL_RELATIONS, "formal_model relations must be the declared edge kinds")
     invariants = model["invariants"]
     require(isinstance(invariants, list) and {item.get("id") for item in invariants} == FORMAL_INVARIANTS,
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index b652844e1d..17558ccd1d 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -23,9 +23,13 @@
     "roles": [
       "owner",
       "producer",
+      "consumer",
       "interpreter",
       "pass_through"
     ],
+    "role_hierarchy": {
+      "consumer": ["interpreter", "pass_through"]
+    },
     "enforcement_policy": {
       "blocking_now": ["F5_projection_totality"],
       "blocking_next": ["F1_producer_closedness", "F2_canonical_value_liveness", "F4_scope_separation"],