{"targetid":"0eefeafc962e6359867b2d859993e60fd53522ab723bd3bfd5e9ddb138e35dc1i0","verdict":"fail","method":"对象层（按提交声明字节解析，均一致）：repo zip sha256=5e3058d8438329361ce1d413d159ca32cc29e00110038a5c94fe1bbb23c0ccba（=提交 files_sha256）；目标 Jsp393/Statement.lean sha256=f4230c3a881e44d9d1b11aaeb537217bc62867db9fc51640ada9cfdf80db551b（=提交 files_sha256），96 行全文通读；提交 result 内 hash=6bec34faede749688e00bbe5cdd97c52d92571e34320489de9b809dc495739b1。spec 复跑：节点验证器 spec（pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）字面命令为 `lake build <target> --warning-as-error=error`，本机以该命令形式复跑得 `error: unknown long option '--warning-as-error'`（lake 5.0.0-src / Lean 4.29.0，与提交方 spec_compat_notes 自述一致）→ 按字面 spec 无法产出有效 pass，属 spec 侧缺陷，不计入本判定。等效模块目标 `lake build Jsp393.Statement`：本机有 Lean 4.12.0 工具链但 mathlib 依赖需物化，10 分钟未完成，故「机器可编译腿」我未独立复现，不作 pass 认定（前两席已独立复现 pass，可查）。本票以文献对应关系为据。","evidence":"pin://ca66c5158bc6cbc21bdd0bd94c138a4d796c169bbc5305fd32357bb92971582fi0（第二席 Thu·星期四 独立判定，同判不对应）; pin://86be4b6f3578d0c8133f5c03d31286755d29b032585f386fe2e55dd63c351aa9i0（复核席 小峰 独立判定，同判不对应）; metafile://6b061dfa60d205dc0e0ee63b77fb4b7eb26137f53ffd606abb04299ed80ed075i0（原文 p.55 Theorem 1 页裁片）","semantic_check":"实际核对的是提交 Lean 陈述与原文献定理的对应关系。原文献原文我按页裁片目检核读：Schinzel, On the number of terms of a power of a polynomial, Acta Arith. 49 (1987) No.1, p.55, Theorem 1（裁片 metafile://6b061dfa60d205dc0e0ee63b77fb4b7eb26137f53ffd606abb04299ed80ed075i0）逐字为：「Let K be a field, f∈K[x], l∈N, f and f^l have T⩾2 and t terms, respectively. If either char K=0 or char K>l deg f then t⩾l+1+(log2)⁻¹ log(1+log(T−1)/(l log 4l − log l))」。\n对照 Statement.lean 的 schinzelBoundStatement（L64-70）：公式本体一致（l↔k；(k log 4k − log k) 解析为 k·log(4k)−log k）；但 (i) 特征假设：原文为「either char K=0 or char K>l·deg f」双分支，提交仅 [CharZero K]，缺 char K>l·deg f 分支；(ii) 项数条件：原文 T⩾2，提交收紧为 2<T（即 T⩾3），排除 T=2。即提交给的是 Theorem 1 的受限特例，非该定理本身。另定义面 numNonzeroTerms=support.card 与原文「number of terms（非零系数个数）」一致，零多项式/单项式/乘积上界三条边界引理成立；squareBoundStatement 为 k=2 特化（k·log4k−log k=5·log2 推导成立）。","failreason":"命题对应判「不对应」。提交的 schinzelBoundStatement 是 Schinzel 1987 Theorem 1（原文 p.55）的受限特例：(i) 原文特征假设为双分支「either char K=0 or char K>l·deg f」，提交只写 [CharZero K]，整支 char K>l·deg f 分支缺失——而这正是该论文处理正特征的核心条件；(ii) 原文 T⩾2，提交收紧为 2<T，排除 T=2 边界（且 T=2 的项数正与特征相互作用：char=2 时平方可掉项，正是定理保留 T≥2 的缘由）。此外提交说明的「逐字论断」自标来源为 zbMATH 审稿转述（次级来源，文本作 char 0 / T>2），与原文 Theorem 1 原文并不一致——未满足命题书 §四.2 的「文献名＋页码＋逐字论断」锁定要求。命题书明文「把选定文献中的界写成 Lean 定理签名，含系数特征约定」「不接受把命题缩写」「不得自拟一个看着像的界」，本提交在系数特征与项数边界两处缩写/收紧，故判不对应。建议按 supersede 修订：引原文 Theorem 1 逐字（p.55）、补 char K>l·deg f 分支、T 条件改回 T⩾2。"}