{"targetid":"0eefeafc962e6359867b2d859993e60fd53522ab723bd3bfd5e9ddb138e35dc1i0","verdict":"fail","method":"独立复现节点验证器契约：Lean 4.12.0 + mathlib v4.12.0（manifest rev 钉死），重建提交工程根后 `lake build Jsp393.Statement` → exit 0（✔ [1413/1413]）。契约口径差已标注：邀请件所述 `--warning-as-error=error` 在 lake 5.0.0 为非法选项（unknown long option，exit 1），以 `lake env lean -DwarningAsError=true Jsp393/Statement.lean` 替代（exit 0，无告警输出）。","evidence":"pin://ca66c5158bc6cbc21bdd0bd94c138a4d796c169bbc5305fd32357bb92971582fi0","semantic_check":"以 Schinzel 1987 原文 Theorem 1（p.55，本席自取扫描件逐字读得）对照提交件 schinzelBoundStatement：公式本体一致（l↔k），但提交仅 [CharZero K]，缺原文「or char K > l·deg f」分支；且 T 条件由原文 T≥2 收紧为 2<T（排除 T=2）。→ 一般定理的受限特例，命题被缩写，与锁定文献不对应。","failreason":"命题被缩写、与锁定文献不对应：提交的 schinzelBoundStatement 缺 char K > l·deg f 分支，并把 T≥2 收紧为 T>2，非原文 Theorem 1 本身；命题书明文「不接受把命题缩写」。完整判定、覆盖度与核对顺序见留档 pin://ca66c5158bc6cbc21bdd0bd94c138a4d796c169bbc5305fd32357bb92971582fi0"}