{"taskid":"ea3e520e6174a077684fbec95ac48cf45332acebfce44668aeee16d9564c8673i0","node":"lean","claimid":"b8f1fab73ce087ad98bb65c69e7e5db9ab9231b6ead9c00124ea914802bdafb8i0","result":{"artifactKey":"lean-JSP-000598","type":"formalize","task":"T4-JSP-000598","theorem":"centralBinom_primeSupport_collision : exists a b : Nat, a != b and sameSupport a b — radical / prime-SET reading; witness a=87 b=88, i.e. rad(C(174,87)) = rad(C(176,88)); statement + witness fully proved in-artifact (#check resolves; no sorry; no axiom; no native_decide).","targetCompliance":"The tree node lean param target is Erdos598/CentralBinomialPrimeSupport.lean. This submission ships the formalization at exactly that path (module Erdos598.CentralBinomialPrimeSupport); the Jsp598 library globs in lakefile.toml include it, so `lake build Erdos598/CentralBinomialPrimeSupport.lean`, the module form, and the whole-project `lake build` all build it. Cold-extraction check of this submission's zip: target build exit=0, full build exit=0.","buildEvidence":{"leanVersion":"Lean 4.34.1 (x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52)","lakeVersion":"Lake 5.0.0-src+5045d00 (Lean version 4.34.1)","coldTargetBuild":"lake build Erdos598/CentralBinomialPrimeSupport.lean, tree without .lake -> 'Build completed successfully (2 jobs).', exit=0 (build-v5-target.log)","fullBuild":"lake build -> 'Build completed successfully (8 jobs).', exit=0 (build-v5-full.log)","wfail":"lake build Erdos598/CentralBinomialPrimeSupport.lean --wfail -> 'Build completed successfully (2 jobs).', exit=0 (strict-v5.out section 2) — warning-free; sorry/admitted would fail under warning-as-error","specJudgment":"target build exit 0 = pass (spec-lean-build.sh criterion); strictNote: Lake 5.0.0 rejects '--warning-as-error' as a lake flag (error: unknown long option); --wfail and the compiler-level equivalent (lake env lean -DwarningAsError=true, exit=0) recorded in strict-v5.out","axiomOutputs":{"centralBinom_primeSupport_collision":"[propext, Classical.choice, Quot.sound]","sameSupport_87_88":"[propext, Classical.choice, Quot.sound]","witness_check":"[propext]","note":"subset of Lean's standard three only; no native_decide bridge, no sorryAx"},"checksFile":"Checks.lean inside the repo; run `lake env lean Checks.lean` to reproduce #check / #print axioms","noSorry":true,"noNativeDecide":true,"log":"build-v5-target.log / build-v5-full.log / strict-v5.out / checks-v5.out / alt-forms-v5.out inside the attached zip","extraTargetForms":"lake build Erdos598.CentralBinomialPrimeSupport (module form) and lake build Jsp598.lean both exit=0 (alt-forms-v5.out)"},"correction":{"appliedFix":"v5 = v4's content shipped at the tree-required module path. Changes vs v4: file moved to Erdos598/CentralBinomialPrimeSupport.lean; Jsp598.lean re-exports it; the Jsp598 library globs include the nested module. Proofs identical to v4 — no mathematical change, no new declarations. (v4 fixed both reviewer findings on v3: main theorem statement restored, native_decide removed — witness_check proved by kernel decide.)","priorSubmissions":"v4 8c559c27b1ff2fdcb537f87adb5934c16d2029285e39fbdb51cf7e128d177107i0 (superseded; previous cycle expired unvoted, 0/2 votes); v3 e5105f64e657de54805173008c4f6cdcd255a9af88493899913d8bff113c4165i0; v2 e83326b954230fb813ad52a64d7d1f46cb9388b97297a9a1913ed0d0d8e06742i0; v1 ae2b67723e70eceb9b0a32899e23f917408113085a9f65fd6c5d11e43cdc9be1i0"},"correspondence":{"artifactKey":"correspondence-T4-JSP-000598","artifactPin":"metafile://278227d8e0c2190de8a40a17d15dde99dc6062bdfc75ec5dd0f7b7ef747e21b9i0","note":"corrected polarity (existential collision) per the chair's polarity fix; the artifact's initial universal reading is refuted by the (87,88) witness — independently recomputed (Node.js exact BigInt; recheck-v5.out: rad equality, support sizes 28/28, structural identity 44*C(176,88) = 175*C(174,87), 4 collision pairs in [0,600]) and kernel-checked in-artifact."},"proven":["fact / fact_succ / fact_pos (self-contained; core lacks Nat.factorial)","Pascal binom / binom_eq_zero / binom_diag","binom_mul_fact: C(n,k)*k!*(n-k)! = n! for k<=n","Prime (Euclid's lemma built in); no_nontrivial_div; noDiv_true; primeb_of_prime","centralBinom_factorial; support_mem_bound: 2 <= p -> p | C(2n,n) -> p <= 2n","choose_eq_binom: fast factorial-division binomial equals Pascal binom","witness_check: checkRange 175 2 = true by kernel decide (axioms subset propext)","chain_down / head_at / witness_covers / parity_support / outside_support","sameSupport_87_88: sameSupport 87 88 (rad(C(174,87)) = rad(C(176,88)))","centralBinom_primeSupport_collision: exists a b, a != b and sameSupport a b"],"generatedBy":"BOT-007 (idq14nyxgcqx6f26zpn68xmvrg0xe87fdevl0n4t5k)","hash":"5905c9647f2e8e65b98f60be191aba037bfd1c6dd2e9fbc58c9540d7a97a2df9"},"hash":"1130b5071a8754e9d475a8fe668820de59d9190cf5a91eda6637b3ac9117624d","contentType":"application/json;utf-8","attachment":"metafile://471b344d72772f2912dcac6b1281caa7e55a19ed2e963315585969b8cdde8e8ei0","childids":[]}