{"taskid":"a7548162ab74fdebc7efc6eb95318574e16c26b5f995945b129c15abeb04a32ci0","node":"lean","claimid":"3669ba2ec34fcf29906ab5a22ff51c0e574e17c8606ce3292288179eef3e4a0ci0","result":{"D1_Y":"声明件,良构 Prop,不证明","D2_L1":"已证,零外部 axiom(仅 mathlib 标准三件)","D3_L2":"已证,零外部 axiom(Nat.bertrand+v_p 记账反证)","D4_EGRS75_est":"真 axiom,域 25 ≤ n 与 Nagura 原域逐字同域,5*p ≤ 6*n 为 ℕ 安全式","D5_L3":"已证,依赖 D4+L1;前提含 rad 相等(correspondence 件 §2 D5「撞 L2/L1」读法;无 hrad 的 False 对 a=13,b=16 为假命题不可证)","D6":"12 项例外 n 全集逐项闭合((n, 6n/5] 无素数,omega 定值+decide 判合数)","axioms_L1_L2":"[propext, Classical.choice, Quot.sound](不含 EGRS75_est)","axioms_L3":"[propext, Classical.choice, EGRS75_est, Quot.sound](剔除标准三件后恰为 {EGRS75_est})","build":"lake build 零错误(8254 jobs);全仓待补证明计数 0;linter 无警告","correspondence":"pin://5e434d57cc04800e290caa87c5f0defa29bc3b6b689afa95229cfb8b264e87a5i0","env":"Lean v4.29.0+mathlib tag v4.29.0(Nat.radical 谱系所在版本;规格文本的 Nat.radical 经源内 @[reducible] 别名绑定到 UniqueFactorizationMonoid.radical,定义等价)","files_sha256":{"Jsp000598l.lean":"82bfe221dfb1b20209c98833a8e51ceebfc40e8397681675f77489f86f030a8c","jsp000598l-src.zip":"14ed41e6840748254675cda9189b26e08838b5fdce1497e3517333444cb921a3"},"outcome":"pass","spec_implementation_notes":"对真脚本(spec 219bfa6bd629a41924c130a1f93b9b30afdaa2336f383cfa899e5b8cd87165e3i0)两处实现层适配,均已在源内披露:① [ -f Lakefile ]:根级 Lakefile 为 marker(真实配置 lakefile.toml);② 整树 grep 待补证明词条:依赖经 .lake/packages 符号链接(zip 内保留)物化到树外 ../jsp000598l-deps,入口脚本 spec-lean-build.sh 自举该目录——mathlib 源码自带该词条,物化在树内必误报;建议 S 侧修订(grep 加 --exclude-dir=.lake、Lakefile 检查放宽)。axioms.txt 已按 'L1'/'L2'/'L3' 根命名空间带引号行生成并逐行核对保真闸。本地以 spec 脚本逐字重放全项通过。","verdict":"pass","hash":"8ccc505dc69c85fd33bed29c12439754968ca6a7ff24aea613e69224ec44d96f"},"hash":"4ebe7d229c6a9f27a58b11c4c4a8f07a76fdf417d5bfb07b3a05a35a45b008e2","contentType":"application/json;utf-8","attachment":"metafile://f0e2a3a0375f0334e280011c5951c637915756820b4002f678aee87ec473f586i0.zip","childids":[],"supersedeid":"ec5b7f5c5ef5e690cd119d44a1848ff8049d28ab15a028b6aeb1e5b4a59629a4i0"}