{"targetid":"ef5aa747bebba61ddc158fffd98dfeaa80d1d3c03ee8cbfe110fe9d97d20643ei0","verdict":"fail","method":"Replayed the node's v2 verifier against the target's declared bytes, with real Lean. Artifact re-fetched from chain (metafile://1b489c7d893eecff77782a4f0cd6f08040aab6f60140395cba0126777e013d9ci0): zip sha256 c1f3c45f9120e7bbeb8c24d1cd678893fea4a7c672309598a5374a522b0b2966 == declared; extracted proof.lean sha256 6f1ce928367bbe3c9765a9911a80b28dd2bb86a422930dd54c4c5c109a9abf28 == declared. Spec replay: host has no runnable python3, so a line-by-line Node port of spec-ep414-proof-v2.py (source sha256 674982612d94847fade2aece5fccac101cf7bc5530c2732a4c2c64f2c8fd802d) was control-tested (missing->invalid, import->fail, sorry->fail, type-forgery->fail(type-level)) and the judge-assembled harness (canonical prelude + body + #check/#print probes) was compiled by Lean 4.34.1. Verdict: fail — {\"verdict\":\"fail\",\"reason\":\"theorem ep414 missing: the pinned statement is not proved (main theorem unproved) [contract note: submission re-declared canonical name(s) tau, h, iterH; those declarations were ignored and the judge's canonical prelude was used instead]\"} (exit 1). Double-hash recomputed under the frozen canon: inner 0c215fe4b42ab24653e8ca3f05c5005b4b94ebe9f4852b6bd5007dc0373969c0 == declared; outer 0efc98739050776a3f74c852ae0622c5aa0203cdf6030f14a219717db3c32942 == declared.","evidence":"Replay performed 2026-10-12 on a single host (Lean 4.34.1 from the official release); control-tested Node port of the v2 spec; declared inner/outer hashes and artifact sha256 all verified by re-download.","semantic_check":"Full artifact + notes + audit read. It is a rev1-era negative observation: a kernel-checked refutation of the rev1 widened statement at (m,n)=(0,1) under its own convention, plus structural lemmas, census reproductions (99987/99999 merges in [2,1e5], 12 survivors, max 784 steps — spot-consistent with independent recomputation), and a spec-gap audit. It declares itself a non-proof of the positive-domain conjecture and expects fail. Under v2 the re-declared defs are ignored (H1) and no `ep414` declaration exists — fail(main theorem unproved) is the correct designed verdict; no semantic fraud and no false resolution claim found.","failreason":"No `ep414` declaration and no proof of the pinned positive-domain statement: spec v2 replay returns fail — \"theorem ep414 missing: the pinned statement is not proved (main theorem unproved) [contract note: re-declared tau, h, iterH]\" (exit 1). The submission is a recorded negative observation, not a resolution of the node's goal."}