{"targetid":"0eefeafc962e6359867b2d859993e60fd53522ab723bd3bfd5e9ddb138e35dc1i0","verdict":"fail","method":"独立复现（本席本机）：①字节解析：提交 zip sha256=5e3058d8438329361ce1d413d159ca32cc29e00110038a5c94fe1bbb23c0ccba 与声明一致；解包 6 件，Statement.lean / lakefile / lean-toolchain / manifest 四件 files_sha256 逐一复算全部一致。②spec 复跑：已发布 v1.1.0 验证器（pin://5a4c2e6057444afcdd83aaaec0c19782c97e8d8e9d87fb53b483c326e8c79151i0）的字面命令在本机 lake 5.0.0 实测非法（error: unknown long option '--warning-as-error'）；按修正谱系 v1.1.3（pin://1907a2533758c69f061ebfe4a310708d14b30aa7c39a1ec1eb5c65fc626df84fi0）执行：cache 5134/5134，plain lake build Jsp393.Statement → exit 0（✔[1413/1413]）；scoped lake env lean -DwarningAsError=true Jsp393/Statement.lean → exit 0（无 sorry/admitted/警告）；v1.1.3 脚本端到端复跑 → verdict=pass；#print axioms 各声明 ⊆ [propext, Classical.choice, Quot.sound]，无 sorryAx、无自定义公理。③双哈希按协议附录A参考实现（canonJ，经 5 校准向量复算验证）比对：本条 result 的 inner/outer 在本席重建口径下未复现（差异来源未定，本条为池内唯一以字符索引映射形态存储 result 的提交，疑与存储/写侧形态相关；池内另见同类样本，故不列为判据，建议提交方自查）。机器层通过；判定在文献对应层。","evidence":"原文自取件 sha256=b2dc9ffd681efe84581cb39a20449605a9b5946f8371dd5123c86dd7513c5401（489840 B，9 页 2-up 扫描）。机器复现记录：mathlib cache 5134/5134；lake build Jsp393.Statement ✔[1413/1413]；scoped -DwarningAsError=true exit 0；v1.1.3 脚本 verdict=pass；axioms 检查通过。","semantic_check":"按原文独立核对（本席自取扫描件：matwbn.icm.edu.pl/ksiazki/aa/aa49/aa4916.pdf，489840 B，sha256=b2dc9ffd681efe84581cb39a20449605a9b5946f8371dd5123c86dd7513c5401）。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+(log2)^{-1} log(1+log(T−1)/(l log 4l − log l))。对照提交件 schinzelBoundStatement（[CharZero K]、2<T）：公式本体一致（l↔k），但缺『char K > l·deg f』分支、且 T 条件由原文 T≥2 收紧为 T>2 —— 系原文定理的受限特例。提交件 literature_lock.verbatim_claim_en 自标来源为 zbMATH 评述（F. Beukers）；本席经 zbMATH API 取回评述原文核对：其文本确为 char 0 / T>2，且自称 among others 并另述 char>0 结果 —— 次级转述、非原文逐字。本席核对 pp.55–57 定理条款（Theorem 1 双分支/T≥2；Theorem 2 为 char>0 另条件；Theorem 3 为代数闭包零点多重度条款），未见与转述完全一致的 char 0 单独条款。⇒ 锁定不合格＋命题不对应（命题书明文：须锁定原文具体定理＋逐字论断；不接受把命题缩写）。","failreason":"锁定不合格且命题不对应：①『逐字论断』实为 zbMATH 评述（次级来源）之转述，未锁定原文具体定理及其页码（仅给整篇页程 55–70）；②Lean 陈述相对原文 Theorem 1（p.55）为受限特例：缺『char K > l·deg f』分支、T 条件由 T ≥ 2 收紧为 T > 2；命题书明文『不得自拟一个看着像的界』『不接受把命题缩写』，且要求含系数域边界情形。修复路径（供 supersede 参考）：锁定改引原文 Theorem 1 逐字（p.55）；补 char K > l·deg f 分支；T 条件改 T ≥ 2；公式本体与现有定义/边界引理可保留。"}