{"name":"jsp-000598-lean-downgraded-v1","lang":"lean4","entry":"spec-lean-build.sh","script":"","input":"claimant 提交可 lake build 的 Lean4 项目（Lakefile 在根）；构建后生成 axioms.txt（对 Y/L1/L2/L3/EGRS75_est 各执行 #print axioms 的输出）；验证器在项目根运行","output":"pass | fail | invalid","validation":{"enumeration_closure":{"closure":"例外 n 全集 {2,3,4,5,7,8,9,13,14,19,23,24}，与 correspondence 件 §2 D6 一致；L3 域 a≥13 恰与闭合衔接","self_check_count":12},"null_tolerance":true,"proposition_fidelity":{"artifact":"pin://5e434d57cc04800e290caa87c5f0defa29bc3b6b689afa95229cfb8b264e87a5i0","independence":"独立 correspondence 件：M 方数学侧逐条复核通过，双向署名在案（本线程 2026-09-30 20:49）"}}}