Independent proof arbitration

Dispositions apply only to listed targets in the original frozen edition. A broken proof is not a refuted theorem. Later-edition decisions are separate.

Usable arbitration: 2/4. Author response: not_supplied.

Prior accounting $7.060184; arbitration accounted/reserved $0.968396; campaign budget $10.00.

Uncovered queued targets: blomgran, friedithm, intersection, intersectionlemma, iteratedens, narrative:13301, narrative:2151, narrative:22058, narrative:41873, narrative:45155, sumsa1

density — gemini-4-argon

Delivery: completed. Scoped proof disposition: broken. Statement: refuted.

Lemma 2.3 (density) is an imported result stated without proof and attributed to James [J]. As stated, the lemma is refuted by a scaling counterexample (f_1 = x^2 + y^2 of discriminant -4 and f_2 = 2x^2 + 2y^2 of discriminant -16): the statement omits primitivity of the form and conductor adjustments for non-fundamental discriminants, so the displayed formula assigns the same positive leading constant to both forms even though B_{f_2}(X) = B_{f_1}(X/2) forces the leading constant of f_2 to be half that of f_1. This misstatement persists in Theorem 2.2 of the 2011 revision (re-attributed to Bernays [Be]), although downstream applications in the paper only use the existence of a positive leading constant c(f_{a_0}) > 0 for a fixed primitive form f_{a_0}. The second finding concerns the concluding sentence of Proposition 2.1 (lowbound) following Lemma 2.3 and is an artifact of packet truncation: equation (relatekappa) and the form f_{a_0} are explicitly defined immediately before Lemma 2.3 in the full reviewed source.

Take the two positive definite integral binary quadratic forms f_1(x,y) = x^2 + y^2 of discriminant -D_1 = -4 (so D_1 = 4) and f_2(x,y) = 2x^2 + 2y^2 of discriminant -D_2 = -16 (so D_2 = 16). Both f_1 and f_2 satisfy every stated hypothesis of Lemma 2.3 (\ref{density}), which does not require f to be primitive or -D to be a fundamental discriminant. Because an integer m is represented by f_2 if and only if m = 2n for an integer n represented by f_1, the counting functions of positive integers < X represented by f_2 and f_1 satisfy B_{f_2}(X) = B_{f_1}(X/2) identically. If the asymptotic B_D(X) = c_D X / \sqrt{\log X} + O(X / \log X) held for both forms, then B_{f_2}(X) = B_{f_1}(X/2) = (c_4 / 2) X / \sqrt{\log X} + O(X / \log X) would force c_{16} = c_4 / 2. However, the displayed formula for \pi c^2 in Lemma 2.3 depends only on the prime divisors of D (which is {2} for both D = 4 and D = 16) and the Kronecker symbol (-D/n) (which agrees for D = 4 and D = 16 for every n >= 1, with \sum_{n=1}^{\infty} (-D/n) n^{-1} = \pi / 4 > 0). Consequently, the formula yields \pi c_{16}^2 = \pi c_4^2 > 0, and since B_D(X) >= 0 forces c_D >= 0, this gives c_{16} = c_4 > 0, contradicting c_{16} = c_4 / 2.

finding-c48e4d0c755b13b97f47 — confirmed_error (substantive)

Lemma 2.3 (\ref{density}) is stated for any positive definite binary quadratic form f over \mathbb{Z} of discriminant -D < 0, without assuming that f is primitive or that -D is a fundamental discriminant. For f_1(x,y) = x^2 + y^2 (D = 4) and f_2(x,y) = 2x^2 + 2y^2 (D = 16), the set of integers represented by f_2 is exactly twice the set of integers represented by f_1, so B_{16}(X) = B_4(X/2) for f_2 and f_1, requiring their leading asymptotic constants to satisfy c_{16} = c_4 / 2. Yet the displayed product formula for \pi c^2 in Lemma 2.3 gives the same strictly positive value for D = 4 and D = 16 because both have prime divisor set {2} and identical Kronecker character (-4/n) = (-16/n) with L(1, \chi_{-4}) = \pi/4 > 0. Note that downstream in Proposition 2.1 (lowbound) and Section 3.1 (narrative:22058), the authors only apply Lemma 2.3 to a single fixed primitive form f_{a_0} of discriminant -4a_0^2 and only use that B_D(X) = c X / \sqrt{\log X} + O(X / \log X) for some constant c > 0 depending on a_0, never using the defective explicit formula for c.

Hypotheses: Checked the hypotheses of Lemma 2.3 and Section 2 of the full reviewed source. While the form f_{a_0} constructed in the proof of Proposition 2.1 is stated to be primitive (gcd(A,B,C) = 1), Lemma 2.3 itself is formulated as a general standalone lemma for any positive definite integral binary quadratic form f of discriminant -D < 0, so f_2(x,y) = 2x^2 + 2y^2 satisfies all stated hypotheses of Lemma 2.3.

Original source: "Let $f$ be a positive definite binary quadratic form over $\\mathbb Z$ of discriminant $-D$, where $D$ is a positive integer."

Later edition: persists. In the 2011 revision, Lemma 2.3 is relabelled as Theorem 2.2 and re-attributed from James (1938) to Bernays (1912). Although the German title of Bernays's dissertation in the bibliography explicitly specifies primitive binary quadratic forms of non-square discriminant, the text of Theorem 2.2 in the revision retains the exact same hypotheses and displayed formula for \pi c_0^2 without requiring f to be primitive or adjusting the Euler factors for non-fundamental discriminants.

Later source: "Theorem 2.2 (Bernays, 1912). Let f be a positive definite binary quadratic form over Z"

Affected targets (arbiter assessment): density, lowbound, narrative:22058

finding-1f45b49d40e7e4883857 — packet_context (none)

In the full reviewed source, Lemma 2.3 (\ref{density}) is placed inside the proof environment of Proposition 2.1 (\ref{lowbound}), and the quoted sentence is the concluding sentence of the proof of Proposition 2.1 rather than part of Lemma 2.3. The definitions of the binary quadratic form f_{a_0} in (2.4)-(2.6) and the lower bound relation (\ref{relatekappa}) in (2.8) appear in the full reviewed source immediately before Lemma 2.3; their absence was purely an artifact of the local packet excerpting.

Hypotheses: In the full reviewed source, f_{a_0} is defined in (2.4)-(2.5) with discriminant -4a_0^2 (a_0 != 0) in (2.6) and relation (\ref{relatekappa}) is displayed in (2.8) just prior to Lemma 2.3.

Original source: "Lemma~\ref{density} paired with (\ref{relatekappa}) implies that\n

Later edition: corrected. In the 2011 revision, the exposition is reorganized so that Lemma 2.1, equation (2.10), and Theorem 2.2 precede Proposition 2.3 (the preliminary lower bound on \kappa(P,X)), cleanly separating the statement of Theorem 2.2 from the deduction of Proposition 2.3.

Later source: "Note that Theorem 2.2 paired with (2.10) immediately yields the preliminary lower bound on\nκ(P, X) from [S1]:"

Affected targets (arbiter assessment):

lowbound — gemini-4-argon

Delivery: provider_failed_or_incomplete. Scoped proof disposition: unresolved. Statement: unresolved.

niederheath — gemini-4-argon

Delivery: provider_failed_or_incomplete. Scoped proof disposition: unresolved. Statement: unresolved.

sievebound — gemini-4-argon

Delivery: completed. Scoped proof disposition: broken. Statement: unresolved.

The proof of Lemma 3.8 (sievebound) in the reviewed manuscript is defective. Although the dyadic decomposition (3.28)/(atok) using (defineAk) is valid, the proof attempts to bound the short-interval progression count for A_0 by directly invoking the cumulative asymptotic for sums of two squares in Lemma 3.7 (friedithm). This fails for four substantive reasons: (1) subtracting the cumulative asymptotic of Lemma 3.7 across an interval of length h = eta * 2^k / sqrt(k) leaves an error term of order (c_q/q) * (2^k / k^(9/14)) * (log q)^(1/7), which is larger than the claimed short-interval main term of order eta * (c_q/q) * (2^k / k) by a factor of k^(5/14)/eta; (2) elements a in A_0 satisfy f_{a_0}(x,y) - a_0 = a where f_{a_0} has discriminant -4a_0^2, and Footnote 4 omits both the shift by a_0 and the multiplier/divisor comparison needed to relate values of f_{a_0} to sums of two squares while tracking intervals and residue classes; (3) Lemma 3.7 requires gcd(a,q) = 1 and a = 1 mod gcd(4,q), whereas Lemma 3.8 is stated for arbitrary residues r mod q and is immediately applied to non-coprime residues; and (4) the proof replaces log x in the error term of Lemma 3.7 by log log q, producing an unbounded factor (log q / log log q)^(1/7) that cannot be absorbed into O(1) uniformly in q. In addition, there is a cosmetic boundary defect at q = 2 where log log 2 < 0. All of these issues persist unchanged in the separately supplied 2011 revision.

Taken literally with natural logarithms and the paper's Section 1 convention for << (existence of a positive constant c > 0), the right-hand side (log log q / q) * eta is negative at q = 2, which is permitted by the stated range 1 < q < log X. For q >= 3 (or under a standard small-modulus convention such as log log(q + 2) or max(1, log log q)), the upper bound is mathematically plausible via a direct upper-bound sieve on values of the shifted binary quadratic form f_{a_0}(x,y) - a_0 in short intervals and arithmetic progressions, as the authors remark prior to Lemma 3.8, but that sieve argument is not supplied in the manuscript.

finding-9a4280f7d662202cfc45 — confirmed_error (substantive)

The inner sum in (atok) counts elements in the short interval [2^k, 2^k + eta * 2^k / sqrt(k)] of length h = eta * 2^k / sqrt(k). Lemma friedithm provides only a cumulative asymptotic for B(x,q,a) up to x, with error term O((c_q/q) * (x / sqrt(log x)) * (log q / log x)^(1/7)). At x = 2^k, subtracting B(2^k, q, r) from B(2^k + h, q, r) yields a main-term difference of order eta * (c_q/q) * (2^k / k), but leaves an error term of order (c_q/q) * (2^k / sqrt(k)) * (log q / k)^(1/7) = (c_q/q) * (2^k / k^(9/14)) * (log q)^(1/7). Because k^(-9/14) >> k^(-1), this error term dominates the claimed bound by a factor proportional to k^(5/14) / eta. Thus Lemma friedithm as stated cannot establish the claimed short-interval upper bound.

Hypotheses: Checked against the hypotheses of Lemma sievebound (1 < q < log X, (log X)^2 <= 2^k, 2^(k+1) <= (log X)^3, 0 < eta < 1) and Lemma friedithm. Even when q is fixed and the residue class is admissible for Lemma friedithm, k ~ log log X grows with X, so the cumulative error term from Lemma friedithm exceeds the short-interval main term.

Original source: "By Lemma~\ref{friedithm}, the inner sum is bounded above (up to a constant) by"

Later edition: persists. In the 2011 revision, Lemma 3.7 becomes Theorem 3.7 and Lemma 3.8 corresponds to sievebound. The proof of Lemma 3.8 on page 22 makes the exact same invalid deduction from the cumulative estimate of Theorem 3.7 to the short-interval bound.

Later source: "By Theorem 3.7, the inner sum is bounded above (up to a constant) by"

Affected targets (arbiter assessment): sievebound, intersectionlemma, iteratedens

finding-503cc257ec76b55e89f2 — confirmed_error (substantive)

In Footnote 4 and the proof of Lemma sievebound, the authors assert that the subset of a in A^{(k)} with a = r mod q is contained in the set of sums of two squares in [2^k, 2^k + eta * 2^k / sqrt(k)] congruent to r mod q, because f_{a_0} has discriminant -4a_0^2. However, by definition of A_0, it is a + a_0 = f_{a_0}(x,y), not a itself, that is represented by f_{a_0}. Moreover, for a binary quadratic form f_{a_0}(x,y) = A_0 x^2 + 2B_0 xy + C_0 y^2 of discriminant -4a_0^2, completing the square gives A_0(a + a_0) = (A_0 x + B_0 y)^2 + (a_0 y)^2, so passing to sums of two squares requires shifting by a_0 and scaling by A_0 (or accounting for prime factors of a_0), which transforms both the interval and the residue class r mod q. No such comparison is carried out in the proof.

Hypotheses: Checked against the definition of f_{a_0} in (binquad)-(disc) and A_0 in Section 3. Because a_0 != 0 is a fixed non-zero curvature, the shift by -a_0 is always non-trivial.

Original source: "\mathcal A_0 = \{a\in\mathbb N\, | \, a\leq X, f_{a_0}(x,y)-a_0 = a \mbox{ for some integers } x,y\geq 0\}"

Later edition: persists. In the 2011 revision (page 5 and equation (2.2) on page 9, together with Footnote 7 on page 21), A_0 still consists of shifted values f_{a_0}(x,y) - a_0, and Footnote 7 repeats verbatim the unshifted claim that A^{(k)} is contained in the set of sums of two squares in [2^k, 2^k + eta * 2^k / sqrt(k)].

Later source: "A0 = {a ∈ N | a ≤ X, a = fa0 (x, y) − a0 for some integers x, y},"

Affected targets (arbiter assessment): sievebound, intersectionlemma, iteratedens

finding-ced4499eef7ad567dcd9 — confirmed_error (substantive)

Apart from the typographical error '(a,q=1)' for gcd(a,q) = 1, Lemma friedithm requires the residue class to be coprime to q and congruent to 1 modulo gcd(4,q). Lemma sievebound imposes no restriction on the residue class r mod q (only that 1 < q < log X is square-free), and its proof applies Lemma friedithm directly to a = r mod q without reducing non-coprime residues (gcd(r,q) > 1) or even residues when 2 | q (where gcd(4,q) = 2 and r = 0 mod 2 violates r = 1 mod 2). In fact, immediately after the proof of Lemma sievebound, the lemma is applied to progressions where q_0 q_1' | a' and q_0 q_1 | a, where the residue class is divisible by a non-trivial divisor of the modulus.

Hypotheses: Checked against the hypotheses of Lemma friedithm and Lemma sievebound. Square-freeness of q implies gcd(4,q) in {1, 2}, which does not ensure r = 1 mod gcd(4,q) when 2 | q, nor does it ensure gcd(r,q) = 1.

Original source: "For $2\\leq q\\leq x$, $(a,q=1)$, and $a\\equiv 1$ mod $(4,q)$ we have"

Later edition: persists. Page 22 of the 2011 revision retains the exact same hypotheses in Theorem 3.7 (including the typo '(a, q = 1)') and the same unrestricted residue r mod q in Lemma 3.8.

Later source: "For 2 ≤ q ≤ x, (a, q = 1), and a ≡ 1 mod (4, q) we have"

Affected targets (arbiter assessment): friedithm, sievebound, intersectionlemma, iteratedens

finding-bb13e00c3edaca1ad4fe — confirmed_error (substantive)

In the displayed bound for the inner sum, the authors replace log x in the error term of Lemma friedithm with log log q, writing O((log q / log log q)^(1/7)). Because (log q / log log q)^(1/7) is unbounded as q grows in the range 1 < q < log X and sum_k (1/k) is of constant order over (log X)^2 <= 2^k <= (log X)^3, substituting c_q << log log q into the displayed expression yields an upper bound of order eta * (log log q / q) * (log q / log log q)^(1/7), which is not << eta * (log log q / q) uniformly in q. Even if log log q arose from miswriting log x ~ k ~ log log X, the displayed deduction is invalid as written.

Hypotheses: Checked against 1 < q < log X and the k-summation range 2 log log X / log 2 <= k <= 3 log log X / log 2.

Original source: "\sum_k\eta\frac{c_q}{q{k}}\Biggl[1+\textrm{O}\Biggl(\left(\frac{\log q}{\log\log q}\right)^{\frac{1}{7}}\Biggr)\Biggr]\ll \eta\frac{\log\log q}{q}"

Later edition: persists. Page 22 of the 2011 revision retains the identical displayed formula with (log q / log log q)^(1/7) and the same unjustified absorption of this unbounded factor.

Later source: "Since cq \u001c log log q, substituting this into (3.28) we have\n " \u0012 \u0013 1 !#\n cq log q 7 log log q\n ∑ η qk 1 + O log log q \u001cη\n k q\n\nas desired."

Affected targets (arbiter assessment): sievebound, intersectionlemma, iteratedens

finding-2ea8ebefe6a0e41529e4 — confirmed_error (cosmetic)

Under the definition of << in Section 1 (y <= c z for a constant c > 0) and standard natural logarithms, the hypothesis 1 < q < log X permits q = 2, for which log log 2 = log(0.6931...) < 0. A negative right-hand side cannot bound a non-negative sum of reciprocals 1/a (nor can a positive constant c_q satisfy c_2 << log log 2 in Lemma friedithm). This is a cosmetic boundary/notational omission at q = 2, where analytic number theory bounds of this form require writing log log(q + 2) or max(1, log log q) (as the authors implicitly do in (finalint) by writing log log(q_0 + q_1 + q_1' + q_2)).

Hypotheses: Checked against the explicit definition of << in Section 1 and the modulus range 1 < q < log X in Lemma sievebound.

Original source: "\frac{\log\log q}{q}\cdot \eta"

Later edition: persists. Lemma 3.8 on page 22 of the 2011 revision retains the unmodified factor log log q / q for 1 < q < log X without a small-q convention.

Later source: "Lemma 3.8. Let A , X, and η be as before. Then we have\n 1 log log q\n ∑ a\u001c q\n ·η\n a∈A\n a≡r (q)\n\nwhere 1 < q < log X is a square-free integer."

Affected targets (arbiter assessment): friedithm, sievebound