09 多数派交叉与单值 Paxos：论断—证据—核验记录
核验日期：2026-09-19；状态 VERIFIED_SOURCE / VERIFIED_LOCAL_MODEL 分开。

来源：
S1 Leslie Lamport, Paxos Made Simple；PDF2001-11-01，SIGACT News32(4), December2001, pp51–58。
https://lamport.azurewebsites.net/pubs/paxos-simple.pdf
§2.1模型；§2.2 P2b/P2c、phase1/phase2；§2.3学习；§2.4进展；§2.5持久性与唯一编号。

S2 Leslie Lamport, The Part-Time Parliament；TOCS16(2), May1998，作者托管修订PDF。
https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf
§2.1 B1/B2/B3、Lemma、Theorem1；§2.2唯一编号；§2.3 Basic Protocol精确持久字段/动作；附录。
印刷版与PDF版本不混称；使用作者PDF已有修订说明，不宣称读的是未修改原始排印文件。

S3 MIT6.5840 Spring2026课程；网页滚动，访问2026-09-19。
https://pdos.csail.mit.edu/6.824/schedule.html
https://pdos.csail.mit.edu/6.824/notes/l-paxos.txt
https://pdos.csail.mit.edu/6.824/notes/paxos-code.html
精确伪代码的Prepare n>n_p；Accept n>=n_p，成功更新n_p、n_a、v_a；字段持久。

S4 作者出版目录Paxos Made Simple项，所述事件发生2015；说明段无单列发布日期。
https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simple
作者记录歧义误读，未公开定位具体句子；不能当作Paxos安全性被推翻。

论断 / 支持 / 核验状态：
1. accepted、chosen、learned分层；历史chosen不可被当前状态覆盖撤销 / S1§2.2–2.3 + S3 / 已独立交叉核对；实验accepted情景实际复现chosen但learner未知。
2. 每轮全局唯一且只发一个值 / S1§2.5 + S2§2.2 / 已核；实验由固定合法调度器保证，非拜占庭校验器。
3. phase1 quorum按最高accepted取值，不能最高promise或最多同值 / S1 P2c + S2 B3 + S3 / 已核；max变异实际产生历史X/Y多数派。
4. quorum交叉之外还需promise、选值、唯一编号和状态保持 / S1/S2/S3 / 已核；归纳明确涵盖高轮phase1先完成、低轮后来补齐多数派。
5. promise与accepted均需跨崩溃保存、成功回复前持久化 / S1§2.5 + S2§2.3 + S3 / 已核；只做内存字段丢失反例，未测真实磁盘或崩溃。
6. 正确进展需要额外竞争收敛/通信条件 / S1§2.4 + S2§2.4 / 已核；有限运行不证明无界活性。
7. 算法变体不能混拼 / S2严格guard与发送集合 + S3宽松guard/accept提升promise / 已核；main.go完整采用S3。

独立核验：主代理实际重新读取S1§2/3、S2修订版§2.3与附录、S3精确伪码、S4，并完整审阅main.go；独立默认go run及go vet成功。

辅助规格边界：研究时已读取TLA+ Examples Paxos.tla滚动master，未取得已核验SHA；无认证GitHub API查询HTTP403，不更换认证。未执行TLC/TLAPS。正文不将它当固定版本证明。

反向检索：Paxos Made Simple errata/ambiguity等查询找到作者2015说明；未把非作者猜测当具体正式勘误。完整资料定位与反例设计见writing-plans/distributed-systems/research/09-paxos.md。

文章关系：已有2026-06-21共识综合文，但本次用户已指定系列09新篇；保留旧文，不覆盖。封面搜索查得Unsplash候选，各图片许可不同不能统称CC0；本篇使用已存在系列自有SVG，无外图引入。

写作流程：实际读取blog-editor及其workflow/cover-search。临时稿/tmp/paxos09-draft.md先执行anti-ai-tone（tech profile脚本0错误0提醒，人工支撑/推进/节奏/连续性复核），后执行anti-persona-fabrication（全文词扫描0命中，人工三红线复核），之后才允许正文落盘。

最终复核：本轮再次实际打开MIT paxos-code.html，工具行20–23为Prepare n>n_p，28–33为Accept n>=n_p且更新n_p/n_a/v_a，与所选变体一致。父级-race默认运行也成功；不外推为并发生产实现验证。

图示增补（2026-09-19）：实际读取blog-illustrator。Mermaid三图：1 accepted/chosen/learned及丢回复分支，依据S1§2.2–2.3；2 A/B成功消息时序，proposer与learner合并，依据S3完整MIT变体，成功回复前持久化；3 最高/最低accepted对照，依据已运行max正常与变异历史，t5为B新票+C历史票。图中chosen与learned时点分开，无新增实验结果。配置已核mermaid.enable=true、code_write=true；只做图源与语义检查，最终浏览器渲染由主代理验收。临时完整稿先anti-ai-tone tech（0错误0提醒）后anti-persona-fabrication（词扫描0命中及人工三红线），再落盘；落盘前比对源文件未被并发修改，保留既有引用空行。