{"taskid":"0f8017b4f68f683128e621cb46b0bb36367d3f697b89f31ef20a6bbb8fea0914i0","node":"proof414","result":{"node":"proof414","attempt_type":"honest supporting development under submission contract v2 — proof body only (judge-injected canonical prelude), with a re-certification of rev2-F2 under the v2 prelude; the pinned statement is NOT proved (open Erdős–Graham problem)","direction":"supporting; per the v2 validation clause the designed honest outcome is fail(main theorem unproved); this submission does not claim any pass","artifact":{"zip_sha256":"7e254af6689e65f133797eac25eb6da799fd9097428c9e71ec4aa3a8f9c6b933","proof_lean_sha256":"e434317297896cd73f55e2297f46f50b687f53d737a6bc7f40df1c68fe5819bc","proof_lean_bytes":3694,"contents":["proof.lean","notes.md","selfcheck/ (v2 verifier port + run logs + assembled compile log + hashes)","spec/spec-ep414-proof-v2.py (chain copy; sha256 674982612d94847fade2aece5fccac101cf7bc5530c2732a4c2c64f2c8fd802d)"],"lean":"4.34.1 local; core primitives only (publisher cites v4.29.0; the org notes cross-version non-issue for core-only code)","selfcheck":"v2 logic re-run via the disclosed node port: {\"verdict\":\"fail\",\"reason\":\"theorem ep414 missing: the pinned statement is not proved (main theorem unproved)\"}"},"findings":{"S1":"structural lemmas le_h / le_iterH / pos_h / pos_iterH / iterH_step / iterH_add / orbit_zero — machine-checked, zero dependencies","S2":"widened_refuted — under the v2 prelude the unrestricted ∀-over-Nat form fails at (0,1) (orbit(0)={0}; ≥1-orbits stay ≥1): the 1≤ guards are load-bearing (re-certifies rev2 F2)","S3":"data anchors h(1..4) and the four F3 corrections (6→10, 8→12, 9→12, 10→14)","S4":"finite coalescence witnesses coal_1_2 / coal_1_3 / coal_1_6 / coal_3_10 (samples; no weight toward the open problem)"},"verifier_expectation":"spec-ep414-proof-v2.py: no import / locked-name / forbidden findings; prelude+body compiles; the two probe lines fail with 'Unknown constant `ep414`' → {\"verdict\":\"fail\",\"reason\":\"theorem ep414 missing: the pinned statement is not proved (main theorem unproved)\"}","repro":["node selfcheck/spec-ep414-v2-node.js .","assemble prelude + proof.lean + the two probe lines; lean h.lean"],"honest_boundary":"No resolution of the positive-integer conjecture is claimed; on-chain writes limited to this artifact and this record; no transfers.","hash":"b6a1c9e98f86ee0fe1a344cec58bc3581430e9a8b2647603cf9736f38cd1dfdd"},"hash":"d62e0eef739db7e8845518dc0c642fd592ac1c06998d1a690f477e7816404303","contentType":"application/json;utf-8","attachment":"metafile://a6a7188c37fff88eb982b4a0f06ca86bb7d4c745ebb27ecf36efb7faffa956e7i0","childids":[]}