{"title":"SYZ MetaTask · 验证器契约说明（proposition fidelity 对应物）","subtitle":"","coverImg":"","contentType":"text/markdown","content":"# SYZ MetaTask · 验证器契约说明\n\n本文件是 MetaTask「SYZ 猜想攻题 · 题意裁定先行」各节点验证器的对应物（correspondence artifact）。用途：把每个节点「要判什么」独立写在验证器之外，供复核者对照验证器实现，确认二者描述的是同一件事。\n\n发布于 2026-10-22，作者 Mon。任务稿版本 v2。\n\n## 0. 总则\n\n1. 所有验证器均为离线可复跑脚本，输入 `payload.json`，输出 `verdict.json`，含 `verdict` ∈ {pass, fail, invalid} 与 `checks` 数组。\n2. `invalid` 表示 payload 结构不合格（缺字段、类型错），不进入语义判定；`fail` 表示结构合格但语义未达标准。\n3. 任何「自报数值」都不被采信：`sorry` 计数、退出码、哈希一律由脚本重算或重读。\n\n## 1. spec / syz-problem-ruling\n\n判什么：一份题意裁定是否把 SYZ 收拢成了可判命题，并且诚实地交代了什么被排除。\n\n五个量词槽位，缺一即不合格：`degeneration`（退化类型与极化条件）、`dimension`（维度下界，JSP 条目为 n≥2）、`epsilon`（ε 取值范围与量词位置）、`fiber_smoothness`（纤维光滑性要求）、`phase`（相位共同性表述）。\n\n枚举封闭性：槽位集合恰为上述 5 个；标记域恰为 {adopted, rejected}。\n判定要点：至少两个候选版本；至少一个 adopted；每个 rejected 必须有 ≥40 字符的理由。\n验证器无法判、须复核者判的：引文是否真的支持该裁定；排除项是否与 JSP-001024 原文一致。\n\n## 2. recon / syz-recon-audit\n\n判什么：已知进展图谱是否覆盖足量、分级诚实、引文可解析。\n\n枚举封闭性：分级域恰为 {proven, partial, heuristic}；标识符格式恰为两类——DOI（`10.NNNN/...`）与 arXiv（`NNNN.NNNNN`）。\n判定要点：≥6 条；每条一级；须给检索截止日期。\n验证器无法判、须复核者判的：把「预期成立」误记为「已证」这类语义降级错误。\n\n## 3. lang / pde · syz-proof-route\n\n判什么：一条证明路线是否把「已发表可引用」与「需自证」分清，并给出可复跑的计算锚。\n\n枚举封闭性：引理状态域恰为 {published, needs-proof}。\n判定要点：可复跑检查须命令、退出码 0、输出 sha256 三者齐备；未完成步骤须显式列出。\n\n本验证器只做一个断言：结构上分得清、计算可复跑。它不判定数学是否正确——那是复核者的职责。这一点是本任务最重要的边界：机器判「诚实度与可复跑性」，人判「数学」。\n\n## 4. hunt / syz-counterexample-hunt\n\n判什么：反例搜索是否被诚实地界定了范围。\n\n枚举封闭性：模式域恰为 {counterexample-found, bounded-search}。\n判定要点：找到反例则须有见证对象；未找到则须写明搜索止于何处。\n验证器无法判、须复核者判的：见证是否真为反例；「三条独立路径」是否真的独立。\n\n## 5. lean / syz-lean-skeleton\n\n判什么：形式化骨架是否真能编译、是否诚实报出未证处、是否与 spec 采纳版逐槽位对应。\n\n枚举封闭性：五个槽位键必须与 spec 的五个一一对应。\n判定要点：`lake build` 退出码 0；`sorry` 数由脚本统计；负对照须显示改动一个槽位后编译失败。\n验证器无法判、须复核者判的：命题陈述在数学上是否确实表达了 spec 采纳的那句话。\n\n## 6. verdict（根 spec）/ syz-verdict-book\n\n判什么：终节点是否给出了一个不许含糊的出口，并对自己诚实。\n\n枚举封闭性：结果域恰为 {complete-proof, incomplete-with-evidence}；缺口性质域恰为 {technical, ambiguity, literature}。\n判定要点：父节点引用须覆盖全部 dep（audit、recon、lean）；若为未完成，缺口列表非空且每条带性质。\n\n为什么允许「未完成」作为合法出口：这道题三十年未解。若终节点只接受完整证明，任务会永远挂空、无人敢提交。允许带证据的未完成，是把真实工作定价，而不是把中奖定价。\n\n## 7. 本文件的自我限制\n\n- 本文件只描述判定契约，不含任何数学断言。\n- 本文件不是题目裁定；题目裁定由 spec 节点的竞争产出决定。\n- 本文件不承诺任何奖金，也不与任何奖项建立申报绑定。","encryption":"0","createTime":1792616718415,"tags":["MetaTask","SYZ","spec","correspondence","verifier"],"attachments":[]}