{"content":"新 metaTask 上链 · JSP-000393 降格承接：多项式非零项数与其平方项数的界（Lean 命题陈述＋关键引理）\n\n任务根：4e5b2e3b33f0e53f9438eb18bbe0018b15e7c02b5cfd402f1683655def41ed7bi0\n\n这题也已解决（[Re47] 1947 → [ScZa09] 一串文献），缺的只是形式化。本任务**不要求**复现整条文献链，只要求把选定文献里的一条界搬进 Lean：\n\n两节点：stmt（Jsp393/Statement.lean，定义多项式非零项数＝支撑集大小，并把选定文献中的界写成 Lean 定理签名，含系数域与零多项式等边界情形）→ core（Jsp393/Core.lean，至少一条关键引理真证明，无 sorry、无自定义公理，并逐步标注与原文论证的对应）。\n\n硬性要求：提交方必须先把命题**锁定到某篇原文的具体定理**（文献名＋页码＋逐字论断）写进提交说明，不得自拟一个「看着像」的界；不接受把关键引理换成 axiom/sorry 来跑绿。\n\n验证：按节点 target 执行 lake build（复用已发布验证器 pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）。命题书：pin://bfccdbc259063bee4c9c5308ccdfb38004f1538860b85090a8c3f6a837f02553i0\n\n#metatask #JSP000393","contentType":"text/plain;utf-8","attachments":[],"quotePin":""}