fix(semantics): two measurements that contradicted themselves

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

@@ -604,7 +604,11 @@ whole population of the same unit. An advisory or unproved stage walks nothing,
 so its `verified` count must be zero, and an enforced stage may not declare an
 empty domain. The selector and the evidence bound of each obligation are pinned
 by `FORMAL_DOMAIN_ANCHOR` in the smoke on the `COVERAGE_ANCHOR` pattern (I5), so
-an invariant cannot widen the set it claims through a registry edit alone. The
+an invariant cannot widen the set it claims through a registry edit alone. F5's
+`verified` count is the number of projections the smoke actually imports and
+executes, taken from `EXECUTED_PROJECTIONS` in code, not the registry's own row
+count; a registered projection with no executed check raises `registered`
+without raising `verified`, the way F1 reports 6 of 26. The
 producer scan reach is measured on every run instead of pinned, because its
 denominator moves with any new module; the smoke prints the current ratio, the
 unresolved-site total, and the share of that total no wider scan could ever
@@ -1142,6 +1146,42 @@ introduce a competing target state.
 
 ## Appendix A: Execution ledger (non-normative)
 
+### 2026-09-17 — Two measurements that contradicted themselves, corrected
+
+Normative for what F5's `verified` count means and for closed-set collision
+identity. No budget, floor or anchor was relaxed; both changes were reproduced
+against `d8e7af141` before being written.
+
+- **A declaration was counting as its own evidence (F5).** The
+  `projections[*]` selector returned `len(registry["projections"])` for *both*
+  `verified` and `registered`, while `check_projections` imported exactly one
+  hardcoded projection. Adding a projection whose owner module and function do
+  not exist anywhere in the tree, and declaring the domain as 2/2, passed the
+  whole smoke and printed `F5:2/2` under the evidence bound
+  `executable_owner_function`. `verified` now counts only the projections named
+  in `EXECUTED_PROJECTIONS`, which is code, and each one's registry `owner` must
+  equal the function the check imports. The same injection now either fails
+  (`claims 2 verified members ... the m0 check walks 1`) or is declared honestly
+  and prints `F5:1/2`.
+- **Reordering a `set` counted as a semantic fork.** Collision identity used
+  `tuple(item["values"])`, which is source order. Swapping three lines inside a
+  `set` literal — membership unchanged — turned a twin into a fork and failed
+  the gate on three budgets at once, while `divergent_value_sets`, computed from
+  the same inventory, correctly reported no divergence: one scan, two outputs,
+  and the wrong one held the gate. Identity is now membership when *every*
+  definition of a name is a `set`/`frozenset`, and source order otherwise.
+- **The normalization is deliberately narrow.** `tuple`, `list` and `as const`
+  carriers keep order-sensitive identity, because `LIFECYCLE_PRIORITY` is a
+  tuple defined in two modules whose order *is* the priority; normalizing every
+  carrier would have replaced a false positive with a false negative. A name
+  carried by mixed containers also stays order-sensitive, which makes the rule a
+  pure relaxation: it can only merge definitions the old rule split, so no
+  untouched tree starts failing.
+- **What this does not do.** It does not establish the ordering semantics of
+  enums or `Literal` aliases, which carry no container and are left
+  order-sensitive; and it does not add a second executed projection. F5 still
+  walks one.
+
 ### 2026-09-17 — B2: three bounded binding forms, and the residue that stays unresolved
 
 - **Trigger:** [#4447](https://github.com/huangruiteng/loopx/issues/4447) recorded

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

@@ -482,7 +482,9 @@ R ⊆ L × V × Version               将值持久化
 建议性（advisory）与未证明（unproved）阶段什么都不走，因此 `verified` 必须为 0；
 已强制阶段则不得声明空值域。每条义务的 selector 与证据边界由 smoke 里的
 `FORMAL_DOMAIN_ANCHOR` 按 `COVERAGE_ANCHOR` 同一模式钉住（I5），因此不可能只改数据
-就扒宽一条不变量所声称的范围。producer 扫描范围本身每次运行现算而不钉住，
+就扒宽一条不变量所声称的范围。F5 的 `verified` 取的是 smoke 真正导入并执行的投影
+条数，来自代码里的 `EXECUTED_PROJECTIONS`，而不是注册表自身的行数；已注册但没有
+对应执行检查的投影只抬高 `registered`，不抬高 `verified`，与 F1 报 6/26 同理。producer 扫描范围本身每次运行现算而不钉住，
 因为分母会随任何新模块移动；smoke 会打印当前比值、未解析位点总数，以及其中
 再宽的扫描也永远无法解析的那一部分（E21）。
 
@@ -920,6 +922,32 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共
 
 ## 附录 A：执行账本（非规范）
 
+### 2026-09-17 — 两处自相矛盾的度量已修正
+
+对 F5 的 `verified` 含义与闭集碰撞身份是规范性的。没有放松任何预算、下限或锚点；
+两处都先在 `d8e7af141` 上复现，再动笔。
+
+- **声明把自己当成了证据（F5）。** `projections[*]` selector 的 `verified` 与
+  `registered` 都返回 `len(registry["projections"])`，而 `check_projections` 只
+  导入了一个写死的投影。加入一个 owner 模块与函数在整棵树里都不存在的投影，并把
+  值域声明成 2/2，完整 smoke 依然通过，并在证据边界 `executable_owner_function`
+  之下打印 `F5:2/2`。现在 `verified` 只统计代码里 `EXECUTED_PROJECTIONS` 点名的
+  投影，且每个投影在注册表里的 `owner` 必须等于检查真正导入的那个函数。同样的注入
+  现在要么失败（`claims 2 verified members ... the m0 check walks 1`），要么如实
+  声明并打印 `F5:1/2`。
+- **重排 `set` 被算成语义分叉。** 碰撞身份用的是 `tuple(item["values"])`，即源码
+  顺序。把一个 `set` 字面量里的三行调换位置——成员完全没变——就会把孪生变成分叉，
+  一次触发三个预算失败；而由同一份 inventory 算出的 `divergent_value_sets` 正确
+  地报告没有分歧：一次扫描、两个输出，且挡住 CI 的是错的那个。现在只有当一个名字
+  的**每一个**定义都是 `set`/`frozenset` 时才按成员判定身份，否则仍按源码顺序。
+- **这个归一化是刻意收窄的。** `tuple`、`list` 与 `as const` 载体保持顺序敏感，
+  因为 `LIFECYCLE_PRIORITY` 就是一个定义在两个模块里的 tuple，它的顺序就是优先级；
+  一刀切归一化等于用一个假阴性换掉一个假阳性。同一名字若由不同容器承载，同样保持
+  顺序敏感——这让该规则成为纯粹的放松：它只会合并旧规则拆开的定义，因此不会让任何
+  未改动的代码树开始失败。
+- **它没有做什么。** 它没有确立 enum 与 `Literal` 别名的顺序语义——这些载体不带
+  container，仍按顺序敏感处理；也没有新增第二个可执行投影，F5 仍然只走一个。
+
 ### 2026-09-17 — B2：三条有界绑定形式，以及仍然保持未解析的残量
 
 - **起因：**[#4447](https://github.com/huangruiteng/loopx/issues/4447) 把 B2 残量

examples/semantic-vocabulary-drift-smoke.py

@@ -110,10 +110,28 @@
         sum(len(entry["contexts"]) for entry in registry["scope_declarations"].values()),
         sum(len(entry["contexts"]) for entry in registry["scope_declarations"].values()),
     ),
-    "projections[*]": lambda registry: (len(registry["projections"]), len(registry["projections"])),
+    # ``verified`` counts the projections ``check_projections`` actually imports
+    # and executes, not the registry's own row count. A registry entry is a
+    # declaration; counting it as its own evidence let a projection whose owner
+    # function does not exist report itself verified. An unexecuted entry now
+    # raises ``registered`` without raising ``verified``, the same way F1
+    # reports 6 of 26.
+    "projections[*]": lambda registry: (
+        sum(1 for name in registry["projections"] if name in EXECUTED_PROJECTIONS),
+        len(registry["projections"]),
+    ),
     # No site declares a persists edge, so F6 has an empty domain, not a small one.
     "persists_edges[*]": lambda registry: (0, 0),
 }
+# The projections F5 executes, and the owner each one must name. Pinned in code
+# for the same reason as COVERAGE_ANCHOR and FORMAL_DOMAIN_ANCHOR: a data-only
+# edit to the registry must not be able to widen what the invariant claims to
+# have verified, and the owner string has to stay tied to the function the check
+# below imports rather than being prose the registry can restate.
+EXECUTED_PROJECTIONS = {
+    "turn_route_to_loop_disposition":
+        "loopx/control_plane/turn_driver/turn_contract_generated.py::project_turn_route",
+}
 FORMAL_ENFORCED_STAGES = frozenset(FORMAL_ENFORCEMENT - {"advisory", "unproved"})
 # What a verified sub-domain rests on, and which stages may claim it. The first
 # three describe evidence something actually walked, so only an enforced stage
@@ -708,6 +726,13 @@ def resolve(member: str) -> None:
 
 
 def check_projections(registry: dict[str, Any]) -> None:
+    for name, owner in EXECUTED_PROJECTIONS.items():
+        require(name in registry["projections"],
+                f"projection {name} is executed by this check but is not registered")
+        declared = registry["projections"][name].get("owner")
+        require(declared == owner,
+                f"projection {name} names owner {declared}; this check executes {owner}, "
+                "so the registry would be crediting a function it does not run")
     projection = registry["projections"]["turn_route_to_loop_disposition"]
     from loopx.control_plane.turn_driver.driver import LoopXTurnRoute
     from loopx.control_plane.turn_driver.turn_contract_generated import LoopDisposition, project_turn_route

loopx/semantics/inventory.py

@@ -221,6 +221,34 @@ def multi_value_carriers(
     return carriers
 
 
+# Containers whose element order the language does not preserve. Two definitions
+# of the same ``set``/``frozenset`` that list the same members in a different
+# order are the same closed set, so reordering one must not invent a fork.
+# ``tuple``, ``list`` and ``as const`` arrays are deliberately excluded: a
+# carrier like ``LIFECYCLE_PRIORITY`` spends its order as its meaning, and
+# normalizing it would hide a real divergence instead of a fake one.
+UNORDERED_CONTAINERS = frozenset({"set", "frozenset"})
+
+
+def _collision_keys(carriers_for_name: list[dict[str, Any]]) -> set[tuple[str, ...]]:
+    """The distinct value sets one name carries; one key means the name agrees.
+
+    Membership decides identity only when *every* definition of the name is an
+    unordered container. A name carried by a ``tuple`` in one module and a
+    ``set`` in another keeps order-sensitive identity, so this can only ever
+    merge definitions that the old rule split -- it never splits a pair the old
+    rule merged, and cannot make an untouched tree start failing.
+
+    Carriers with no ``container`` (enums, ``Literal`` aliases, TypeScript
+    ``as const`` arrays) are ordered by this rule, which reports a reordering
+    rather than hiding it -- the safe direction while their own ordering
+    semantics are unestablished here.
+    """
+    if all(item.get("container") in UNORDERED_CONTAINERS for item in carriers_for_name):
+        return {tuple(sorted(set(item["values"]))) for item in carriers_for_name}
+    return {tuple(item["values"]) for item in carriers_for_name}
+
+
 def multi_value_name_collisions(
     carriers: list[dict[str, Any]],
 ) -> tuple[list[dict[str, Any]], list[dict[str, Any]]]:
@@ -249,7 +277,9 @@ def multi_value_name_collisions(
             key=lambda item: item["module"],
         )
         entry: dict[str, Any] = {"name": name, "definitions": definitions}
-        if len({tuple(item["values"]) for item in definitions}) == 1:
+        # Keyed off the raw carriers, which still carry ``container``; the
+        # ``definitions`` entries keep their source order for review.
+        if len(_collision_keys(carriers_for_name)) == 1:
             entry["values"] = definitions[0]["values"]
             entry["modules"] = [item["module"] for item in definitions]
             twins.append(entry)

tests/architecture/test_semantic_inventory.py

@@ -17,6 +17,7 @@
 import pytest
 
 from loopx.semantics.inventory import (
+    multi_value_name_collisions,
     INVENTORY_SCHEMA_VERSION,
     SourceFile,
     build_inventory,
@@ -387,3 +388,86 @@ def test_typescript_single_quoted_carriers_are_visible(repo: Path) -> None:
     inventory = build_inventory(repo)
     assert inventory["typescript_const_arrays"][0]["values"] == ["one", "two"]
     assert any(item["name"] == "SHARED" for item in inventory["duplicate_definitions"]["same_runtime_forks"])
+
+
+def _carrier(module: str, values: list[str], container: str = "set") -> dict:
+    return {
+        "kind": "python_closed_set", "name": "STATES", "module": module,
+        "values": values, "container": container,
+    }
+
+
+def test_reordering_an_unordered_carrier_is_not_a_fork() -> None:
+    """A ``set`` has no element order, so listing the same members differently
+    is the same closed set. Before this rule, re-indenting a set literal
+    manufactured a semantic fork and blocked the gate, while the divergence
+    report computed from the same inventory correctly saw no divergence -- two
+    outputs of one scan disagreeing, with the wrong one holding the gate.
+    """
+    twins, forks = multi_value_name_collisions([
+        _carrier("loopx/a.py", ["open", "closed"]),
+        _carrier("loopx/b.py", ["closed", "open"]),
+    ])
+    assert [row["name"] for row in twins] == ["STATES"]
+    assert forks == []
+    # Diagnostics keep source order; only the identity key is normalized.
+    assert [item["values"] for item in twins[0]["definitions"]] == [
+        ["open", "closed"], ["closed", "open"],
+    ]
+
+
+def test_changing_membership_of_an_unordered_carrier_is_still_a_fork() -> None:
+    twins, forks = multi_value_name_collisions([
+        _carrier("loopx/a.py", ["open", "closed"]),
+        _carrier("loopx/b.py", ["open", "shut"]),
+    ])
+    assert twins == []
+    assert [row["name"] for row in forks] == ["STATES"]
+
+
+def test_reordering_an_ordered_carrier_is_still_a_fork() -> None:
+    """``tuple`` and ``list`` carriers spend their order as meaning.
+
+    ``LIFECYCLE_PRIORITY`` is a tuple defined in two modules: the order *is* the
+    priority. Normalizing every carrier to sorted membership would trade a false
+    positive for a false negative and hide that divergence, so orderedness is
+    read from the container the source actually used.
+    """
+    for container in ("tuple", "list"):
+        twins, forks = multi_value_name_collisions([
+            _carrier("loopx/a.py", ["first", "second"], container),
+            _carrier("loopx/b.py", ["second", "first"], container),
+        ])
+        assert twins == [], container
+        assert [row["name"] for row in forks] == ["STATES"], container
+
+
+def test_a_name_carried_by_mixed_containers_keeps_order_sensitive_identity() -> None:
+    """Membership decides identity only when every definition is unordered.
+
+    This keeps the rule a pure relaxation: it can only merge definitions the old
+    rule split, never split a pair it merged, so no untouched tree starts
+    failing because one side of a name is a tuple.
+    """
+    twins, forks = multi_value_name_collisions([
+        _carrier("loopx/a.py", ["open", "closed"], "set"),
+        _carrier("loopx/b.py", ["open", "closed"], "tuple"),
+    ])
+    assert [row["name"] for row in twins] == ["STATES"]
+    assert forks == []
+
+
+def test_a_carrier_without_a_container_stays_order_sensitive() -> None:
+    """Enums, ``Literal`` aliases and ``as const`` arrays carry no ``container``.
+
+    Their ordering semantics are not established here, so they keep the
+    reporting behaviour rather than being silently normalized.
+    """
+    twins, forks = multi_value_name_collisions([
+        {"kind": "python_enum", "name": "STATES", "module": "loopx/a.py",
+         "values": ["open", "closed"]},
+        {"kind": "python_enum", "name": "STATES", "module": "loopx/b.py",
+         "values": ["closed", "open"]},
+    ])
+    assert twins == []
+    assert [row["name"] for row in forks] == ["STATES"]

tests/architecture/test_semantic_vocabulary_drift.py

@@ -718,3 +718,63 @@ def test_inventory_report_discloses_budget_slack(monkeypatch):
     )
     _, line = smoke["check_inventory"](widened, sources)
     assert "slack=conflicting_values=2" in line, line
+
+
+def _with_unexecuted_projection(registry: dict) -> dict:
+    registry = copy.deepcopy(registry)
+    registry["projections"]["unexecuted_probe"] = {
+        "meaning": "A projection whose owner module and function do not exist.",
+        "owner": "loopx/semantics/does_not_exist.py::no_such_function",
+        "mapping": {"a": "b"},
+    }
+    return registry
+
+
+def test_an_unexecuted_projection_cannot_count_itself_as_verified() -> None:
+    """F5 claims the evidence bound ``executable_owner_function``.
+
+    Before this, ``verified`` was ``len(registry["projections"])`` -- the
+    registry's own row count standing in for evidence -- while
+    ``check_projections`` only ever imported one hardcoded projection. Adding a
+    projection whose owner function does not exist anywhere in the tree passed
+    the full smoke and reported ``F5:2/2``. A declaration was counting as its
+    own proof.
+    """
+    smoke = runpy.run_path(str(SMOKE))
+    registry = _with_unexecuted_projection(smoke["load_registry"]())
+    walked, population = smoke["FORMAL_DOMAIN_SELECTORS"]["projections[*]"](registry)
+    assert (walked, population) == (1, 2)
+
+
+def test_declaring_an_unexecuted_projection_as_verified_fails() -> None:
+    smoke = runpy.run_path(str(SMOKE))
+    registry = _with_unexecuted_projection(smoke["load_registry"]())
+    for invariant in registry["formal_model"]["invariants"]:
+        if invariant["id"] == "F5_projection_totality":
+            invariant["domain"]["registered"] = 2
+            invariant["domain"]["verified"] = 2
+    with pytest.raises(smoke["Drift"], match="claims 2 verified members"):
+        smoke["check_formal_model"](registry["formal_model"], registry)
+
+
+def test_a_projection_owner_the_check_does_not_run_is_rejected() -> None:
+    """The owner string must name the function ``check_projections`` imports.
+
+    Otherwise the registry can point at any module while the check keeps
+    exercising the real one, and the invariant credits a function it never ran.
+    """
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke["load_registry"]())
+    registry["projections"]["turn_route_to_loop_disposition"]["owner"] = (
+        "loopx/semantics/elsewhere.py::some_other_function"
+    )
+    with pytest.raises(smoke["Drift"], match="crediting a function it does not run"):
+        smoke["check_projections"](registry)
+
+
+def test_every_executed_projection_must_be_registered() -> None:
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke["load_registry"]())
+    del registry["projections"]["turn_route_to_loop_disposition"]
+    with pytest.raises(smoke["Drift"], match="is not registered"):
+        smoke["check_projections"](registry)