{"title":"JSP-000393 降格承接 · 多项式非零项数与其平方项数的界（Lean 命题陈述＋关键引理）","brief":"承接对象：TheJustinSunPrize 官方题库 JSP-000393（≤1961 年提出）。题面逐字：「What bounds relate the number of nonzero terms of a polynomial to that of its square?」。**重要澄清：该题已解决**（[Re47] Hungarica Acta Math. 30-34；[Er49b] Nieuw Arch. Wiskunde 63-65；[Sc87] Acta Arith. 55-70；[ScZa09]），缺的只是形式化。本任务是**降格承接**：不要求形式化整条文献链，只要求把选定文献里的一条界搬进 Lean。两节点：stmt（Jsp393/Statement.lean，定义多项式非零项数＝支撑集大小，并把选定文献中的界写成 Lean 定理签名，含系数域与零多项式等边界情形）→ core（Jsp393/Core.lean，至少一条关键引理真证明，无 sorry、无自定义公理，并在对应件里逐步标注与原文论证的对应）。硬性要求：提交方必须先把要形式化的命题**锁定到某篇原文的具体定理**（文献名＋页码＋逐字论断）写进提交说明，不得自拟一个「看着像」的界；不接受把命题缩写或把关键引理换成 axiom/sorry 来跑绿。验证：按节点 target 执行 lake build（复用已发布验证器 pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）；交付完整 lake 工程根。编译通过只证明机器可编译，文献对应关系由两名独立复核者判定。命题书 pin://bfccdbc259063bee4c9c5308ccdfb38004f1538860b85090a8c3f6a837f02553i0；本任务为独立链上悬赏层，不替代 JSP 官方评奖入口，不得表述为「解决了本题」。","treeid":"9de9f1fe8474a653b8a09bf01e6ad645e7927b61958ed77f258ab313751e0773i0","specid":"434549d78a2ef5fa8c93d16317d53dd75c039b05a0bf12c407b56df249db156ei0","policy":{"claim_ttl_hours":72,"verify_quorum":2,"verify_window_hours":120,"reward_sat":0,"challenge_ttl_days":14,"split":{"submitterShareBP":8000,"rosterid":"2f53a3072626419698d91f466210f809368252db6a0fd61f42a10c87d5e2901ei0"}},"tags":["metatask","JSP-000393","lean","formalization","polynomials"]}