docs(semantics): define relative completeness boundary

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

@@ -363,28 +363,29 @@ whose listed symbol is a journal or receipt writer marks the vocabulary
 ### 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:
+`V` be the set of registered vocabularies, `L` the source sites, `U(v)` the
+ambient runtime values, and `S(v)` the registered admitted values of vocabulary
+`v`. Production and consumption range over `U(v)` before validation. 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
+D ⊆ L × V                         defines
+P ⊆ L × V × U(v)                  produces
+C ⊆ L × V × U(v)                  consumes or branches on
+I ⊆ L × V × V                     interprets one vocabulary as another
+T ⊆ L × V                         passes through without changing meaning
+G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) projects
+R ⊆ L × V × Version               persists a value durably
 ```
 
 The minimum semantic obligations are:
 
-1. **Producer closedness:** `Produced(v) ⊆ Val(v)`. A recognised producer
+1. **Producer closedness:** `Produced(v) ⊆ S(v) ⊆ U(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
+3. **Consumer domain closedness:** `Accepted(c) ⊆ S(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.
@@ -404,6 +405,61 @@ edges are modelled. The registry stores this proof boundary in
 implicit pass.
 
 
+### Soundness, relative completeness, and candidate decisions
+
+The word *complete* is scoped here. Let `U(v)` be the ambient runtime value
+space for a vocabulary, `S(v)` its registered admitted set, `P(v)` the values
+actually produced, and `O(v)` the values observed by the scanner. The producer
+obligation is meaningful only when production is defined over `U(v)`:
+
+```text
+P(v) ⊆ S(v) ⊆ U(v)
+```
+
+Defining `P(v)` as a subset of `S(v)` in advance would make the first
+inclusion tautological. M0 currently establishes only bounded claims about
+`O(v)` and registered structural carriers.
+
+For a recognised language fragment `L0` and an exact analyser `A0`, define:
+
+```text
+Sound(A0, property, L0)    := A0 accepts c ⇒ property(c)
+Complete(A0, property, L0) := property(c) ⇒ A0 accepts c
+```
+
+The M0 guard can aim at both properties for its fixed carrier and dispatch
+forms. It cannot claim either property for arbitrary dynamic Python or
+TypeScript. A value flowing through an alias, configuration, reflection,
+external input, or unrecognised syntax belongs to `unknown` until a bounded
+analysis accounts for it. Unknown is an evidence result, not proof of absence.
+
+Advisory candidate triage uses one finite disposition:
+
+```text
+reuse_existing | extend_vocabulary | create_vocabulary | local_only
+external_input | compatibility_only | unknown
+```
+
+This makes the *workflow classification* exhaustive even though the program
+analysis is not. The registry stores the allowed labels and default, not
+per-candidate decisions; this metadata does not enforce candidate handling in
+product code. The drift smoke validates the label contract only.
+`reuse_existing` requires the same slot, compatible scope, and an equivalent
+contract. `extend_vocabulary` requires a witness that
+reusing an existing value would collapse two states with different required
+behaviour. `create_vocabulary` requires a new semantic domain or independently
+owned lifecycle. If the evidence cannot decide among these cases, the default
+is `unknown`; the agent must not silently treat an unresolved candidate as a
+reuse.
+
+General behavioural equivalence remains undecidable for arbitrary programs, so
+`same_concept` is not promoted to a theorem by this schema. It becomes a
+blocking property only for a restricted contract with explicit inputs,
+outputs, transitions, persistence version and finite test domain. This is the
+boundary between a useful proof skeleton and an uncheckable claim of
+whole-program semantic convergence.
+
+
 ### State model and schema
 
 `loopx/semantics/vocabulary_v0.json`, `schema_version`
@@ -420,7 +476,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 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` | finite universes, role relations and hierarchy, semantic obligations, candidate decisions, and established/bounded/unknown/unproved claims | Exact schema, role hierarchy, candidate decisions, 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 |
@@ -540,7 +596,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 |
+| The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, candidate decision, 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:
 
@@ -768,6 +824,15 @@ introduce a competing target state.
 
 ## Appendix A: Execution ledger (non-normative)
 
+### 2026-09-16 — Review consistency repair
+
+- Keep one candidate-decision section per language.
+- Use `L` for source sites, `U(v)` for ambient values and `S(v)` for admitted
+  values throughout the registry and narrative. Production is not admitted by definition.
+- Clarify candidate dispositions as advisory metadata; no per-candidate runtime
+  store or enforcement is delivered by this schema.
+
+
 ### 2026-09-15 — M0 opened with the RFC
 
 - **Baseline:** `1dc6ad8d8`

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

@@ -298,25 +298,26 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持
 
 ### 形式模型与证明边界
 
-注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`Val(v)` 为词表
-`v` 允许的值集合，`S` 为源码位点集合。模型记录的是关系，而不只是名称：
+注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`L` 为源码位点集合，
+`U(v)` 为词表 `v` 的环境运行时值空间，`S(v)` 为注册允许集合。生产与消费先在
+`U(v)` 上定义，再验证是否属于允许集合。模型记录的是关系，而不只是名称：
 
 ```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               将值持久化
+D ⊆ L × V                         定义词表
+P ⊆ L × V × U(v)                  生产值
+C ⊆ L × V × U(v)                  消费或据值分支
+I ⊆ L × V × V                     将一个词表解释为另一个词表
+T ⊆ L × V                         不改变含义地透传
+G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) 做投影
+R ⊆ L × V × Version               将值持久化
 ```
 
 最低语义义务如下：
 
-1. **生产闭包：** `Produced(v) ⊆ Val(v)`。被识别的生产者不能写入注册集合之外的值。
+1. **生产闭包：** `Produced(v) ⊆ S(v) ⊆ U(v)`。被识别的生产者不能写入注册集合之外的值。
 2. **规范值存活：** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`。只被比较、
    没有生产来源的值是死值或兼容值，不能是 canonical。
-3. **消费者定义域闭包：** `Accepted(c) ⊆ Val(v)`，除非消费者显式声明外部定义域或部分定义域。
+3. **消费者定义域闭包：** `Accepted(c) ⊆ S(v)`，除非消费者显式声明外部定义域或部分定义域。
 4. **作用域分离：** 只有声明作用域相交时，同名冲突才是语义冲突。拼写本身不能证明等价。
 5. **投影全性：** 每个源值都必须映射到目标值，或显式映射为 `reject`。
 6. **持久化兼容性：** 持久化词表改变时，必须保持所有读者可读，或声明带版本的迁移。
@@ -328,6 +329,51 @@ R ⊆ S × V × Version               将值持久化
 `formal_model` 保存这条证明边界；标记为 `unproved` 的性质是显式局限，不能被当作默认通过。
 
 
+### 健全性、相对完备性与候选决策
+
+这里的“完备”必须带范围。令 `U(v)` 为词表的运行时完整值域，`S(v)` 为注册表允许
+的值集合，`P(v)` 为实际产生的值集合，`O(v)` 为扫描器观察到的值集合。生产义务
+只有在完整值域上定义时才有意义：
+
+```text
+P(v) ⊆ S(v) ⊆ U(v)
+```
+
+如果预先把 `P(v)` 定义成 `S(v)` 的子集，第一个包含关系就变成恒真命题。M0 当前
+只对 `O(v)` 和已登记的结构载体建立有界结论。
+
+对一个受限语法片段 `L0` 和精确分析器 `A0`，定义：
+
+```text
+Sound(A0, property, L0)    := A0 接受 c ⇒ property(c)
+Complete(A0, property, L0) := property(c) ⇒ A0 接受 c
+```
+
+M0 守卫可以对固定载体和固定分发形式追求这两个性质，但不能对任意动态 Python 或
+TypeScript 宣称它们成立。值如果经过别名、配置、反射、外部输入或未识别语法流动，
+在有界分析覆盖它之前都属于 `unknown`。Unknown 是证据结果，不是“不存在”的证明。
+
+建议性的候选分类使用一个有限决策：
+
+```text
+reuse_existing | extend_vocabulary | create_vocabulary | local_only
+external_input | compatibility_only | unknown
+```
+
+这样可以让“流程分类”完备，即使程序分析本身不完备。`reuse_existing` 要求槽位相同、
+作用域兼容、契约等价。`extend_vocabulary` 要求给出反例，证明复用旧值会把两个需要
+不同处理的状态压成一个。`create_vocabulary` 要求出现新的语义定义域或独立 owner 与
+生命周期。如果证据不足以在这些情况之间做决定，默认就是 `unknown`；Agent 不能把
+未解析候选静默当成复用旧词。
+
+任意程序的行为等价通常不可判定，因此这个 schema 不会把 `same_concept` 自动提升为
+定理。只有当输入、输出、状态转换、持久化版本和有限测试域都明确时，行为等价才可
+在受限契约内成为阻断条件。这就是可用的证明骨架与“全程序语义收敛已被证明”之间的
+边界。
+
+候选处置在此仅为建议性元数据。注册表只保存允许标签与默认值，不存储逐候选决策，
+也不在产品代码中强制执行候选处理；漂移 smoke 只验证标签合同。
+
 ### 状态模型与 schema
 
 `loopx/semantics/vocabulary_v0.json`，`schema_version` 为
@@ -344,7 +390,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` | 有限的集合、角色关系与层次、语义义务、候选决策，以及已建立/有界/unknown/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次、候选决策和不变量 ID；属性实施阶段不能冒充已完成证明 |
 | `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
@@ -447,7 +493,7 @@ PR 中重新生成清单。
 | 有界上下文名字只能靠声明离开分叉预算（M0.5） | 为 `SOURCE_SURFACES` 声明四个上下文；另行只改名其中一处定义而不声明 | 声明把 `multi_value_forks` 降到 3；单独改名不降 | I14；诚实的修法是评审者看得见的注册表修改，改名是不碰注册表的代码改动 |
 
 | 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 |
-| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 |
+| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、候选决策、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 |
 
 已知边界，写明是为了不让这个检查被过度信任：
 
@@ -628,6 +674,14 @@ planner 条目则有意保留 `python3`。
 
 ## 附录 A：执行账本（非规范）
 
+### 2026-09-16 — 评审一致性修复
+
+- 每种语言只保留一个候选决策小节。
+- 注册表与叙述统一使用源码位点 `L`、环境值空间 `U(v)` 和允许集合 `S(v)`，
+  不把生产值预先定义为合法值。
+- 明确候选处置为建议性元数据；本 schema 不交付逐候选运行时存储或执行门禁。
+
+
 ### 2026-09-15 — 随 RFC 开启 M0
 
 - **基线：** `1dc6ad8d8`

examples/semantic-vocabulary-drift-smoke.py

@@ -51,7 +51,7 @@
 STATUSES = {"canonical", "legacy", "merge_candidate"}
 FORMAL_MODEL_KEYS = {
     "schema_version", "universes", "roles", "role_hierarchy", "relations", "invariants", "proof_boundary",
-    "enforcement_policy",
+    "enforcement_policy", "candidate_decisions",
 }
 FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0"
 FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"}
@@ -67,6 +67,15 @@
 }
 FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"}
 FORMAL_POLICY_KEYS = {"blocking_now", "blocking_next", "advisory", "unproved"}
+FORMAL_CANDIDATE_DECISIONS = {
+    "reuse_existing",
+    "extend_vocabulary",
+    "create_vocabulary",
+    "local_only",
+    "external_input",
+    "compatibility_only",
+    "unknown",
+}
 
 # 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
@@ -230,9 +239,17 @@ def check_formal_model(model: dict[str, Any]) -> None:
     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")
+    candidates = model["candidate_decisions"]
+    require(set(candidates) == {"values", "default", "meaning"},
+            "formal_model candidate_decisions must define values, default, and meaning")
+    require(candidates["values"] == sorted(FORMAL_CANDIDATE_DECISIONS),
+            "formal_model candidate_decisions must be a stable exhaustive classification")
+    require(candidates["default"] == "unknown",
+            "formal_model candidate_decisions must default unresolved candidates to unknown")
+    require(candidates["meaning"].strip(), "formal_model candidate_decisions needs a meaning")
     boundary = model["proof_boundary"]
-    require(set(boundary) == {"established", "bounded", "unproved"},
-            "formal_model proof_boundary must separate established, bounded, and unproved claims")
+    require(set(boundary) == {"established", "bounded", "unknown", "unproved"},
+            "formal_model proof_boundary must separate established, bounded, unknown, 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")