fix(semantics): state each formal invariant over the domain it verifies

[songoow]

What

Each formal invariant (F1–F6) now states the domain it actually quantifies over, and the smoke enforces that the stated domain cannot silently widen.

This is a normative change to the registry's formal model and both RFC mirrors — it needs maintainer review.

Why

The invariants were stated as unconditioned universals (Produced(v) ⊆ S(v)) but only verified over a true subdomain:

• F1/F2: 6 of 26 vocabularies (kernel only), scan reach 432/1203 files
• F3: 0 of 26 (advisory, escape clause)
• F4: 4 of 4 scope declarations
• F5: 1 of 1 projection (the genuinely blocking one)
• F6: 0 (persistence compatibility, honestly unproved)

The lanes were pinned to propositions stronger than what any check verifies. The registry now prints this every run:

formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0
formal_domain_bounds: kernel_with_producers=6/6 cross_runtime_unverified=20/20
                      producer_scan_reach=432/1203_files
unresolved_producer_sites=41 (not proven safe; 15 can never become evidence)

cross_runtime_unverified=20/20 is the headline: the highest-risk tier has zero F1/F2 coverage, stated in the registry for the first time (previously only discoverable by reading the scanner code).

Anti-escalation anchor

FORMAL_DOMAIN_ANCHOR pins each (selector, bound) pair in the smoke, so an invariant cannot widen its own domain by editing the registry alone. Mutation-tested:

attack	result
edit registry lane only	rejected
+ evidence_bound (self-consistent)	rejected
+ verified (fully self-consistent)	rejected
+ code anchor (two-file)	rejected by the pre-existing lane check
+ enforcement_policy lane (three-part)	accepted — see residual

Stated residual (known gap, not fixed here)

A fully self-consistent three-part edit (registry invariant + registry policy lane + smoke anchor) can still claim an unimplemented invariant is blocking_now. The anchor pins which set an invariant quantifies over, never which function raises. The enforced_by grounding gap remains open; closing it is a separate change and should not block this one.

Also fixes

• F4's statement is rewritten to the enumerable form actually enforced (declaration completeness: every defining module named exactly once, owner symbol matches the declaration) — the old statement was a definition, not a falsifiable claim.
• The check_producers comment that mislabeled the 20 skipped vocabularies as "other kernel families" — they are the entire cross_runtime tier.

Validation

• python3.11 examples/semantic-vocabulary-drift-smoke.py — green, now printing the formal_domain and bounds lines
• python3.11 -m pytest -q tests/architecture/test_semantic_vocabulary_drift.py — 90 passed (32 new tests cover the domain anchor and the reworded F4)
• RFC en/zh mirrors updated in lockstep

Known interactions

Conflicts with #4614 (RFC + registry + tests) and #4626 (registry + tests); resolutions are additive. Merge-tree clean against #4617 / #4606 / #4608 / #4628 / #4629 / #4630.

[songoow]

本 PR 在 #4447 计划中的位置

issue #4447 现在有一节统一协调（中英双语），把这 13 个在开 PR 作为一个计划列出：各自修什么、为何必要、以及实测出的合并顺序。

冲突实测：对全部 78 对做了试合并，9 对冲突，分四簇，每一处都是文本相邻，没有一处是语义分歧。

冲突簇	涉及 PR	后合并者的解法
棘轮锚点	#4606、#4608、#4617、#4629	四者全部合并后的终态已实测：same_runtime_forks 18、same_runtime_fork_definitions 41、same_runtime_forks_semantic 11、conflicting_values 16、conflicting_definitions 55、multi_value_twins 13。registry 与 BUDGET_ANCHOR 两处都要带同一组值（该检查是相等而非 <=）
漂移测试文件	#4626、#4629、#4631	三者都在文件末尾追加，全部保留即可
RFC 双镜像	#4614、#4627、#4631	附录 B 决策行，按日期先后保留两条
清单与生成器	#4614、#4630	加法式：owner 对过滤与改名不变性证据同时保留

建议顺序（代价从低到高）：#4628 → #4625、#4626 → #4627 → #4619、#4621 → #4630 → #4614 → #4631 → #4629 → #4617 → #4606 → #4608。四个棘轮 PR 放最后，因为每落地一个，下一个的数字就从估算变成确定值。

全部 13 个 PR 现已同步到 main、零失败检查。

[songoow]

exact-head 复核（25e1d535c）— 同步 main 并解冲突

#4614 在本分支开会期间合并了，两者都向附录 B 决策日志追加一条带日期的行。按日期先后两条都保留，两份镜像一致：

| 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory ...
| 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 ...

附录 B 按设计就是只追加的决策日志，两条行互不修改对方，因此没有"取哪一侧"的问题——这也是我预判的四个冲突簇里唯一一个冲突本身就是期望形态的。

验证：docs-governance-smoke ok；tests/architecture/test_semantic_vocabulary_drift.py 93 passed。合并提交带 DCO 签名。

[huangruiteng]

Reviewed exact head: c035fd4f17d5dae5d7cb0e1d065b670bf02fbda7 (codex/invariant-domain).

动机

形式模型里的 F1/F2 原本写成无条件的全称命题（Produced(v) ⊆ S(v) ⊆ U(v)），但检查实际只走声明了 producer 的 kernel 层（26 个词表里的 6 个，扫描覆盖 1206 个文件里的 435 个）；F3 是 advisory 逃生条款、F6 是 unproved。也就是说lane 被钉在比任何检查都强的命题上，而且最强风险层（cross_runtime，20 个词表）的零覆盖只能靠读 scanner 代码才发现。

改动后每个不变量都声明它实际量化的集合，并且 smoke 每轮打印这些数字：formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0，以及 kernel_with_producers=6/6 cross_runtime_unverified=20/20 producer_scan_reach=435/1206_files。这是把「证明契约」从口号变成可核对事实的完整切片。

改动思路

入口是 check_formal_model -> check_invariant_domain。归属设计对：selector 与 evidence bound 是代码所有的枚举（FORMAL_DOMAIN_SELECTORS / FORMAL_EVIDENCE_BOUNDS），verified/registered 每次从注册表推导，FORMAL_DOMAIN_ANCHOR 把每个不变量的 (selector, bound) 钉在代码里——这正是仓库既有的 COVERAGE_ANCHOR/BUDGET_ANCHOR 模式，而不是新机制。校验还包含：advisory/unproved 阶段必须 verified == 0（「不走的阶段就是不走的」由机器判定而非散文声明）、enforced 阶段必须等于实际走到的数量且非空、verified <= registered。

展示侧 summarise_formal_domains 只做投影：数字来自已被校验的注册表，扫描覆盖量则在运行时从树测量（因为分母会随任何新模块变化，写死会误伤无关 diff）。

具体改动

5 个文件、+588/-38：smoke 约 60 行（selector/anchor/校验/打印 + 一处注释修正）、测试约 200 行（32 个新用例）、其余是注册表 formal_model 与 RFC 中英镜像的规范性改写（F4 改成 check_scope_declarations 真正执行的「枚举完整性」命题，因为它原来是定义而不是可反驳的断言）。

我独立复现的核对结果：smoke → ok 且打印上面两行；pytest tests/architecture/test_semantic_vocabulary_drift.py -q → 93 passed；其它计数面与 merge-base 一致（coverage 26/26、same_runtime_forks 18/18、multi_value_twins 13/13、conflicting_values_semantic 0/0）；unresolved_producer_sites=41 (not proven safe; 15 can never become evidence) 的注释也与正文一致。正文里的 432/1203_files 是其较早 head 的快照，本 head 合并新 main 后为 435/1206，属正常漂移。

关键代码讲解

• FORMAL_DOMAIN_SELECTORS / FORMAL_EVIDENCE_BOUNDS / FORMAL_DOMAIN_ANCHOR（smoke 93 起）：selector 从注册表推导 (walked, population)，bound 与 stage 有兼容表（producer_scan_reach/declared_defining_modules/executable_owner_function 只允许 enforced 阶段，inventory_only 只允许 advisory，unmodelled 只允许 unproved），anchor 保证注册表数据不能自选更宽的集合。
• check_invariant_domain（382 起）：把「声明 vs 实际」逐项对齐，报错信息直接点名不变量与分歧；enforced 阶段还要求 verified > 0，所以「空域上声称已强制」会被拒。
• summarise_formal_domains / producer_scan_reach（617/591 起）：前者投影已校验的数字，后者在运行时数树上的可达文件——注释解释了为什么不把分母写进注册表。
• formal_model.invariants[*].domain（注册表 73 起）：F1/F2 = vocabularies[tier=kernel].producers + producer_scan_reach，F3 = advisory + inventory_only 且 verified 0，F4 = scope_declarations[*].contexts 4/4，F5 = projections[*] 1/1，F6 = persists_edges[*] 空域 + unmodelled；proof_boundary.unproved 新增 cross_runtime_producer_closedness。我逐条把它和实际执行的检查对过。

对主干的风险

这是规范性改动，最大风险是「反升级锚」名不副实。我把 smoke 作为模块导入（这样 patch REGISTRY_PATH 才是活的），对注册表副本做了四组变更并跑真实 main()：

变更	结果
A 只改注册表 lane（把 F1 宽到 vocabularies[*]）	拒绝（anchor 报出分歧）
B 注册表 + 自洽的 policy lane（把 F1 降为 advisory）	拒绝（anchor）
C 注册表 + policy + 代码 anchor（三段自洽）	接受（与正文声明的 residual 一致）
D/E 只改注册表：把 F1/F2 的 statement 还原成改写前的无条件全称式	接受（见 F1）

也就是说：声明域本身确实钉住了，作者在正文里主动声明的「三段自洽仍可把未实现的不变量标成 blocking_now」也属实（anchor 钉的是集合，不是抛错函数），这条 residual 应当作为独立后续保留。

一条 P2（F1，非阻塞）：statement 文本没有锚，所以这次修的那个缺陷本身可以只用注册表改动复活。check_invariant_domain 只要求 statement.strip() 非空；我把 F1 的 statement 还原为 Produced(v) ⊆ S(v) ⊆ U(v)（F2 同理）后，main() 返回 0、测试全绿——即「不变量被写回比检查更强的全称命题」这个 PR 试图消灭的缺陷可以静默回归，同时两份 RFC 镜像还会与注册表不一致而无人报错。最小修复：把量化词也锚住（例如按 evidence bound 要求 statement 必须含 Kernel(V) 量化词并点名 bound），或把 statement 移进代码 anchor、注册表只留计数，并补一个「只改 statement 期望 Drift」的测试。

我的整体评价

结论 APPROVE。这是把形式模型从「听起来更强」修成「说得出实际覆盖」的正确方向：domain 由代码所有的 selector 推导、anchor 阻止注册表自行放宽、advisory/unproved 的 0 覆盖被如实打印，且作者主动披露了 enforced_by 仍未落地这一条。我独立复现了正文的 A/B/C 三组反升级行为，确认 D/E 这条未覆盖路径，跑了 smoke 与 93 个测试。回退成本是一个 commit。

F1 是同一机制内的一个缺口（statement 未锚），非阻塞，但值得在合并前顺手补上——否则这份 PR 的核心保证只在「域元组」这一半成立。

English verdict: APPROVE - exact head c035fd4; each formal invariant now declares the set it quantifies over with code-owned selectors and a code anchor, the smoke derives and prints the coverage (F1/F2 6/26 kernel vocabularies over 435/1206 files, cross_runtime_unverified=20/20), and I reproduced the anti-escalation behaviour myself (registry-only and self-consistent registry+policy widenings rejected, the three-part edit accepted exactly as the PR discloses). 93 architecture tests pass and the other smoke counters are unchanged. One non-blocking P2: the invariant statement text is not anchored, so a registry-only edit restoring F1/F2's pre-PR unconditional wording is accepted with a green suite, which is the very overstatement this PR fixes; anchoring the quantifier (or moving the statement into the anchor) would close it.

[songoow]

Head moved: merged main, so the existing approval no longer covers this head (5a69bda48).

main gained #4619, #4621, #4625, #4626, #4627, #4628, #4632 and #4634 since the review. The only conflict was the end of tests/architecture/test_semantic_vocabulary_drift.py, where #4625 and #4626 append their value-notes coverage blocks and this branch appends the invariant-domain fixtures — the append-at-end cluster #4447's merge-order table names, whose stated resolution is "keep every block; there is no overlap". Both sides are kept, theirs first. No behaviour or invariant text changed in the merge.

Revalidated on the integrated tree: semantic-vocabulary-drift-smoke ok, docs-governance-smoke ok, pytest tests/architecture/ 331 passed.

Per the exact-head rule in AGENTS.md, this needs a re-confirmation on 5a69bda48 rather than carrying the earlier approval forward.

[huangruiteng]

Reviewed exact head: 5a69bda4811302f7ff9ab7c4ba9248e2acb416f6 (codex/invariant-domain, re-review after the earlier head c035fd4f1 was superseded by a main merge).

动机

未变：形式模型里的 F1/F2 写成无条件的全称命题（Produced(v) ⊆ S(v) ⊆ U(v)），但检查实际只走「声明了 producer 的 kernel 词表」——26 个词表里的 6 个。也就是说 lane 被钉在比任何检查都强的命题上，而覆盖缺口与 cross_runtime 层在输出里完全看不见。F3 是 advisory、F6 是 unproved，同样没有任何地方指出它们其实什么都没走。这个动机在本次 head 上仍然成立。

改动思路

把「每个不变量到底量化在哪个集合上」变成代码所有、每次运行重新推导的东西：register 侧只声明 selector 名字与计数，真正的集合由 smoke 里的 selector 映射给出；构造一个 FORMAL_DOMAIN_ANCHOR（沿用仓库既有的 COVERAGE_ANCHOR/BUDGET_ANCHOR 模式）钉住「哪个不变量属于哪个集合与哪种证据边界」，并规定 advisory/unproved 阶段的 verified 必须是 0。计数从注册表推导，所以树变了而声明没跟着变会在同一次 diff 里失败。

具体改动

5 个文件、+588/-38（相对当前 main；本次 head 只多了 main 合并，内容增量与上次 review 相同）：

• loopx/semantics/vocabulary_v0.json：六个不变量重写为在其真实域上的命题，并新增 domain.quantifies_over / verified / registered / evidence_bound。
• examples/semantic-vocabulary-drift-smoke.py：新增 FORMAL_DOMAIN_SELECTORS（lambda 从注册表演化计数）、FORMAL_EVIDENCE_BOUNDS（哪种证据边界允许出现在哪个阶段）、FORMAL_DOMAIN_ANCHOR（把不变量钉到 selector+bound）；check_formal_model(model, registry) 现在接收注册表并在最后校验；load_registry 改为在词表/扫描校验之后再校验形式模型。
• tests/architecture/test_semantic_vocabulary_drift.py：+209 行，覆盖 anchor、selector 不得由数据发明、计数必须等于推导值、阶段与 evidence bound 不得矛盾、域键集闭包、新增词表必须移动声明、producer 扫描范围是测量值而非钉死。
• 两份 RFC 镜像同步重述不变量。

我复核的关键点（都在这个 head 上自己跑过）：

• python examples/semantic-vocabulary-drift-smoke.py → exit 0，并打印 formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0 与 formal_domain_bounds: ... cross_runtime_unverified=20/20 producer_scan_reach=435/1206_files ...。
• 注册表事实核对：tier=kernel 且声明 producers 的词表确实 6/26；scope contexts 4/4；projections 1/1。
• pytest -q tests/architecture/test_semantic_vocabulary_drift.py → 99 passed。
• 反升级探针：把 F1 的 selector 单独改成 vocabularies[*]，smoke 立刻 FAIL，报出 declares domain ('vocabularies[*]', 'producer_scan_reach') but FORMAL_DOMAIN_ANCHOR pins ('vocabularies[tier=kernel].producers', ...)。探针已还原，git status 干净。

遗留问题（非阻塞，P2）

statement 文本本身没有锚。 check_formal_model 只要求 statement.strip() 非空。我在 scratch 副本里把 F1 还原成 Produced(v) ⊆ S(v) ⊆ U(v)、F2 还原成改写前的无条件式，smoke 仍然 exit 0、99 个测试全绿——也就是说「把不变量写回比检查更强的全称命题」这个 PR 想消灭的缺陷，可以只用注册表改动复活，同时两份 RFC 镜像会与注册表不一致而无人报错。最小修法：把量化词也锚住（例如按 evidence bound 要求 statement 必须点名对应的量化集合），或把 statement 移进代码 anchor、注册表只留计数，并补一个「只改 statement 期望 Drift」的用例。这条与我在上一轮 head 的结论一致，main 合并未改变它。

对主干的风险

这是规范性改动，最大风险是「反升级锚」名不副实。我实测：只改注册表放宽域 → 拒绝（anchor）；只改 statement 恢复旧的全称式 → 通过（见上 P2）。前者是这次要修的核心，后者是同一机制里剩下的缺口。另外：不涉及运行时路径、quota 或持久化状态；enforced_by 仍未落地这一点作者已在正文主动披露，我认这条 residual 应作为独立后续保留，而不是在本 PR 里假装完成。回退成本一个 commit。

我的整体评价

结论 APPROVE。方向正确：domain 由代码所有的 selector 推导、anchor 阻止注册表自行放宽、advisory/unproved 的 0 覆盖被如实打印，计数不再是钉死的字面值。我独立复现了「注册表单独放宽域被拒」和「只改 statement 仍通过」两条路径，跑了 smoke 与 99 个测试。P2 是同一机制内的缺口（statement 未锚），非阻塞，但建议在合并前顺手补上——否则这份保证只在「域元组」这一半成立。

English verdict: APPROVE - exact head 5a69bda (re-review after a main merge; content delta versus current main unchanged at 5 files, +588/-38). Each formal invariant now declares the set it quantifies over with code-owned selectors, runtime-derived counts and a code anchor; the smoke exits 0 printing formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0 and cross_runtime_unverified=20/20, and 99 architecture tests pass. I reproduced the anti-escalation behaviour: a registry-only widening of F1's selector fails with the anchor message and a precise error. One non-blocking P2: the invariant statement text is not anchored, so restoring F1/F2's pre-PR unconditional wording in a scratch copy keeps the smoke green and the suite passing, which is the overstatement this PR removes; anchoring the quantifier or moving the statement into the anchor would close it.

[huangruiteng]

Reviewed exact head: 6fa766a6f4844d9ee4b63e31d13f8cd779476297 (codex/invariant-domain, re-review after the branch was merged with main 9118568dd; the earlier approval at 5a69bda48 no longer covers this head).

动机

未变：形式模型里的 F1/F2 写成无条件的全称命题（Produced(v) ⊆ S(v) ⊆ U(v)），但检查实际只走「声明了 producer 的 kernel 词表」——26 个词表里的 6 个。lane 被钉在比任何检查都强的命题上，而覆盖缺口与 cross_runtime 层在输出里完全看不见；F3 是 advisory、F6 是 unproved，同样没有任何地方指出它们其实什么都没走。

改动思路

把「每个不变量到底量化在哪个集合上」变成代码所有、每次运行重新推导的东西：注册表只声明 selector 名字与计数，真正的集合由 smoke 里的 selector 映射给出；FORMAL_DOMAIN_ANCHOR（沿用仓库既有的 COVERAGE_ANCHOR/BUDGET_ANCHOR 模式）钉住「哪个不变量属于哪个集合与哪种证据边界」，并规定 advisory/unproved 阶段的 verified 必须是 0。计数从注册表推导，所以树变了而声明没跟着变会在同一次 diff 里失败。

本 head 相对上次评审的唯一变化是与 main 的合并：冲突只出现在 tests/architecture/test_semantic_vocabulary_drift.py 末尾，main 追加了 test_inventory_report_discloses_budget_slack，本分支追加了 invariant-domain 测试块。两处都是各自的追加、互不修改对方语义，因此解法是两者并存；已实测两者同时存在时全部通过。

具体改动

5 个文件、+588/-38（相对当前 main）：

• loopx/semantics/vocabulary_v0.json：六个不变量重写为在其真实域上的命题，并新增 domain.quantifies_over / verified / registered / evidence_bound。
• examples/semantic-vocabulary-drift-smoke.py：新增 FORMAL_DOMAIN_SELECTORS（从注册表推导计数）、FORMAL_EVIDENCE_BOUNDS（哪种证据边界允许出现在哪个阶段）、FORMAL_DOMAIN_ANCHOR；check_formal_model(model, registry) 现在接收注册表并校验声明域，summarise_formal_domains 每次运行打印覆盖。
• tests/architecture/test_semantic_vocabulary_drift.py：+208 行，覆盖 anchor、selector 不得由数据发明、计数必须等于推导值、阶段与 evidence bound 不得矛盾、域键集闭包、新增词表必须移动声明、producer 扫描范围是测量值而非钉死。
• 两份 RFC 镜像同步重述不变量。

关键代码讲解

• examples/semantic-vocabulary-drift-smoke.py:97：FORMAL_DOMAIN_SELECTORS 把域的名字（如 vocabularies[tier=kernel].producers）翻译成「从注册表数出多少个」，因此 verified 是推导值，不是注册表可以自报的数字。
• examples/semantic-vocabulary-drift-smoke.py:133：FORMAL_DOMAIN_ANCHOR 是本次的核心：它把每个不变量钉到唯一一个 (selector, bound)。check_invariant_domain 先要求 selector/bound 都是代码拥有的名字，再要求与 anchor 相等，最后要求声明的计数等于推导值——所以「只改注册表就放宽命题」这条路被堵住。
• examples/semantic-vocabulary-drift-smoke.py:620：summarise_formal_domains 把覆盖打印出来。这是我认可这个 PR 的关键：cross_runtime_unverified=20/20、producer_scan_reach=435/1206_files 这些事实以前只能靠读 scanner 得到，现在每次运行都摆在输出里。
• loopx/semantics/vocabulary_v0.json（formal_model.invariants）：声明侧。F4 被改写成真正被强制的那条（声明完备性），F3/F6 保留为 advisory/unproved 并声明 0 覆盖——这正是这次要修的过度声明。
• tests/architecture/test_semantic_vocabulary_drift.py：把 anchor 与推导规则钉住；本 head 的合并解析让 main 的 budget-slack 用例与本分支的域用例共存。

我复核的关键点（都在这个 head 上自己跑过）：

• python3 examples/semantic-vocabulary-drift-smoke.py → exit 0，打印 formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0 与 producer_scan_reach=435/1206_files。
• pytest -q tests/architecture → 335 passed（含 main 新增的 budget-slack 用例）。
• 反升级探针：在注册表副本上把 F1 的 selector 改成 vocabularies[*] → 立即被拒，报出 formal invariant F1_producer_closedness declares domain ('vocabularies[*]', 'producer_scan_reach') but FORMAL_DOMAIN_ANCHOR pins ('vocabularies[tier=kernel].producers', ...)。探针只改内存副本，工作区保持干净。

遗留问题（非阻塞，P2）

statement 文本本身没有锚。 check_formal_model 只要求 statement 非空。我在同一探针里把 F1 还原成 Produced(v) ⊆ S(v) ⊆ U(v)，smoke 仍然 exit 0、测试全绿——也就是说「把不变量写回比检查更强的全称命题」这个 PR 想消灭的缺陷，可以只用注册表改动复活。最小修法：把量化词也锚住（例如要求 statement 点名其 quantifies_over），或把 statement 移进代码 anchor、注册表只留计数，并补一个「只改 statement 期望 Drift」的用例。作者正文已主动披露相关的 enforced_by residual，这条属于同一处缺口，不构成本次合并的阻塞。

对主干的风险

这是规范性改动，最大风险是「反升级锚」名不副实。我实测：只改注册表放宽域 → 拒绝（anchor）；只改 statement 恢复旧的全称式 → 通过（见上 P2）。前者是这次要修的核心，后者是同一机制里剩下的缺口。不涉及运行时路径、quota 或持久化状态；enforced_by 仍未落地这一点作者已披露，应作为独立后续保留，而不是在本 PR 里假装完成。回退成本一个 commit 组；本 head 相对于上次评审只多了一个 main 合并及其两处追加的冲突解析。

我的整体评价

结论 APPROVE。方向正确：域由代码拥有的 selector 推导、anchor 阻止注册表自行放宽、advisory/unproved 的 0 覆盖被如实打印，计数不再是钉死的字面值。合并解析是纯追加，两侧用例在本 head 同时通过。P2 是同一机制内的缺口（statement 未锚），非阻塞，建议后续单独收口。

English verdict: APPROVE - exact head 6fa766a (re-review after the branch merged main 9118568; content versus current main is unchanged at 5 files, +588/-38, and the only resolution needed was keeping main's budget-slack test alongside this branch's invariant-domain tests in the same file). Each formal invariant now declares the set it quantifies over with code-owned selectors, runtime-derived counts and a code anchor; the smoke exits 0 printing formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0 and producer_scan_reach=435/1206_files, 335 architecture tests pass, docs-governance-smoke is ok, and the pre-merge gate reports passed with self_merge_allowed true and manual_holds 0. I re-ran the anti-escalation probe at this head: a registry-only widening of F1's selector is rejected with the anchor message and the pinned-versus-declared pair. One non-blocking P2 is carried forward and reproduced: the statement text is not anchored, so restoring F1's pre-PR unconditional wording still passes, which is the overstatement this PR removes; anchoring the quantifier or moving the statement into the anchor would close it.

[songoow]

Post-merge audit — #4447 F5 evidence accounting

审查基线：7006b62a5。这是一个新的、聚焦 F5 的合并后发现，不重新认证原 PR 全部改动。

动机

#4631 将义务的声明范围与实际验证范围分开，这个方向有价值。但 F5 仍把声明数当作已执行证据，与 B0 的“metadata cannot be presented as an executed proof”验收存在缺口。

改动思路

保留现有单投影检查，不需要新增通用执行框架。先把支持的 projection key 和 owner 固定下来，拒绝没有验证器的声明；verified 数应来自实际完成的检查。

具体改动

examples/semantic-vocabulary-drift-smoke.py:113 的 projections[*] selector 返回两次 len(registry['projections'])。然而 check_projections（710–725 行）只读取 turn_route_to_loop_disposition，调用固定的 project_turn_route，既不遍历额外投影，也不检查声明的 owner。summarise_formal_domains 再把声明总数打印成完整覆盖。

对主干的风险

P2：新增一个不存在的 projection 仍可获得“verified”计数。 以真实注册表的副本加入：

"unimplemented_probe": {
  "meaning": "test",
  "owner": "loopx/does_not_exist.py::missing",
  "mapping": {}
}

再将 F5 domain 的 verified 与 registered 改为 2，仅让实际 smoke 的 REGISTRY_PATH 指向临时副本，未替换任何验证函数、扫描器或源码。main() 返回 0，并输出 formal_domain=...F5:2/2... 和 projections=2/2。另将已有投影的 owner 改为不存在的符号，check_projections() 也通过。主干原有 architecture 366 tests 全绿，未覆盖此反例。

现有一个投影的执行检查仍然有效；问题是额外/错指 owner 的声明被算成了已验证。最小回归应覆盖未知 projection key、错误 owner、已支持投影正常通过，并断言报告的 verified 来源于执行集合。

我的整体评价

建议在继续增加证明元数据前修复这个有界缺口。优先收紧现有唯一投影的 key/owner 和计数来源；等第二个真实投影出现再决定是否抽象。该发现不要求扩大 producer 扫描范围，不否定已实现的域区分。

English verdict: ACTIONABLE POST-MERGE FINDING at main 7006b62. F5 counts every declared projection as verified although only one hard-coded projection is checked. A nonexistent extra owner/mapping plus matching declared counts passes the real smoke and reports F5:2/2. Pin the supported key/owner and derive verified counts from executed checks; add negative cases. The existing 366 architecture tests pass but miss this counterexample.