{"case_id": "case-08d1571a48a71c8bc6f1f2b9", "target_id": "eq:cIQ11bnd", "original_proof_status": "supported", "statement_status": "locally_supported", "statement_argument": "Under the section hypothesis Q_0 <= Q < X, the proof of eq:cIQ1def bounds the summands of eq:IQbnd1 pointwise in absolute value for each pair (\\ff,\\ff'), so restricting the off-diagonal sum to (a,a') > H yields the first displayed inequality for \\cI_Q^{(\\neq,>)}. By eq:vgIs, eq:fFdef, and eq:TT1T2, each \\ff \\in \\fF corresponds (with multiplicity) to \\gamma \\in \\fF with integer coefficient a = \\langle e_1, \\gamma v_0 \\rangle satisfying T/100 < a \\ll T = N^{1/100}. Writing h = (a,a') > H, \\tilde q_1 = (a^2,q), and \\tilde q_1' = ((a')^2,q), and using (a-a',q) \\le q, the inner sum over q \\asymp Q with [\\tilde q_1,\\tilde q_1'] \\mid q is bounded by O(1/[\\tilde q_1,\\tilde q_1']). Since [n,m] \\ge (nm)^{1/2} for all positive integers n,m, the factor (\\tilde q_1 \\tilde q_1')^{1/2}/[\\tilde q_1,\\tilde q_1'] is at most 1. Because 0 < a,a' \\ll T, the divisor sums over \\tilde q_1 \\mid a^2, \\tilde q_1' \\mid (a')^2, and h \\mid a contribute O_\\varepsilon(T^\\varepsilon). Since 1 \\le H < h \\le a \\ll T < N, Lemma lem:spec3 (eq:spec3) applies to the inner sum over \\ff' \\in \\fF with a' \\equiv 0 (mod h), bounding it by O(T^\\delta h^{-\\eta_0}) = O(T^\\delta H^{-\\eta_0}), while eq:fFTbnd bounds the outer sum over \\ff \\in \\fF by O(T^\\delta). Finally, using eq:His (H = U^{10/\\eta_0}), eq:fuIs (U = Q_0^{\\eta_0^2/100}), eq:Q0is (Q_0 = T^{(\\delta-\\Theta_1)/20} with \\Theta_1 < \\delta), and eq:TXNis (T = N^{1/100}, TX^2 = N), we obtain U^6 (X^2/T) T^\\varepsilon T^{2\\delta} H^{-\\eta_0} = N T^{2(\\delta-1)} T^\\varepsilon U^{-4} \\ll N T^{2(\\delta-1)} N^{-\\eta} for a suitable \\eta > 0.", "summary": "The proof of Proposition eq:cIQ11bnd is supported by the full manuscript. Four of the five findings arise solely from context omitted in the local review packet (the proof of Lemma eq:cIQ1def, the definition and size bounds of the family \\fF in eq:fFdef and eq:fFTbnd, and the scaling relations in eq:TXNis and eq:Q0is), all of which are explicitly supplied in Sections 2, 3, 5, 6, and 7 of the full source. The remaining finding identifies a harmless typographical slip where strict inequality [n,m] > (nm)^{1/2} is written instead of [n,m] >= (nm)^{1/2}; the non-strict inequality holds for all positive integers and suffices for the displayed estimate.", "chronology_note": "The recorded review policy cutoff is 2012-05-24 (journal received date). The verification of eq:cIQ11bnd from its internal manuscript dependencies is completely elementary and imports no external results. Model weights contain post-cutoff knowledge, which is not used as evidence.", "external_results": [], "decisions": [{"finding_id": "finding-88406dca5d888d3e6c81", "outcome": "confirmed_error", "severity": "cosmetic", "source_quote": "where we used $[n,m]>(nm)^{1/2}$.", "reasoning": "For positive integers n and m, [n,m] = (nm)^{1/2} when n = m (for example, when \\tilde q_1 = \\tilde q_1' = 1), so the strict inequality > is false as written and should be >=. However, the step only requires (\\tilde q_1 \\tilde q_1')^{1/2} / [\\tilde q_1, \\tilde q_1'] <= 1, which follows immediately from the elementary inequality [n,m] >= (nm)^{1/2}. Thus this is a cosmetic typographical slip with no impact on the proof.", "hypothesis_check": "In the proof, \\tilde q_1 = (a^2,q) and \\tilde q_1' = ((a')^2,q) are positive integers because q >= 1 and a, a' > T/100 > 0.", "affected_claims": ["eq:cIQ11bnd"], "revised_status": "not_checked", "revised_quote": "", "revised_reasoning": "No later edition was supplied for comparison."}, {"finding_id": "finding-5123f425c6e3b8aa1b00", "outcome": "packet_context", "severity": "none", "source_quote": "Assume $Q)} and \\cI_Q^{(\\neq,\\le)} decompose the off-diagonal sum according to whether (a,a') > H or (a,a') <= H. Because the bound in eq:cIQ1def is proved term-by-term for each pair (\\ff,\\ff'), restricting the sum to (a,a') > H is fully justified in the source.", "hypothesis_check": "Section 7 specifies Q_0 <= Q < X, which satisfies the hypothesis Q < X of Lemma eq:cIQ1def.", "affected_claims": [], "revised_status": "not_checked", "revised_quote": "", "revised_reasoning": "No later edition was supplied for comparison."}, {"finding_id": "finding-9f82e41a6712e46b2c60", "outcome": "packet_context", "severity": "none", "source_quote": "Writing $(a,a')=h>H$,", "reasoning": "The required integrality, positivity, and polynomial size bounds on a and a' are provided in the full manuscript. By Section 1.1 and eq:vgIs, v_0 \\in \\Z^4 and \\gamma \\in \\Gamma \\subset \\SO_F(\\Z), so a = a_\\gamma = \\langle e_1, \\gamma v_0 \\rangle \\in \\Z. By eq:fFdef and eq:TT1T2 (Section 3.1), every \\gamma = \\gamma_1 \\gamma_2 \\in \\fF satisfies \\|\\gamma_1\\| < 2T_1, \\|\\gamma_2\\| < 2T_2 with T_1 T_2 = T, and \\langle e_1, \\gamma_1 \\gamma_2 v_0 \\rangle > T/100. As noted explicitly in the proof of eq:fincK (Section 5.2), this gives a \\asymp T. Consequently, a and a' are positive integers of size O(T), and the divisor sums over \\tilde q_1 \\mid a^2, \\tilde q_1' \\mid (a')^2, and h \\mid a are bounded by O_\\varepsilon(T^\\varepsilon).", "hypothesis_check": "All elements of \\fF satisfy T/100 < a \\ll T by definition eq:fFdef.", "affected_claims": [], "revised_status": "not_checked", "revised_quote": "", "revised_reasoning": "No later edition was supplied for comparison."}, {"finding_id": "finding-3289f7db80d832610970", "outcome": "packet_context", "severity": "none", "source_quote": "Apply \\eqref{eq:spec3} to the innermost sum, getting", "reasoning": "All prerequisites for applying eq:spec3 and eq:fFTbnd are established in the full manuscript. Section 3.1 (following eq:fFTbnd) explicitly identifies \\ff \\in \\fF with \\gamma \\in \\fF (preserving multiplicity from \\gamma = \\gamma_1 \\gamma_2 in eq:fFdef) and sets a = a_\\gamma = \\langle e_1, \\gamma v_0 \\rangle. For every divisor h \\mid a with h > H, since 0 < a \\ll T = N^{1/100} (by eq:TXNis), we have 1 <= h <= a \\ll N^{1/100} < N, satisfying the hypothesis 1 <= q < N of Lemma lem:spec3. Applying eq:spec3 with q = h and r = 0 bounds the inner sum by O(T^\\delta h^{-\\eta_0}) = O(T^\\delta H^{-\\eta_0}), and eq:fFTbnd gives #\\fF \\ll T^\\delta for the outer sum.", "hypothesis_check": "The modulus h satisfies 1 <= H < h <= a \\ll T = N^{1/100} < N, and the family parameters T_1, T_2 are fixed in eq:TT1T2 and eq:cCis as required by Lemma lem:spec3.", "affected_claims": [], "revised_status": "not_checked", "revised_quote": "", "revised_reasoning": "No later edition was supplied for comparison."}, {"finding_id": "finding-9360b6ebc9c6ea156988", "outcome": "packet_context", "severity": "none", "source_quote": "By \\eqref{eq:His} and \\eqref{eq:fuIs}, this is a power savings, as claimed.", "reasoning": "The scale relations needed to convert the T-power saving into an N-power saving are explicitly defined in the full manuscript. Equation eq:TXNis (Section 3) sets T = N^{1/100} and X = N^{99/200} so that TX^2 = N. Together with eq:gT1def (1 < \\Theta_1 < \\delta), eq:Q0is (Q_0 = T^{(\\delta-\\Theta_1)/20}), eq:fuIs (U = Q_0^{\\eta_0^2/100}), and eq:His (H = U^{10/\\eta_0}), we have (X^2/T) T^{2\\delta} = X^2 T \\cdot T^{2(\\delta-1)} = N T^{2(\\delta-1)} and U^6 H^{-\\eta_0} = U^{-4} = N^{-(\\delta-\\Theta_1)\\eta_0^2/50000}. Taking \\varepsilon > 0 sufficiently small yields the claimed bound N T^{2(\\delta-1)} N^{-\\eta}.", "hypothesis_check": "The global parameter definitions in eq:TXNis, eq:Q0is, eq:fuIs, and eq:His are in force throughout Section 7.", "affected_claims": [], "revised_status": "not_checked", "revised_quote": "", "revised_reasoning": "No later edition was supplied for comparison."}]}