{"taskid":"ea3e520e6174a077684fbec95ac48cf45332acebfce44668aeee16d9564c8673i0","node":"lean","claimid":"60eab5a16bcb8684aac2e8684ccd88a8e79efd25f789005cac3dbcfe4f68784fi0","result":{"artifactKey":"lean-JSP-000598","buildEvidence":{"defaultBuild":"lake build (clean, from scratch) -> 'Build completed successfully', exit=0","leanVersion":"Lean 4.34.1 (arm64-apple-darwin24.6.0), Lake 5.0.0","log":"build.log inside the attached zip; three build checks all exit=0","noSorry":true,"specJudgment":"lake env lean -DwarningAsError=true Jsp598.lean -> exit 0 (no errors, no sorry/admitted warnings)","strictNote":"this Lake (5.0.0) does not accept --warning-as-error as a lake flag; the spec's compiler-level judgment was executed as the equivalent lean-level command 'lake env lean -DwarningAsError=true Jsp598.lean' (exit 0), plus 'lake build' default and 'lake build Jsp598.lean' both green","target":"Jsp598.lean"},"honestScope":{"axiomStatement":"egrS75 : forall n m, sameSupport n m -> n = m","axiomation":"the deep [EGRS75] analytic core is carried as a single explicitly declared axiom egrS75 (prime support of C(2n,n) determines n), NOT as hidden sorry; everything else is proved from scratch in-file because this Lean core ships without Nat.factorial/Nat.choose/Nat.Prime","correspondenceArtifact":"metafile://278227d8e0c2190de8a40a17d15dde99dc6062bdfc75ec5dd0f7b7ef747e21b9i0 (correspondence-T4-JSP-000598)","proven":["fact / fact_succ / fact_pos","Pascal binom / binom_eq_zero / binom_diag","binom_mul_fact: C(n,k)*k!*(n-k)! = n! for k<=n (the factorial identity)","Prime with Euclid's lemma built in; prime_le_of_dvd_fact: prime p | fact m -> p <= m","centralBinom_factorial: C(2n,n)*(n!)^2 = (2n)!","support_mem_bound: 2 <= p -> p | C(2n,n) -> p <= 2n"],"residualRisk":"whether the axiom faithfully captures the exact EGRS75 lemma chain used by the credited proof is NOT machine-checked here; the Overleaf exposition was not consulted (read-only, stability-flagged in the correspondence artifact) - reviewers should check the axiom statement against [EGRS75] Math. Comp. 29 (1975) 83-92 directly"},"task":"T4-JSP-000598","type":"formalize","hash":"55fab4be6a6a040a780826c81b818fb970e27598af85c169bf58cbbd3fc16940"},"hash":"ded725565597da67ca4cb2d0786d5fe1c8d48e79d74bf47216aec27a4889f379","contentType":"application/json;utf-8","attachment":"metafile://257d346bb0c68413a872a2ca25f49491b04dca7e076b86c9768a7a513352481bi0.zip","childids":[]}