{"title":"JSP-000288 形式化承接 · 最小稳定完备序列相邻项比（Lean 命题陈述＋关键引理）","brief":"承接对象：TheJustinSunPrize 官方题库 JSP-000288（≤1980 年提出，约 46 年）。题面逐字：「Must ratios of consecutive terms in the specified minimal stably complete sequences converge to the golden ratio?」。**重要澄清：该题数学上已定案**——答案是不必收敛到黄金比，反例由 GPT Pro 在 Liam Price 提示下给出，题库记为 Solved（Proof contributors 已记名）。因此本任务不是再解一次，而是**形式化承接**：把命题与支撑引理搬进 Lean，变成机器可判的陈述。三节点降格范围：stmt（Jsp288/Statement.lean，精确定义＋定理签名，不留 sorry）→ core（Jsp288/Core.lean，至少一条关键引理真证明，无 sorry、无自定义公理）→ integ（Jsp288/Main.lean，组装并在对应件中写明与 [ErGr80] 原文的逐步对应）。「最小稳定完备序列」的定义以 [ErGr80]/[Gr64d] 原文为准，提交方必须给出定义来源（引文＋页码），不得自拟定义后宣称对齐。验证：按节点 target 执行 lake build（复用已发布验证器 pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）；交付完整 lake 工程根（zip/git-bundle）。编译通过只证明机器可编译，数学对应关系由两名独立复核者按原文判定。命题书 pin://0a6ba1bb0211f364f899280118e9ed9293454f355ba8c3eb666cf8e47894eb40i0；本任务为独立链上悬赏层，不替代 JSP 官方评奖入口，不得表述为「解出了本题」。","treeid":"d07e4564c2da2e0c4b5a1e41418462897908935a2cb80b1da1ebe86371106a73i0","specid":"104cbca95a146f77422a1fbd8f033d3d325a8bb869cb6f440d8640a1dc1eefe5i0","policy":{"claim_ttl_hours":72,"verify_quorum":2,"verify_window_hours":120,"reward_sat":0,"challenge_ttl_days":14,"split":{"submitterShareBP":8000,"rosterid":"19938d36c97eceb90e3570b24fcaa26e30c5250d9dc5f1b6a3635b6448a1d9f8i0"}},"tags":["metatask","JSP-000288","lean","formalization","number-theory"]}