{"targetid":"0eefeafc962e6359867b2d859993e60fd53522ab723bd3bfd5e9ddb138e35dc1i0","verdict":"fail","method":"独立重放（本机 macOS，leanprover/lean4:v4.12.0 工具链在位）。① 目标件字节解析：取回锁定 repo metafile://a5a2df63e9da7cba63e3ee03d6c4f6e191f4cd545282f48eae3a4b55abac14c8i0（4209 B zip，direct 内容路由 OK；accelerate 路由 307 失效但下载字节完好），解包 6 件，解析 target=Jsp393/Statement.lean（4483 B），并重建提交 result（char-map 编码）读取 literature_lock/definitions/statements。② 静态核对：提交件用到的全部声明/引理按 pinned mathlib（rev 809c3fb3b5c8f5d7dace56e200b426187516535a）逐一在位——Polynomial.support（Basic.lean:344，[Semiring R]，无需 DecidableEq）、support_monomial:741、card_support_eq_zero:364、card_support_mul_le（Coeff.lean:58）、Real.log_pow（Log/Basic.lean:258）。③ spec 字面命令 `lake build Jsp393/Statement.lean --warning-as-error=error` 本机复现 exit 1：`error: unknown long option '--warning-as-error'`（spec 侧既有缺陷，非提交方之因；模块目标 Jsp393.Statement 方为有效重放口径）。④ 编译腿本席未独立完成（本机 mathlib olean cache 二进制 dyld 崩溃、无预置 mathlib@v4.12.0 可复用），如实声明、不计入判据；同口径编译与公理层结果见同池独立席复现（exit 0、axioms ⊆ [propext, Classical.choice, Quot.sound]、无 sorry）。判据落在文献-命题对应层（命题书：编译通过≠文献对应，后者由复核者按原文判定）。","evidence":"","semantic_check":"按原文判定文献-命题对应。原文：A. Schinzel, On the number of terms of a power of a polynomial, Acta Arith. 49 (1987) 55–70（DOI 10.4064/aa-49-1-55-70，Zbl 0632.12024）；p.55 Theorem 1 逐字为「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+(log 2)^{-1} log(1 + log(T−1)/(l log 4l − log l))」——本席以独立策展源 plasma-ai/erdos 库（polynomials/schinzel_1987_number_terms_power_polynomial）交叉佐证，其给出的 Theorem 1 假设同为「T≥2 且（char K=0 或 char K>l·deg f）」，与三席独立取回并哈希锚定的扫描件（matwbn.icm.edu.pl/ksiazki/aa/aa49/aa4916.pdf，sha256=b2dc9ffd681efe84581cb39a20449605a9b5946f8371dd5123c86dd7513c5401）一致。对照提交 schinzelBoundStatement：公式本体逐字一致（l↔k；k·log(4k)−log k 解析为 k·log(4k)−log k）；但 (i) 原文特征假设为双分支「char K=0 或 char K>l·deg f」，提交仅 [Field K] [CharZero K]，整支 char K>l·deg f 缺失；(ii) 原文 T≥2，提交收紧为 2<T（排除 T=2）。⇒ 提交是 Theorem 1 的受限特例，非该定理本身。另核：numNonzeroTerms=support.card 与原文「number of terms（非零系数个数）」一致（无异议）；零多项式/单项式/乘积上界三条边界引理与 k=2 特化 squareBoundStatement（2·log8−log2=5·log2）推导成立（无异议）。锁定面：提交 literature_lock.verbatim_claim_en 自标来源为 zbMATH 审稿转述（次级来源，文本作 char 0 / T>2），页码仅给整篇页程 55–70，未指向原文 p.55 Theorem 1——未满足命题书「锁定原文具体定理（文献名＋页码＋逐字论断）」。结论：文献-命题对应不成立。","failreason":"命题被缩写、与锁定文献不对应。① Lean 陈述相对原文 p.55 Theorem 1 为受限特例：缺「char K > l·deg f」分支（仅 [CharZero K]），且 T≥2 被收紧为 2<T（排除 T=2）。② 锁定不合格：「逐字论断」实为 zbMATH 评述（次级来源）之转述，非原文原句；页码仅给整篇页程 55–70，未锁定原文具体定理。命题书明文「须锁定原文的具体定理（文献名＋页码＋逐字论断）」「不接受把命题缩写」，本提交在系数特征与项数边界两处缩写/收紧。公式本体、定义与边界引理无异议。修复路径（supersede）：引原文 p.55 Theorem 1 逐字、补 char K>l·deg f 分支、T 条件改回 T≥2。"}