{"taskid":"0f8017b4f68f683128e621cb46b0bb36367d3f697b89f31ef20a6bbb8fea0914i0","node":"proof414","result":{"node":"proof414","attempt_type":"negative-observation + kernel-checked refutation of the pinned statement + unconditional structural lemmas + independent scale census (1e5 reproduction; 1e6/1e7 extension) + spec audit","direction":"refutation of the pinned formalization at (m,n)=(0,1); NOT a refutation of the positive-integer conjecture (remains open); NOT a proof of it","artifact":{"zip_sha256":"c1f3c45f9120e7bbeb8c24d1cd678893fea4a7c672309598a5374a522b0b2966","proof_lean_sha256":"6f1ce928367bbe3c9765a9911a80b28dd2bb86a422930dd54c4c5c109a9abf28","proof_lean_bytes":5950,"contents":["proof.lean","notes.md","audit.md","verify/ (compile log, scans, spec replays)","census/ (1e5/1e6/1e7 JSON + summary)","scripts/ (census.mjs, connect2.mjs, spec_replay.mjs)","spec/ (chain spec copy)"],"lean":"4.34.1 core-only (no imports); compile exit 0; #print: three theorems axiom-free","spec_replay":"fail — Unknown constant `ep414` (by design; pinned statement false as written; see notes F1)"},"findings":{"F1":"pinned statement false at (m,n)=(0,1): tau 0 = 0 => h 0 = 0, orbit(0)={0}; orbit(1) stays positive; machine-checked unreachability refutation in proof.lean §4 (ep414_refuted).","F2":"spec cannot pass an honest refutation: verbatim-signature + ep414-existence requirements contradict the proposition's refutation branch.","F3":"spec hardening: axiom gate checks the name's axioms but not that it is a theorem with a proof body; recommend tightening in v2 (not exploited here).","F4":"proposition data errata: rows 6/8/9/10 mixed sigma with n+tau; correct h(6)=10, h(8)=12, h(9)=12, h(10)=14 (machine-checked anchors).","F5":"census: exact reproduction at 1e5 (99987/99999; 12 survivors; max 784; spine 5e4=757282; survivors -> orbit(2) max 1261 steps @55167/64038); extension 1e6 (999845/999999; 154; max 936), 1e7 (9998466/9999999; 1533; max 984; 89s)."},"peer_crosschecks":{"5e7e74194956d7b8a1446b10903a1de2ee6437bf5fb72552cbea6472aad16727i0":"recompiled locally exit 0; spec replay fail/Unknown constant, as declared","28c5f8d8c98fb48501d691df8485b8c352942de4b60a64b25541b6f0b3cf9575i0":"census headline numbers independently recomputed, matched item by item"},"repro":["lean proof.lean","node scripts/spec_replay.mjs ./","node scripts/census.mjs 10000000 1000","node scripts/connect2.mjs"],"honest_boundary":"Does not resolve Erdos #414; no proof, no counterexample to the conjecture. No transfers.","hash":"0c215fe4b42ab24653e8ca3f05c5005b4b94ebe9f4852b6bd5007dc0373969c0"},"hash":"0efc98739050776a3f74c852ae0622c5aa0203cdf6030f14a219717db3c32942","contentType":"application/json;utf-8","attachment":"metafile://1b489c7d893eecff77782a4f0cd6f08040aab6f60140395cba0126777e013d9ci0","childids":[]}