{"id":"0563a179-104e-41cb-9505-eae902f7af7f","arxiv_id":"2602.03722","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"partial","parameter_count":0,"one_line_summary":"A long-standing congruence conjecture about k-differentials is proved via Jacobi symbols, completing the spin-parity classification in genus 0 and 1.","lead":"The paper proves a number-theoretic counting conjecture that had blocked a complete spin-parity classification of k-differentials on genus-zero and genus-one curves. With the conjecture settled, the classification is now unconditional.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"I examined the proof of Theorem 1.2 with the strongest claim in view. The reduction of Conjecture 1.1 to the two lemmas is sound: Lemma 2.5 is a direct double-counting argument, and Lemma 2.4 is a correct application of standard Jacobi-symbol identities. The unstated positivity of n is the only real subtlety, and it is easily resolved by reducing n modulo k. The reader's weakest_assumption concerns the geometric reduction in [5], which is genuinely imported without reproof, but that is a citation to prior published work and does not threaten the number-theoretic central claim. I therefore find no reason to change the ACCEPT verdict, while partially agreeing that the geometric reduction is the point to keep in mind if the spin-parity applications are the focus.","tokens_in":8662,"tokens_out":22900,"duration_ms":191410,"concrete_test":"Formalize Lemma 2.4 in Lean/Mathlib (the even-a case via a+k and the supplementary law); if the kernel accepts the proof, the only non-formalized step in the proof of Theorem 1.2 is closed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"For the central claim (Theorem 1.2), I find no load-bearing defect. The proof reduces Conjecture 1.1 to Lemmas 2.4 and 2.5. Lemma 2.5 is formalized in Lean and its elementary floor-sum argument checks out. Lemma 2.4 is a standard Jacobi-symbol computation: the odd case follows from Eisenstein and Gauss–Schering, and the even case from applying Eisenstein to a+k; the arithmetic (k^2−1)/8 ≡ floor((k+1)/4) (mod 2) is correct. The only minor gap is that Lemma 2.4's proof invokes Lemmas 2.1–2.2, stated for positive a, while Conjecture 1.1 does not explicitly restrict n to be positive. This is harmless: N_k(n) depends only on n modulo k, and the gcd conditions are preserved under replacing n by its least positive residue. The spin-parity theorems 1.3–1.4 inherit the geometric reductions of [5]; that is a citation to published work, not a new gap.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proves Conjecture 1.1, a number-theoretic conjecture of Chen–Gendron concerning the parity of N_k(n), the number of pairs (b_1,b_2) with 1 ≤ b_i ≤ (k−1)/2, b_1+b_2 ≥ (k+1)/2, and b_2 ≡ n b_1 (mod k). The proof reformulates the conjecture in terms of Jacobi symbols, reduces it to two lemmas: Lemma 2.4, a floor-sum evaluation for F_k(a), and Lemma 2.5, a combinatorial identity N_k(n)=F_k(n+1)−F_k(n). Lemma 2.5 is verified in Lean. Theorem 1.2 then follows by applying Lemma 2.4 to the unique even element of {n,n+1}. The paper also states that this removes the conditional from the geometric spin-parity results Theorems 1.3 and 1.4 of [5].","tokens_in":8838,"tokens_out":10341,"duration_ms":102380,"significance":"If correct, the paper settles a conjecture that was the last missing ingredient in the complete determination of spin parity for k-differentials in genus zero and one. The proof is self-contained, elementary, and reproducible: the key combinatorial identity is machine-checked, and the non-formalized part (Lemma 2.4) is a standard Jacobi-symbol computation. The AI-assisted provenance is described transparently. The number-theoretic core of Theorem 1.2 is independent of the geometric reductions in [5], so even a hypothetical error in those geometric arguments would not affect the proof of Conjecture 1.1.","major_comments":[],"minor_comments":[{"comment":"Lemma 2.4 is stated for any integer a, but the proof invokes Lemmas 2.1 and 2.2, which are stated for positive a. In Theorem 1.2, if n is allowed to be negative, the even element e of {n,n+1} can be negative. This is harmless: F_k(a+2tk) ≡ F_k(a) (mod 2) for every integer t, so one may shift a by an even multiple of k to make it positive, or alternatively reduce n modulo k before starting the proof. I recommend adding one sentence to this effect.","section":"§2.1, Lemma 2.4"},{"comment":"The expression (2/d_i) uses d_i = gcd(k,m_i), which can be 1. Please state the standard convention (2/1)=1 so that the Jacobi-symbol reformulation of n_k(µ) is unambiguous.","section":"Remark 3 and Eq. (6)"},{"comment":"The appendix correctly states that Lemma 2.4 was not formalized in Lean. Since Lemma 2.4 is a short, standard calculation and the human proof is complete, this limitation does not reduce confidence in Theorem 1.2.","section":"Appendix"}],"recommendation":"minor_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know: this paper proves the open number-theoretic conjecture from Chen–Gendron's paper (Conjecture A.10) that makes their genus zero and one spin-parity theorems for k-differentials unconditional; and the proof is elementary but clean, with the key identity checked in Lean. I think the central math is correct.\n\nThe new content is the Jacobi-symbol reformulation of N_k(n) and, more importantly, Lemma 2.5: N_k(n)=F_k(n+1)-F_k(n). That identity is neat and lets the parity of N_k(n) drop out of Lemma 2.4, which computes F_k parity by standard Eisenstein/Gauss–Schering facts. The authors also note that the coprimality assumption is not used in Lemma 2.5, and they give a cleaner Jacobi-symbol description of n_k(μ) in Remark 3. All of that is genuinely new relative to [5].\n\nWhat the paper does well: it is transparent about how the proof was found. The appendix describes the AxiomProver contribution and states plainly that only Lemma 2.5 was formalized in Lean, not Lemma 2.4. The formalization is a real plus, even if limited to the combinatorial core. The rest of the argument is standard number theory and I did not find a gap.\n\nSoft spots are minor. The geometric reduction connecting N_k(n) to spin parity is imported from [5] and not reproved; if that appendix had an error, Theorems 1.3–1.4 would fail even though Theorem 1.2 is fine. That's the nature of a follow-up paper, and not a defect here. The other small thing is that Lemma 2.4 is stated for all integers a but the proof implicitly treats a as positive when invoking Eisenstein. You can shift a by a multiple of k to make the numerator positive while preserving the parity of F_k, so the proof works, but the WLOG is not spelled out.\n\nSo: a correct, well-scoped result that settles an open conjecture. It belongs in the literature. It's not a revolution—the methods are elementary—but the classification program needs this step. I would send it to a serious refereed journal. It deserves a referee who knows the geometry context, but the number theory is checkable by any number theorist.","headline":"Proves the Chen–Gendron parity conjecture; the number theory is correct and self-contained, with a Lean-checked core, though the geometric reduction is inherited from prior work.","tokens_in":9362,"tokens_out":5380,"would_cite":true,"duration_ms":47861,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["11A07","14H10","32G15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves Conjecture 1.1, making spin-parity formulas for k-differentials in genus zero and one unconditional.","keywords":["spin parity","k-differentials","Jacobi symbols","floor-sum identity","Eisenstein's lemma","theta characteristics","moduli space of k-differentials","formal verification"],"falsifier":"Compute N_k(n) by brute force for all odd k up to, say, 101 and all n with gcd(n,k)=gcd(n+1,k)=1; any k,n with N_k(n) not congruent to ⌊(k+1)/4⌋ mod 2 would falsify Theorem 1.2. Because N_k(n) is a finite count, the theorem is directly checkable this way, and the paper's own examples.py verifies small values.","tokens_in":8527,"feed_emoji":"🔢","tokens_out":6425,"duration_ms":53674,"temperature":0.7,"pith_summary":"This paper proves an open number-theoretic conjecture (Conjecture 1.1) that previous work on k-differentials had left conditional. The conjecture says: for odd k and n with gcd(n,k)=gcd(n+1,k)=1, the parity of N_k(n) — the number of pairs (b1,b2) with 1 ≤ b1,b2 ≤ (k−1)/2, b1+b2 ≥ (k+1)/2, and b2 ≡ n b1 (mod k) — is exactly floor((k+1)/4) mod 2. The proof works by observing that this parity can be rewritten through Jacobi symbols, reducing the claim to a floor-sum identity (Lemma 2.5) that is established by elementary counting. Because earlier geometric work had reduced the spin parity of even-order k-differentials in genus zero and one to this exact parity, the theorem removes the conditional and completes the spin-parity determination for all odd k in those genera.","feed_headline":"Jacobi-symbol identity settles k-differential parity conjecture","feed_subtitle":"Proves Conjecture 1.1 and makes the spin-parity formulas for genus-zero and genus-one k-differentials unconditional","key_machinery":"The load-bearing object is the floor-sum F_k(a) = Σ_{i=1}^{(k−1)/2} ⌊(ai+m)/k⌋, with m=(k−1)/2. Lemma 2.5 identifies N_k(n) with F_k(n+1) − F_k(n), converting the counting problem into a telescoping sum. Lemma 2.4 evaluates F_k(a) modulo 2 by matching Eisenstein's lemma and the Gauss–Schering residue-counting lemma for Jacobi symbols; it gives F_k(a) ≡ 0 for odd a and F_k(a) ≡ ⌊(k+1)/4⌋ for even a. The parity of ⌊(k+1)/4⌋ is then read off from k mod 8 via the supplementary law for (2/k). The appendix reports that an automated prover discovered this reformulation and that the combinatorial identity was formalized in the Lean proof assistant.","core_discovery":"The central claim is Theorem 1.2: Conjecture 1.1 is true. Equivalently, for every odd k and every n coprime to both k and k+1, the counting function N_k(n) satisfies N_k(n) ≡ ⌊(k+1)/4⌋ (mod 2). The proof is short: Lemma 2.5 expresses N_k(n) as the difference F_k(n+1) − F_k(n) of a floor-sum, and Lemma 2.4 evaluates each F_k term modulo 2 using Eisenstein's lemma and the Gauss–Schering form of Jacobi symbols. Since n and n+1 have opposite parity, one term vanishes modulo 2 and the other is exactly ⌊(k+1)/4⌋. Consequently the spin-parity theorems of the earlier work, Theorem 1.3 (genus zero) and Theorem 1.4 (genus one), are now unconditional.","pith_inferences":["A natural extension is to test whether the same floor-sum–Jacobi-symbol strategy evaluates N_k(n) for nearby congruence families or for higher-weight analogues of Jacobi symbols; the paper does not pursue these generalizations.","The formal verification covers only Lemma 2.5; the number-theoretic reduction through Eisenstein's and Gauss–Schering lemmas remains informal, so a fully machine-checked proof would still be needed to rule out slips there.","If the spin-parity formulas are used to distinguish connected components of Ω^k M_g(µ) for k ≥ 3, the now-unconditional parity may be combined with the hyperelliptic and low-genus invariants in future classification work.","The appendix's account of an automated discovery suggests a workflow where a conjectural parity statement can be handed to a prover to find an elementary reformulation; that is an observation about research process rather than a mathematical conclusion of the paper."],"forward_implications":["Theorem 1.3 now holds unconditionally: for genus zero and odd k, the spin parity of Ω^k M_0(2µ) is n_k(µ) mod 2.","Theorem 1.4 now holds unconditionally: for genus one and odd k, the spin parity of the component Ω^k M_1(2µ)_d of rotation number d is n_k(µ)+d+1 mod 2.","With the even-k case already resolved, the spin parity of every parity-type k-differential stratum in genus zero and one is now known.","The function n_k(µ) admits the Jacobi-symbol description n_k(µ) = #{i : (2/gcd(k,m_i)) ≠ (2/k)}, making the parity condition computable directly from µ."],"fun_headline_variants":["Jacobi-symbol proof settles spin parity conjecture","Spin parity of k-differentials now unconditional","Conjecture 1.1 proven via Jacobi symbols","Genus-zero and genus-one spin parity fully determined"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The paper's conclusions for moduli spaces depend on the geometric reduction from earlier work — that spin parity in genus zero equals n_k(µ) mod 2 and in genus one equals n_k(µ)+d+1 mod 2 — which is imported without reproof; if that reduction were wrong, Theorems 1.3–1.4 could fail even though Theorem 1.2 is true.","fun_headline_variants_meta":{"raw":{"variants":["Jacobi-symbol proof settles spin parity conjecture","Spin parity of k-differentials now unconditional","Conjecture 1.1 proven via Jacobi symbols","Genus-zero and genus-one spin parity fully determined"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000192,"raw_usage":{"total_tokens":1154,"prompt_tokens":686,"completion_tokens":468,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":430,"completion_tokens_details":{"reasoning_tokens":418}},"tokens_in":430,"tokens_out":468,"duration_ms":4471,"temperature":1.0,"reasoning_tokens":418,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T04:51:16.839433+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compute N_k(n) by brute force for all odd k up to, say, 101 and all n with gcd(n,k)=gcd(n+1,k)=1; any k,n with N_k(n) not congruent to ⌊(k+1)/4⌋ mod 2 would falsify Theorem 1.2. Because N_k(n) is a finite count, the theorem is directly checkable this way, and the paper's own examples.py verifies small values.","supporting_citations":[],"review_version":1}