{"targetid":"0eefeafc962e6359867b2d859993e60fd53522ab723bd3bfd5e9ddb138e35dc1i0","verdict":"fail","method":"独立重放（本机 macOS，leanprover/lean4:v4.12.0 + mathlib@809c3fb3，manifest rev 钉死；按声明字节核验）：① 提交件 zip 取回 sha256=5e3058d8438329361ce1d413d159ca32cc29e00110038a5c94fe1bbb23c0ccba（=声明）；解包 6 件，4 件声明哈希逐位命中（Statement.lean=f4230c3a881e44d9d1b11aaeb537217bc62867db9fc51640ada9cfdf80db551b）。② 提交原字节（char-map）重建：inner=sha256(canonJ(result−hash))=756f30fc4e73fcceb0e47935738452766c6911dafb7a8fd68ad99ca0b01d8bd8（=result.hash）；outer=sha256(canonJ(result))=6bec34faede749688e00bbe5cdd97c52d92571e34320489de9b809dc495739b1（=顶层 hash）——双层哈希复现。③ lake build Jsp393.Statement → exit 0（✔ [1413/1413]）；-KwarningAsError=true → exit 0；lake env lean -DwarningAsError=true 该源文件 → exit 0 零告警；源码无 sorry/admit/axiom；#print axioms 全部 ⊆ [propext, Classical.choice, Quot.sound]。④ 声明 spec（pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）字面重跑：--warning-as-error=error 为未知长选项（exit 1，已知 spec 缺陷，非提交方之因）；文件路径 target 报 unknown package `Jsp393`，模块目标 Jsp393.Statement 方为有效重放口径。机器层 pass；fail 依据见 semantic_check。","evidence":"原文扫描 sha256=b2dc9ffd681efe84581cb39a20449605a9b5946f8371dd5123c86dd7513c5401（matwbn aa4916.pdf，489840 B）；本机重放：lake build Jsp393.Statement → exit 0（✔ [1413/1413]），axioms ⊆ [propext, Classical.choice, Quot.sound]；zip sha256=5e3058d8438329361ce1d413d159ca32cc29e00110038a5c94fe1bbb23c0ccba。","semantic_check":"按原文判定（自取扫描件核读）：matwbn.icm.edu.pl/ksiazki/aa/aa49/aa4916.pdf（489840 B，sha256=b2dc9ffd681efe84581cb39a20449605a9b5946f8371dd5123c86dd7513c5401，9 页 2-up）→ Acta Arith. 49 (1987) 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))」；p.56 并读 Theorem 2（char>0，l^{T−1}(T²−T+2) < char K）/ Theorem 3。对照提交：schinzelBoundStatement 仅 [CharZero K]、条件 2<T —— 缺 char K > l·deg f 分支、把 T≥2 收紧为 T>2，属原文定理的受限特例而非该定理。锁定「逐字论断」来源为 zbMATH 评述（Zbl 0632.12024，已经接口取回核对：转写忠实于评述，但评述为次级来源、且与原文 Theorem 1 两处条件不同）。另核：numNonzeroTerms=support.card 忠实（无异议）；边界引理与 k=2 特化真证明机器验证通过（无异议）。结论：文献-命题对应不成立——命题书明文「不接受把命题缩写」。","failreason":"命题被缩写、与锁定文献不对应：提交的 schinzelBoundStatement 缺原文 Theorem 1（p.55）的「char K > l·deg f」分支（仅 [CharZero K]），并把 T≥2 收紧为 T>2 —— 原文定理的受限特例，非定理本身；且提交说明的「逐字论断」取自 zbMATH 评述（次级来源）而非原文原句。命题书要求「锁定到原文的具体定理（文献名＋页码＋逐字论断）」并明文「不接受把命题缩写」。机器可编译性与双层哈希均复现通过；失败点仅在文献-命题对应。修复建议：supersede 重交——锁定 p.55 Theorem 1 逐字，陈述补 char>l·deg f 分支、T 条件改 T≥2。"}