# 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: 1/1. Author response: not_supplied.

Prior accounting $7.721109; arbitration accounted/reserved $0.272742; campaign budget $25.00.

Uncovered queued targets: eq:cI3bnd, eq:cI41bnd, eq:cI42bnd, eq:cIQ11bnd, eq:cIQ1def, eq:cIQ2bnd, eq:cIQ3def, eq:cKzBnd, eq:cRfuIs, eq:cSfbnd1, eq:decayMtrx, eq:eqeq, eq:fincK, eq:gls, eq:hatRfuBnd, eq:modBndaEqAp, eq:modBndaNeqAp, eq:nmUpToM, eq:vgIs, lem:GGq, lem:kEllD, lem:spec0, lem:spec1, lem:spec2, lem:spec3, lm_generation, lm_local, lm_transference, narrative:103198, narrative:104579, narrative:105898, narrative:109314, narrative:110408, narrative:112352, narrative:114852, narrative:115416, narrative:118709, narrative:119956, narrative:122162, narrative:123431, narrative:123918, narrative:13050, narrative:144695, narrative:47002, narrative:55546, narrative:68030, narrative:71322, narrative:86590, narrative:92045, narrative:93454, narrative:98161, narrative:99181, th_sg, thm:CircMeth, thm:IQ0, thm:IQM, thm:IQX, thm:Main, thm:RNU, thm:Vin, thm:cMNis, thm:cMNtoMNU, thm:specGap

## eq:cIQ12bnd — gemini-4-argon

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

The displayed proof of Proposition eq:cIQ12bnd contains one substantive gap in its written step and one cosmetic notation omission, while the remaining three findings are resolved by inspecting context present in the full manuscript outside the local review packet. Specifically, the step bounding Q^{-1/4} \sum_{\tilde g \ll Q} \tilde g^{-3/4 - \eta_0} by O(Q_0^{-\eta_0}) fails for \eta_0 \in [1/4, 1), and the manuscript only states 0 < \eta_0 < 1 in eq:fuIs. In addition, the intermediate display omits the pairwise coprimality subscript on (g_1, g_1', \tilde g) that was just established in the preceding prose and is needed before bounding the q-sum. Both issues are locally repairable using the manuscript's own setup (taking 0 < \eta_0 < 1/4 in Lemma lem:spec3 and keeping the prose coprimality restriction through the q-counting step), so the statement eq:cIQ12bnd is locally supported.

New repair (self-contained): In the proof of Proposition eq:cIQ12bnd, retain the pairwise coprimality condition on (g_1, g_1', \tilde g) established in the preceding prose through the first displayed inequality. On the support of this sum, [h g_1, h g_1', h \tilde g] = h g_1 g_1' \tilde g \ge g_1 g_1' \tilde g; since the outer sum is restricted to [h g_1, h g_1', h \tilde g] \ll Q, the inner sum over q \asymp Q with q \equiv 0 \pmod{[h g_1, h g_1', h \tilde g]} has at most O(Q / (g_1 g_1' \tilde g)) terms. After bounding the inner q-sum by O(Q / (g_1 g_1' \tilde g)), drop the coprimality condition and use 0 < a, a' \ll T (from eq:fFdef) so that \sum_{h \mid (a,a'), h \le H} h^{9/4} \sum_{g_1 \mid a} \sum_{g_1' \mid a'} 1 \ll_\varepsilon H^{9/4} T^\varepsilon. Moreover, in Lemma lem:spec3, since q \ge 1, the bound eq:spec3 remains valid if \eta_0 > 0 is replaced by any smaller positive constant (and in fact the proof of Lemma lem:spec3 already produces an exponent \eta_0 \ll (\delta - \Theta_0) / \mathcal{C} < 1/4 by eq:cCis). Fixing 0 < \eta_0 < 1/4 before defining U and H in eq:fuIs and eq:His, the sum over \tilde g \ll Q satisfies Q^{-1/4} \sum_{1 \le \tilde g \ll Q} \tilde g^{-3/4 - \eta_0} \ll Q^{-1/4} Q^{1/4 - \eta_0} = Q^{-\eta_0} \le Q_0^{-\eta_0} because Q \ge Q_0. Combining this with eq:TXNis (X^2 T = N and T = N^{1/100}), eq:Q0is (Q_0 = T^{(\delta - \Theta_1)/20}), eq:fuIs (U = Q_0^{\eta_0^2/100}), and eq:His (H = Q_0^{\eta_0/10}) yields \mathcal{I}_Q^{(\neq, \le)} \ll_\varepsilon N T^{2(\delta-1)} Q_0^{6\eta_0^2/100 + 9\eta_0/40 - \eta_0} T^\varepsilon = N T^{2(\delta-1)} Q_0^{-(31\eta_0/40 - 3\eta_0^2/50)} T^\varepsilon \ll N T^{2(\delta-1)} N^{-\eta} for a suitable \eta > 0.

### finding-362dc54b75277cb7dcb6 — confirmed_error (substantive)

In the last display of the proof of Proposition eq:cIQ12bnd, the authors bound Q^{-1/4} \sum_{\tilde g \ll Q} \tilde g^{-3/4 - \eta_0} by O(Q_0^{-\eta_0}) using Q \ge Q_0. Direct evaluation of the sum over 1 \le \tilde g \ll Q gives O(Q^{1/4 - \eta_0}) only when 0 < \eta_0 < 1/4; for \eta_0 = 1/4 it gives O(\log Q), and for \eta_0 > 1/4 the series converges so the sum is \Theta(1) (the \tilde g = 1 term alone is 1), yielding \Theta(Q^{-1/4}) after multiplying by Q^{-1/4}. When Q = Q_0 and \eta_0 > 1/4, Q_0^{-1/4} is strictly larger in order of magnitude than the asserted Q_0^{-\eta_0} (and for \eta_0 close to 1, H^{9/4} Q_0^{-1/4} = Q_0^{9\eta_0/40 - 1/4} would not even decay). Because Lemma lem:spec3 only states the existence of \eta_0 > 0 and eq:fuIs only specifies 0 < \eta_0 < 1, the displayed inequality does not follow as written without restricting \eta_0 < 1/4.

Hypotheses: Checked Lemma lem:spec3 and eq:fuIs in the full manuscript. Equation eq:fuIs explicitly states 'where 0 < \eta_0 < 1 is the number which appears in Lemma \ref{lem:spec3}'. Although the proof of Lemma lem:spec3 actually produces a very small \eta_0 (and weakening \eta_0 to lie in (0, 1/4) is trivially valid since q \ge 1), the restriction \eta_0 < 1/4 is not stated in Lemma lem:spec3 or eq:fuIs.

Original source: "since $Q\\ge Q_{0}$."

Later edition: not_checked. No later edition was supplied for comparison.

Later source: ""

Affected targets (arbiter assessment): eq:cIQ12bnd

### finding-75f06dc5ae478b6e8083 — confirmed_error (cosmetic)

In the prose immediately preceding the display, the authors define g = (a, q) = h g_1, g' = (a', q) = h g_1' with h = (g, g'), and (a - a', q) = h \tilde g, and correctly observe that g_1, g_1', and \tilde g are pairwise coprime, so that [h g_1, h g_1', h \tilde g] \ge g_1 g_1' \tilde g. However, when writing the first multi-line inequality of the display, they omit the pairwise coprimality condition from the summation subscripts on g_1, g_1', \tilde g before bounding the inner sum \sum_{q \asymp Q, q \equiv 0 ([h g_1, h g_1', h \tilde g])} 1 by O(Q / (g_1 g_1' \tilde g)). For unrestricted divisors g_1 \mid a, g_1' \mid a', \tilde g \mid (a - a'), the inequality [h g_1, h g_1', h \tilde g] \ge g_1 g_1' \tilde g fails when the divisors share common factors. Because the prose right before the display explicitly establishes pairwise coprimality for the gcd variables in order to justify [h g_1, h g_1', h \tilde g] \ge g_1 g_1' \tilde g, this is a cosmetic notation omission in the intermediate display line: keeping the pairwise coprimality condition in force until the inner q-sum is bounded by O(Q / (g_1 g_1' \tilde g)), and only then dropping it by positivity, makes the step completely rigorous.

Hypotheses: Checked the preceding sentences in the proof of eq:cIQ12bnd: for g = (a,q), g' = (a',q), h = (g,g'), one has (g_1, g_1') = 1, and any common divisor of g = (a,q) and (a-a',q) divides (a, a-a', q) = (a, a', q) = h, so (g_1, \tilde g) = (g_1', \tilde g) = 1.

Original source: "\\sum_{g_{1}\\mid a\\atop g_{1}\\ll Q}\n\\sum_{g_{1}'\\mid a'\\atop g_{1}'\\ll Q}"

Later edition: not_checked. No later edition was supplied for comparison.

Later source: ""

Affected targets (arbiter assessment): eq:cIQ12bnd

### finding-2ecac14b29119cca2ded — packet_context (none)

In the full manuscript (Section 7), Lemma eq:cIQ1def establishes the upper bound \mathcal{I}_Q^{(\neq)} \ll U^6 (X^2 / T) \sum_{\ff \in \fF} \sum_{\ff' \in \fF, a' \neq a} \sum_{q \asymp Q} \{(a^2, q)((a')^2, q)\}^{1/2} (a - a', q)^{1/4} / q^{5/4}, and eq:cIQ1break splits this off-diagonal contribution into \mathcal{I}_Q^{(\neq, >)} + \mathcal{I}_Q^{(\neq, \le)} according to whether (a, a') > H or (a, a') \le H. Thus the starting expression in the proof of eq:cIQ12bnd is supplied by eq:cIQ1def and eq:cIQ1break in the full source (with '=' used as shorthand for the (a, a') \le H piece of the majorant in eq:cIQ1def).

Hypotheses: Verified against eq:cIQ1def and eq:cIQ1break in Section 7 of the full reviewed source; the hypothesis Q < X of Lemma eq:cIQ1def is in force throughout Section 7.

Original source: "\\cI_{Q}^{(\\neq,\\le)}\n&=&"

Later edition: not_checked. No later edition was supplied for comparison.

Later source: ""

Affected targets (arbiter assessment): eq:cIQ12bnd

### finding-fd1b38508d14eff5b8b9 — packet_context (none)

All prerequisites for applying the divisor bound and Lemma lem:spec3 are supplied in Section 3.1 of the full manuscript: (1) eq:fFdef and the paragraph following eq:fFTbnd identify \g \in \fF_T (with multiplicity from \g = \g_1 \g_2) with shifted forms \ff = \ff_\g \in \fF and a = a_\g = \langle e_1, \g v_0 \rangle; (2) eq:fFdef enforces a = \langle e_1, \g_1 \g_2 v_0 \rangle > T/100 > 0 and \|\g_1\| \asymp T_1, \|\g_2\| \asymp T_2 with T_1 T_2 = T (eq:TT1T2), so 0 < a, a' \asymp T and 0 < |a - a'| \ll T for a' \neq a, which justifies absorbing the divisor counts into T^\varepsilon; (3) since \tilde g \mid (a - a') with 0 < |a - a'| \ll T = N^{1/100} (and also \tilde g \ll Q < X = N^{99/200} by eq:TXNis), every modulus \tilde g satisfies 1 \le \tilde g < N as required by Lemma lem:spec3; and (4) the outer cardinality bound \#\fF_T \ll T^\delta is given in eq:fFTbnd.

Hypotheses: Verified against eq:TXNis, eq:TT1T2, eq:fFdef, eq:fFTbnd, and Lemma lem:spec3 in the full reviewed source.

Original source: "To the last sum, we again apply Lemma \\ref{lem:spec3}, giving"

Later edition: not_checked. No later edition was supplied for comparison.

Later source: ""

Affected targets (arbiter assessment): eq:cIQ12bnd

### finding-2c13e42c06ef86425b45 — packet_context (none)

The scale relations needed to convert the final bound into N T^{2(\delta - 1)} N^{-\eta} are explicitly given in the full manuscript: eq:TXNis sets T = N^{1/100} and X = N^{99/200} so that T X^2 = N, and eq:Q0is sets Q_0 = T^{(\delta - \Theta_1)/20} with \Theta_1 < \delta (eq:gT1def). Hence (X^2 / T) T^{2\delta} = (X^2 T) T^{2(\delta - 1)} = N T^{2(\delta - 1)}, and Q_0 = N^{(\delta - \Theta_1)/2000} grows as a fixed positive power of N, so that U^6 H^{9/4} Q_0^{-\eta_0} T^\varepsilon = Q_0^{-(31\eta_0/40 - 3\eta_0^2/50)} T^\varepsilon \ll N^{-\eta} for sufficiently small \varepsilon > 0.

Hypotheses: Verified against eq:TXNis, eq:gT1def, eq:Q0is, eq:fuIs, and eq:His in the full reviewed source.

Original source: "By \\eqref{eq:His} and \\eqref{eq:fuIs}, this is again a power savings, as claimed."

Later edition: not_checked. No later edition was supplied for comparison.

Later source: ""

Affected targets (arbiter assessment): eq:cIQ12bnd