fix(semantics): report the formal detail ratios from what the checks walked

[songoow]

The formal detail report counted registered projections on both sides of its ratio, so an unexecuted second projection printed 2/2. It now reuses the existing formal-domain selectors and prints 1/2. This implements defect ③ from discussion #4738.

Merged current main (361347713) into this branch and resolved the test insertion conflict with #4747 by preserving both suites: projection detail regressions and canonical producer-domain regressions. The PR diff remains two files, +52/-4; enforcement and runtime behavior are unchanged.

Current-head validation:

• Focused semantic drift and real settlement-binding witness tests: 129 passed.
• Drift smoke passed: F1/F2 7/26, cross-runtime unverified 19/20, projections 1/1 on the real registry. The synthetic unexecuted projection still reports 1/2.
• git diff --check passed; GitHub now reports MERGEABLE. The previous-head full architecture result was 672 passed; it is not claimed as a rerun on this merge head.

The existing selector is the owning boundary, so no new abstraction, vocabulary or gate is needed. The new merge head requires review and CI; the prior approved head's review is historical.

Current-head CI repair

Head 1f2bf57d8167bb3a80be9a401874d0f8dbed1ea8 includes the verified repair for date-dependent manager-context fixtures. Shared module-budget repair from #4793 is included as dependency ancestry, with current main incorporated; once #4793 lands its shared diff disappears from this PR. The PR-specific implementation is unchanged by this update.

Focused current-head validation: 184 passed, no skips or failures in that run. Diff checks pass. This is local evidence; the newly triggered remote CI remains authoritative for readiness. No PR was merged and no new unrelated feature PR was opened.

[huangruiteng]

动机

我复审的是 4772@904345178454664823d54a02464d5a05b989c1df。结论：APPROVE，没有阻断项。

这个 PR 修的是一个真实、可复现、但不改变门禁判定的报告缺陷。summarise_formal_domains 原来把 len(registry['projections']) 同时当作 projections 比率的分子和分母，因此只要注册表有两行就会打印 2/2，即使 check_projections 实际仍只 import 并执行一个 projection owner。维护者最先看到的明细会因此把“已声明”误写成“已执行”。

我用同一个合成的未执行 projection 分别跑了 merge-base 916763e2 与当前 head：旧实现输出 2/2，当前 head 输出 1/2；真实注册表仍输出 1/1。这证明变化修正的是可观察报告语义，而不是为了让测试变绿而改文案。

改动思路

实现复用了已有权威边界，没有新建第二套计数：

1. check_invariant_domain 已通过 FORMAL_DOMAIN_SELECTORS 推导 formal invariant 的 verified/registered；
2. FORMAL_DOMAIN_SELECTORS['projections[*]'] 的分子取注册名与 EXECUTED_PROJECTIONS 的交集，分母取注册表全部 projection；
3. check_projections 再校验 EXECUTED_PROJECTIONS 中每个名字的 owner，并实际 import/执行 projection；
4. 本 PR 让 summarise_formal_domains 直接使用同一 selector pair，避免 renderer 自己重算并与检查器分叉。

declared_contexts 仍可能在成功输出时显示 100%，但这里不是同一个漏洞：check_scope_declarations 会先把每个声明 context 的 owner module 与 inventory 发现的全部 defining modules 做精确集合比较，缺失或多余都会失败。因此它表达的是“本次成功检查清掉了多少声明 context”，而不是一个允许缺口继续通过的覆盖率。

具体改动

关键内容讲解

• examples/semantic-vocabulary-drift-smoke.py 删除本地 projections=N/N 与 contexts=N/N 自计数，改为调用现有的 FORMAL_DOMAIN_SELECTORS['projections[*]'] 和 FORMAL_DOMAIN_SELECTORS['scope_declarations[*].contexts']；没有改变 main 的检查顺序、异常路径或退出码。
• test_the_formal_detail_line_cannot_report_a_projection_it_never_executed 加入决定性反例：在有效 registry 副本中加入一个不存在的 owner 后，detail 必须是 1/2，不能再是 2/2。
• test_the_formal_detail_line_agrees_with_the_selectors_it_reports 将两个公开标签与 selector 返回 pair 绑定，防止以后只修 formal invariant、却再次漏掉 detail renderer。

完整 diff 只有两个现有文件、+52/-4；没有生产运行时、schema、CLI、权限、持久化或新 gate。仓库检索未发现既有测试覆盖 projections= 明细与 selector 的一致性；同作者相邻的 producer soundness、ranking、formal evidence 和 action classification PR 也不是同形重复。本 PR 直接修既有 central smoke，而不是添加一次性 smoke 文件，具有持续回归价值。

对主干的风险

没有发现阻断风险。最强回归场景是：未来注册一个没有执行见证的 projection，报告仍显示 100%，维护者据此误判 F5 证据边界。当前实现通过共享 selector 消除了这个 renderer 分叉；负例从旧 head 的 2/2 变为当前 head 的 1/2，覆盖正中缺陷。

本轮独立验证：

检查	结果
uv run --extra test python examples/semantic-vocabulary-drift-smoke.py	通过；真实输出 F5:1/1、projections=1/1
merge-base/head 合成 mutation probe	通过；旧 2/2，新 1/2
uv run --extra test python -m pytest -q tests/architecture/test_semantic_vocabulary_drift.py	111 passed in 34.18s
uv run --extra test python -m pytest -q tests/architecture	672 passed in 101.60s
git diff --check origin/main...HEAD	通过
git merge-tree --write-tree HEAD origin/main	无冲突；tree 61c141f0026902cabc5621cb75d9f56ab72804b0
changed-file Ruff	仅报一个 render_inventory 未使用；该 import 已存在于 origin/main 且不在本 diff 中，没有新增 lint 回归

分支虽然显示 BEHIND，但当前 main 没有修改这两个文件，merge-tree 也证明无文本冲突。剩余风险只在既有策略：F5 允许把“注册但未执行”的未来 row 显示成部分覆盖；本 PR 的职责正是如实暴露它，不是改变 enforcement policy。

我的整体评价

APPROVE。 这是一个范围合适的报告语义修复：它把 detail renderer 接回已有的 typed/code-owned selector 权威，提供能区分旧新行为的负例，并保留现有 gate、domain 与 authority 语义。未来向前看也不需要新抽象；直接复用 selector 已经是最小、最容易回滚的边界。

English verdict: APPROVE - head 9043451. The exact head replaces a self-satisfying projection detail ratio with the existing code-owned formal-domain selector pair. An identical synthetic unexecuted projection prints 2/2 on the merge base and 1/2 here, while the real smoke, 111 focused tests, the full 672-test architecture suite, diff check, and conflict-free merge-tree all pass. No runtime or gate semantics change; the sole Ruff finding is pre-existing on origin/main.

[huangruiteng]

有冲突

[songoow]

Approval conclusion (author-owned PR; GitHub blocks formal self-approval)

动机

Discussion #4738 缺陷③可复现：旧 summarise_formal_domains 用 registry projection 数量同时做分子与分母，未执行的第二个 projection 仍显示 2/2。exact head 1f2bf57d8167bb3a80be9a401874d0f8dbed1ea8 在同一反例下输出 1/2。

改动思路

报告复用 FORMAL_DOMAIN_SELECTORS["projections[*]"]，不再维护本地计数。formal domain、报告和 check_projections 因而共享同一 executed set 与 owner 边界。

具体改动

• selector 分子只统计 registry 与 EXECUTED_PROJECTIONS 的交集，分母保留全部注册项。
• 报告打印 selector pair；当前树为 1/1，注入未执行 projection 为 1/2。
• owner 漂移、已执行项未注册或映射不完整继续失败关闭。
• 共享 Chat/Lark ancestry 的默认值、非法值与 404 行为也有独立 characterization。

对主干的风险

主要风险是报告再次与检查器漂移。新增反例和 selector 对齐测试分别约束两侧；315 semantic tests、drift smoke、diff 和最终 CI 通过。没有改变运行时、权限、验证域或词表。正文早期“两文件 diff”不是当前累计 head 的完整描述，但后段已披露共享 ancestry，且本次已审完整 diff。

我的整体评价

APPROVE。 报告分子现在确实来自执行集合，不再自证覆盖率。

English verdict: APPROVE — exact head 1f2bf57 replaces the self-satisfying ratio with the executed-projection selector, fails closed on drift, and passes semantic validation and CI.

[huangruiteng]

动机

我复审的是 exact head 1f2bf57d8167bb3a80be9a401874d0f8dbed1ea8，并按当前 origin/main 重新核对了真正的 PR 差异：只有 examples/semantic-vocabulary-drift-smoke.py 与 tests/architecture/test_semantic_vocabulary_drift.py 两个文件，+52/-4。PR 历史里的 Chat/Lark 共享 ancestry 已进入主干，不是这次结论的改动面。

这个修复针对的是一个容易被忽略、但会误导维护决策的语义差异。旧 summarise_formal_domains 把 len(registry['projections']) 同时作为 projections 比率的分子和分母，所以只要 registry 新增一行，无论 check_projections 是否 import/执行它，报告都会显示 100%。这会把“已声明”伪装成“已有执行证据”。我用同一个未执行 projection 反例实际对照了当前主干和本 head：主干输出 2/2，本 head 输出 1/2；缺陷真实存在，修复结果也可观察。

改动思路

实现没有再造一个计数器，而是直接复用已经存在、并被 check_invariant_domain 验证的 code-owned selector：

1. FORMAL_DOMAIN_SELECTORS['projections[*]'] 的分子只统计 registry key 与 EXECUTED_PROJECTIONS 的交集，分母是全部注册 projection；
2. check_invariant_domain 要求 F5 声明的 verified/registered 与这个 selector 完全一致；
3. check_projections 继续验证 EXECUTED_PROJECTIONS 里点名的 owner，并执行真实 projection；
4. summarise_formal_domains 现在只渲染同一 selector pair，不再维护第二套报告规则。

declared_contexts 也改成调用 F4 selector，但它仍会在成功输出时显示 100%。这里不是同一漏洞：main() 在输出前已经通过 check_inventory -> check_scope_declarations 对每个声明 context 与 inventory 发现的 defining modules 做精确集合验证，缺失或多余都会先失败。因此这个比率表达“本次 fail-closed 检查清掉了多少声明项”，注释把这一差异说清楚了。

具体改动

关键代码讲解

• examples/semantic-vocabulary-drift-smoke.py:756 的 summarise_formal_domains 删除 N/N 本地自计数，改为读取 projections[*] 和 scope_declarations[*].contexts 两个现有 selector 的 walked/registered pair；没有改变检查顺序、异常、exit code 或 registry。
• tests/architecture/test_semantic_vocabulary_drift.py:524 的 mutation regression 在真实 registry 副本中加入不存在的 projection owner，要求真实 registry 为 1/1、未执行第二行后为 1/2。这条用例直接命中旧缺陷，而不是从新实现反推期望。
• tests/architecture/test_semantic_vocabulary_drift.py:544 把两个公开 label 与各自 selector 返回值绑定，防止以后 formal invariant 与 detail renderer 再次分叉。

正向路径是：真实 registry 经 domain/projection 检查后，F5 与 detail 都输出 1/1。负向反例是：只增加一个从未执行的 registry row，registered 变为 2，walked 仍为 1，因此 detail 必须输出 1/2；如果有人同时伪造 F5 声明值，check_invariant_domain 仍会按 code-owned selector 失败关闭。

对主干的风险

没有发现阻断项。最强风险是 renderer 再次维护独立规则，或者把 F4 的成功态 100% 误判为另一处自证覆盖。当前实现分别用 selector 复用与明确注释处理了这两点，没有新增 vocabulary、typed state、substring heuristic、authority、gate、CLI 或持久化契约。

我在当前 exact head 上实际验证：

• 相同 synthetic input 的 base/head probe：当前主干 projections=2/2，本 head projections=1/2；
• test_semantic_vocabulary_drift.py + test_semantic_settlement_binding_witness.py：129 passed in 48.36s；
• 真实 semantic drift smoke 通过，输出 F1/F2 7/26、F5 1/1、projections=1/1、declared_contexts=4/4；
• npm run typecheck:control-plane 与 git diff --check 通过；
• 与当前 main 的 git merge-tree --write-tree 无冲突，tree 为 0e1f62e230b638303dc12f646a51fb7c3ed27b28；该合并结果保留主干已落地的 import/budget 清理，同时包含本修复，合并内容和改动测试的 Ruff 均通过；
• exact head 的 DCO、dependency review、build、兼容性、分片测试、stage2c、pytest 与 merge-gate 均成功，只有预期的发布/展示 job 跳过。

分支当前仍是 BEHIND，但当前 merge tree 已证明没有文本冲突；若作者更新产生新 head，仍需按新 exact head 复核。future-facing refactor 检查后不建议再抽 helper：直接复用现有 selector 已经消除了重复知识，再抽一层只会增加跳转。

我的整体评价

APPROVE。 这是一个边界小但证据充分的报告语义修复：它没有靠改文案或扩大预算掩盖问题，而是把 operator-visible detail 接回已有的 code-owned authority，并用一个能在旧实现失败、在新实现通过的反例锁定行为。当前 exact head 未发现需要修改的 blocker。

English verdict: APPROVE - Exact head 1f2bf57 replaces a self-satisfying projection detail ratio with the existing code-owned selector pair. The same unexecuted-projection fixture reports 2/2 on current main and 1/2 here; focused semantic tests, the real drift smoke, merge-tree/static validation, and required CI all pass without changing runtime or enforcement semantics.

The merge-base changed after approval.

[huangruiteng]

动机

我复审的是 exact head 1f2bf57d8167bb3a80be9a401874d0f8dbed1ea8，并按当前 origin/main 重新核对了真正的 PR 差异：只有 examples/semantic-vocabulary-drift-smoke.py 与 tests/architecture/test_semantic_vocabulary_drift.py 两个文件，+52/-4。PR 历史里的 Chat/Lark 共享 ancestry 已进入主干，不是这次结论的改动面。

这个修复针对的是一个容易被忽略、但会误导维护决策的语义差异。旧 summarise_formal_domains 把 len(registry['projections']) 同时作为 projections 比率的分子和分母，所以只要 registry 新增一行，无论 check_projections 是否 import/执行它，报告都会显示 100%。这会把“已声明”伪装成“已有执行证据”。我用同一个未执行 projection 反例实际对照了当前主干和本 head：主干输出 2/2，本 head 输出 1/2；缺陷真实存在，修复结果也可观察。

改动思路

实现没有再造一个计数器，而是直接复用已经存在、并被 check_invariant_domain 验证的 code-owned selector：

1. FORMAL_DOMAIN_SELECTORS['projections[*]'] 的分子只统计 registry key 与 EXECUTED_PROJECTIONS 的交集，分母是全部注册 projection；
2. check_invariant_domain 要求 F5 声明的 verified/registered 与这个 selector 完全一致；
3. check_projections 继续验证 EXECUTED_PROJECTIONS 里点名的 owner，并执行真实 projection；
4. summarise_formal_domains 现在只渲染同一 selector pair，不再维护第二套报告规则。

declared_contexts 也改成调用 F4 selector，但它仍会在成功输出时显示 100%。这里不是同一漏洞：main() 在输出前已经通过 check_inventory -> check_scope_declarations 对每个声明 context 与 inventory 发现的 defining modules 做精确集合验证，缺失或多余都会先失败。因此这个比率表达“本次 fail-closed 检查清掉了多少声明项”，注释把这一差异说清楚了。

具体改动

关键代码讲解

• examples/semantic-vocabulary-drift-smoke.py:756 的 summarise_formal_domains 删除 N/N 本地自计数，改为读取 projections[*] 和 scope_declarations[*].contexts 两个现有 selector 的 walked/registered pair；没有改变检查顺序、异常、exit code 或 registry。
• tests/architecture/test_semantic_vocabulary_drift.py:524 的 mutation regression 在真实 registry 副本中加入不存在的 projection owner，要求真实 registry 为 1/1、未执行第二行后为 1/2。这条用例直接命中旧缺陷，而不是从新实现反推期望。
• tests/architecture/test_semantic_vocabulary_drift.py:544 把两个公开 label 与各自 selector 返回值绑定，防止以后 formal invariant 与 detail renderer 再次分叉。

正向路径是：真实 registry 经 domain/projection 检查后，F5 与 detail 都输出 1/1。负向反例是：只增加一个从未执行的 registry row，registered 变为 2，walked 仍为 1，因此 detail 必须输出 1/2；如果有人同时伪造 F5 声明值，check_invariant_domain 仍会按 code-owned selector 失败关闭。

对主干的风险

没有发现阻断项。最强风险是 renderer 再次维护独立规则，或者把 F4 的成功态 100% 误判为另一处自证覆盖。当前实现分别用 selector 复用与明确注释处理了这两点，没有新增 vocabulary、typed state、substring heuristic、authority、gate、CLI 或持久化契约。

我在当前 exact head 上实际验证：

• 相同 synthetic input 的 base/head probe：当前主干 projections=2/2，本 head projections=1/2；
• test_semantic_vocabulary_drift.py + test_semantic_settlement_binding_witness.py：129 passed in 48.36s；
• 真实 semantic drift smoke 通过，输出 F1/F2 7/26、F5 1/1、projections=1/1、declared_contexts=4/4；
• npm run typecheck:control-plane 与 git diff --check 通过；
• 与当前 main 的 git merge-tree --write-tree 无冲突，tree 为 0e1f62e230b638303dc12f646a51fb7c3ed27b28；该合并结果保留主干已落地的 import/budget 清理，同时包含本修复，合并内容和改动测试的 Ruff 均通过；
• exact head 的 DCO、dependency review、build、兼容性、分片测试、stage2c、pytest 与 merge-gate 均成功，只有预期的发布/展示 job 跳过。

分支当前仍是 BEHIND，但当前 merge tree 已证明没有文本冲突；若作者更新产生新 head，仍需按新 exact head 复核。future-facing refactor 检查后不建议再抽 helper：直接复用现有 selector 已经消除了重复知识，再抽一层只会增加跳转。

我的整体评价

APPROVE。 这是一个边界小但证据充分的报告语义修复：它没有靠改文案或扩大预算掩盖问题，而是把 operator-visible detail 接回已有的 code-owned authority，并用一个能在旧实现失败、在新实现通过的反例锁定行为。当前 exact head 未发现需要修改的 blocker。

English verdict: APPROVE - Exact head 1f2bf57 replaces a self-satisfying projection detail ratio with the existing code-owned selector pair. The same unexecuted-projection fixture reports 2/2 on current main and 1/2 here; focused semantic tests, the real drift smoke, merge-tree/static validation, and required CI all pass without changing runtime or enforcement semantics.

The merge-base changed after approval.

[huangruiteng]

动机

我复审的是 exact head 1f2bf57d8167bb3a80be9a401874d0f8dbed1ea8，并按当前 origin/main 重新核对了真正的 PR 差异：只有 examples/semantic-vocabulary-drift-smoke.py 与 tests/architecture/test_semantic_vocabulary_drift.py 两个文件，+52/-4。PR 历史里的 Chat/Lark 共享 ancestry 已进入主干，不是这次结论的改动面。

这个修复针对的是一个容易被忽略、但会误导维护决策的语义差异。旧 summarise_formal_domains 把 len(registry['projections']) 同时作为 projections 比率的分子和分母，所以只要 registry 新增一行，无论 check_projections 是否 import/执行它，报告都会显示 100%。这会把“已声明”伪装成“已有执行证据”。我用同一个未执行 projection 反例实际对照了当前主干和本 head：主干输出 2/2，本 head 输出 1/2；缺陷真实存在，修复结果也可观察。

改动思路

实现没有再造一个计数器，而是直接复用已经存在、并被 check_invariant_domain 验证的 code-owned selector：

1. FORMAL_DOMAIN_SELECTORS['projections[*]'] 的分子只统计 registry key 与 EXECUTED_PROJECTIONS 的交集，分母是全部注册 projection；
2. check_invariant_domain 要求 F5 声明的 verified/registered 与这个 selector 完全一致；
3. check_projections 继续验证 EXECUTED_PROJECTIONS 里点名的 owner，并执行真实 projection；
4. summarise_formal_domains 现在只渲染同一 selector pair，不再维护第二套报告规则。

declared_contexts 也改成调用 F4 selector，但它仍会在成功输出时显示 100%。这里不是同一漏洞：main() 在输出前已经通过 check_inventory -> check_scope_declarations 对每个声明 context 与 inventory 发现的 defining modules 做精确集合验证，缺失或多余都会先失败。因此这个比率表达“本次 fail-closed 检查清掉了多少声明项”，注释把这一差异说清楚了。

具体改动

关键代码讲解

• examples/semantic-vocabulary-drift-smoke.py:756 的 summarise_formal_domains 删除 N/N 本地自计数，改为读取 projections[*] 和 scope_declarations[*].contexts 两个现有 selector 的 walked/registered pair；没有改变检查顺序、异常、exit code 或 registry。
• tests/architecture/test_semantic_vocabulary_drift.py:524 的 mutation regression 在真实 registry 副本中加入不存在的 projection owner，要求真实 registry 为 1/1、未执行第二行后为 1/2。这条用例直接命中旧缺陷，而不是从新实现反推期望。
• tests/architecture/test_semantic_vocabulary_drift.py:544 把两个公开 label 与各自 selector 返回值绑定，防止以后 formal invariant 与 detail renderer 再次分叉。

正向路径是：真实 registry 经 domain/projection 检查后，F5 与 detail 都输出 1/1。负向反例是：只增加一个从未执行的 registry row，registered 变为 2，walked 仍为 1，因此 detail 必须输出 1/2；如果有人同时伪造 F5 声明值，check_invariant_domain 仍会按 code-owned selector 失败关闭。

对主干的风险

没有发现阻断项。最强风险是 renderer 再次维护独立规则，或者把 F4 的成功态 100% 误判为另一处自证覆盖。当前实现分别用 selector 复用与明确注释处理了这两点，没有新增 vocabulary、typed state、substring heuristic、authority、gate、CLI 或持久化契约。

我在当前 exact head 上实际验证：

• 相同 synthetic input 的 base/head probe：当前主干 projections=2/2，本 head projections=1/2；
• test_semantic_vocabulary_drift.py + test_semantic_settlement_binding_witness.py：129 passed in 35.46s；
• 真实 semantic drift smoke 通过，输出 F1/F2 7/26、F5 1/1、projections=1/1、declared_contexts=4/4；
• npm run typecheck:control-plane 与 git diff --check 通过；
• 与最新 main 6c2976f8c3447a4bd1d3af79e251c2f78c9ed733 的 git merge-tree --write-tree 无冲突，tree 为 6faae3da723ebecc13c8c568fcdff2b1b06b1110；该合并结果保留主干的 import/budget 清理，同时包含本修复，合并内容和改动测试的 Ruff 均通过；
• npm run typecheck:control-plane 与 git diff --check 通过。本轮不读取、轮询或等待远端 CI。

分支当前仍是 BEHIND，但当前 merge tree 已证明没有文本冲突；若作者更新产生新 head，仍需按新 exact head 复核。future-facing refactor 检查后不建议再抽 helper：直接复用现有 selector 已经消除了重复知识，再抽一层只会增加跳转。

我的整体评价

APPROVE。 这是一个边界小但证据充分的报告语义修复：它没有靠改文案或扩大预算掩盖问题，而是把 operator-visible detail 接回已有的 code-owned authority，并用一个能在旧实现失败、在新实现通过的反例锁定行为。当前 exact head 未发现需要修改的 blocker。

上一条 formal approval 因基线推进被撤销。本轮失效检查确认：head 未变，当前 main 相对先前证据基线没有修改这两个 PR 文件，旧 2/2 反例的 baseline 实现也未变；关键 129 项测试、真实 drift smoke、合并内容 Ruff、typecheck、diff 与最新 merge tree 均重新验证，因此本条是对最新基线的独立重新确认，而非继承旧批准。

English verdict: APPROVE - Exact head 1f2bf57 replaces a self-satisfying projection detail ratio with the existing code-owned selector pair. The unchanged baseline still reports 2/2 for an unexecuted projection while this head reports 1/2; focused semantic tests, the real drift smoke, and current-main merge/static validation pass without changing runtime or enforcement semantics.

The merge-base changed after approval.