# Dependency-guided review

No theorem verdict is inferred from local votes, scheduling order or source-quote matches.

Source `9939002e09d4f1726684edebc860d0b6f9dce839e4ea6761c41c4660ef932f64`; shared map `fc1b462b5c54d3282fe96069e1139bfefe4706972052db7894d3b6948fb5d076`.

41 claims and 25 narrative tasks; all mathematical body characters assigned.
Map completeness and external references remain unverified. Each local result is conditional on its stated inputs.

Usable assessments: 66/73. New reservations $20.532268; prior reservations $0.000000; total budget $25.00.

Arbitration: required; 64 queued cases. This queue is offline and does not submit generation.

Scheduling cycles: []. Cycles remain unresolved; grouped scheduling does not discharge them.

## Wave 0

eq:cIQ3def, eq:cKzBnd, eq:cRfuIs, eq:cSfbnd1, eq:decayMtrx, eq:fincK, eq:gls, eq:modBndaEqAp, eq:modBndaNeqAp, eq:vgIs, lem:GGq, lem:kEllD, lem:line:1307, lem:spec0, lem:spec3, 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:73512, narrative:86590, narrative:92045, narrative:93454, narrative:98161, narrative:99181, th_sg, thm:CircMeth, thm:IQM, thm:IQX, thm:Vin, thm:cMNtoMNU, thm:specGap

### eq:cIQ3def — gpt-6.1-sol

Delivery: completed; local status: defective.

The stated prefactor follows from the proposed input eq:IQbnd2, M=XT, and the asserted trivial bound for lambda_f. However, the proof replaces Fourier decay by an unsupported exact frequency cutoff. Consequently, the displayed argument does not establish the lemma as written; this is not a counterexample to the lemma itself. Several definitions needed for uniformity are also absent. No external theorem is imported: the assessment uses displayed algebra and elementary properties of finite Fourier sums. Model knowledge alone is not treated as dated evidence of availability before the recorded cutoff, 2012-05-24.

Conditional inputs used: eq:IQbnd2, eq:Mis, eq:glfDef

- **error**: Smallness of the quadratic phase does not make this finite Fourier sum vanish outside the indicated range. Even at beta=0, a smoothly weighted lattice sum generally has nonzero Fourier coefficients beyond such a cutoff. Appropriate smoothness can give rapid decay, but the proof supplies neither a quantitative decay estimate nor control of the discarded frequencies after summation against |S|. The remaining obligation is to show that the full four-frequency expression is bounded by the asserted truncated expression, or to state and bound a retained remainder. Pointwise rapid decay alone does not automatically establish that sharp truncation.

  Source: "there is contribution  only if $nx/q_{0}, my/q_{0} \\ll 1$"

- **unverified**: The supplied expansion uses nonnegative residue representatives, whereas Fourier localization is measured by distance to an integer. Frequencies near q0 represent small negative frequencies and need not be negligible. The restriction n,m << u q0/X therefore requires centered representatives, or explicit inclusion of both endpoints, together with periodicity of the modular factors. The supplied proof does not explain this change of representation.

  Source: "\\sum_{0\\le n,m<q_{0}}"

- **context**: This support assertion requires a definition of Upsilon, which is not supplied. Its smoothness and uniform derivative bounds are also needed for any Fourier-decay argument. The phase estimate additionally uses a uniform coefficient/size bound f(x,y)=O(T(X/u)^2) for every form under consideration; that bound and the definition of the family are absent. These are prerequisites, not consequences of Q>=X.

  Source: "Since $x,y\\asymp X/u$"

- **map_correction**: The three mapped dependencies are relevant but incomplete. To replace u q0/X by UQ/X requires, in addition to u<U and q asymp Q, a relation such as q0<=q. The referenced definition eq:tilQis is absent. Definitions of S, the diagonal/off-diagonal quantities, and the family of forms are also needed to specify exactly what is being bounded. These are missing dependency/context edges, not evidence that the three supplied premises have been established.

  Source: "recall the notation \\eqref{eq:tilQis}"

- **context**: Conditional on this bound and a justified frequency restriction, the numerical factor is correct: the beta interval has length O(1/(QM)), the product of the two lambda bounds is O(X^4/u^4), and M=XT gives U X^3/(QT u^4). Taking absolute values makes this step applicable to either relation a'=a or a'!=a. Thus the obstruction is localization and its prerequisites, not the displayed power counting.

  Source: "In this range, we give $\\gl_{f}$ the trivial bound of $X^{2}/u^{2}$."

- **error**: There is an upstream sign mismatch in the supplied setup: opening the square of amplitudes containing e(-a beta) produces e(beta(a'-a)), not e(beta(a-a')). This does not affect the absolute-value bound sought here, but eq:IQbnd2 is not literally the displayed square expansion with the supplied conventions. Its use above remains conditional, as required for supplied dependency statements.

  Source: "\\overline{\\gl_{f'}\\left(X,\\gb;\\frac {n'}{q_{0}},\\frac {m'}{q_{0}},u\\right)}\ne(\\gb (a-a'))"

Missing context: Definition and uniform support, smoothness, and derivative bounds of Upsilon; parameter conditions sufficient for the asserted lattice-count bound.; Definitions of f, frak f=f-a, the family frak F, and the uniform O(T) coefficient bounds used in estimating the quadratic phase.; Equation eq:tilQis defining q0 and u0, including the relation between q0 and q.; Definition eq:cSdef, its residue periodicity, and precise definitions of I_Q^(=) and I_Q^(!=).; A quantitative Fourier-tail estimate and a summation argument sufficient to justify the stated four-frequency truncation, including any convention for negligible errors and signed residue representatives.

### eq:cKzBnd — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied proof has an algebraic sign inconsistency and an unjustified equality between classes and residue solutions. The primitive-representation reduction and subsequent local counting are otherwise valid conditional on the displayed negative-square congruence, but that congruence does not follow from the preceding determinant equation. This is a local proof assessment, not a counterexample to the lemma. No external result is imported beyond the 2012-05-24 cutoff; later knowledge cannot be excluded from model weights, but is not used as evidence here.

Conditional inputs used: eq:ApBpCpABC, eq:BtoZ1

- **error**: Reducing this equation modulo z₁ gives B² ≡ +4a² (mod z₁), not the negative-square congruence displayed in eq:BtoZ1. Consequently, the subsequent reduction to B₁² ≡ −1 does not follow. For example, when a=1 and z₁=3, the positive-square congruence has two solutions and the displayed negative-square congruence has none. This is not merely an equality-versus-upper-bound issue.

  Source: "-4a^{2}=z_{1}C-B^{2}"

- **context**: The preceding context uses this normalization, whereas the target proof asserts z₁C−B²=−4a². The change-of-variables formula preserves AC−B² because its multiplier is (det M)²=1. Thus the two equations cannot describe equivalent forms with the same nonzero a. If 'determinant −4a²' means the ordinary discriminant 4(B²−AC), the preceding context is consistent with that terminology, but the target proof's determinant equation and congruence still have incorrect normalization. The intended convention must be supplied.

  Source: "$AC-B^{2}=a^{2}$"

- **error**: Normalization of B modulo z₁ provides representatives, not a bijection between equivalence classes and roots. Under the GL(2,Z) equivalence used in the supplied context, reflection sends B to −B; an additional unipotent transformation normalizes it modulo z₁. Hence distinct residues can yield equivalent forms. Moreover, counting all roots need not enforce primitiveness. Only an upper bound by the number of roots is justified or needed.

  Source: "So the number of inequivalent  such $f_{1}$ is equal to"

- **context**: Conditional on the negative-square congruence actually displayed, the local estimate checks out. When 2f≥e, there are p^{floor(e/2)} roots. Otherwise, after removing the unit part of 2a, roots have valuation f and reduce to roots of −1 modulo p^{e−2f}, with p^f lifts. For odd p there are at most two such roots; for p=2 there is one modulo 2 and none modulo 4 or higher. The omitted unit rescaling is legitimate but should be stated.

  Source: "If $2f\\ge e$, then the number of local solutions is at most $p^{e/2}$."

- **context**: The opening reduction is valid for positive z: w² divides z, and the divided representation vector is primitive. Bézout completion gives a unimodular matrix with that vector as its first column. Summing over possible z₁=z/w² costs at most the divisor count. Conditional on the required root bound, the final epsilon bookkeeping is valid by using smaller exponents for the two subpower factors. Their product is subpower: primewise, (e+1)2 is eventually bounded by p^{epsilon e}, and the finitely many remaining primes contribute a bounded constant.

  Source: "The number of divisors $z_{1}$ of $z$ is $\\ll_{\\vep} z^{\\vep}$, completing the proof."

- **map_correction**: This dependency is an intermediate equation inside the target proof, not an independently established premise. Its class-count equality and its connection to the determinant equation fail as written. The map should not treat its full equality chain as verified input. The proof anchor is present; this is not an anchor-location defect.

  Source: "\\label{eq:BtoZ1}"

Missing context: The intended definition of 'determinant −4a²' and its exact relation to AC−B² and the ordinary discriminant 4(B²−AC).; The precise primitiveness convention: gcd(A,B,C)=1 or gcd(A,2B,C)=1. This distinction does not obstruct counting all roots as an upper bound, but matters to the asserted equality.; Confirmation that the target uses the GL(2,Z) equivalence specified in the preceding excerpt, rather than proper SL(2,Z) equivalence.

### eq:cRfuIs — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The displayed derivation is algebraically correct conditional on the arithmetic definitions and hypotheses permitting Poisson summation. In the explicitly adopted even-u case, the change of variables has Jacobian 1/(u²q₀²), produces the positive residue-class phase e_{q₀}(nk+mℓ), and yields the stated frequencies. The q₀² normalization in S_f then leaves the claimed prefactor 1/u². No local sign or normalization error is apparent. The packet does not establish the weight's regularity or all arithmetic domain conditions, so unconditional applicability remains unchecked.

Conditional inputs used: eq:cRffuIs, eq:cSfDef

- **unverified**: The definition and regularity of Upsilon are absent. For example, Upsilon in C_c^infinity(R), with X and u nonzero, would make the transformed summand Schwartz and justify Poisson summation, absolute convergence, and the subsequent rearrangements. The exact remaining obligation is to supply the actual weight hypotheses and verify that they justify this application. This is missing context, not a demonstrated failure of Poisson summation.

  Source: "Apply Poisson summation to the bracketed term above:"

- **context**: Separating the sum into residue classes requires e_{q₀}(r u₀ f(x,y)) to depend only on x,y modulo q₀. Integer polynomial coefficients suffice, but their integrality is not stated in the supplied excerpts; the referenced definition eq:ffVdef is missing. Homogeneity itself is supplied and correctly used.

  Source: "f(x,y)=Ax^{2}+2Bxy+Cy^{2}"

- **context**: This is the declared domain of S_f. Its use here with second argument r u₀ requires gcd(r u₀,q₀)=1. The supplied reduction proves gcd(u₀,q₀)=1, but the setup does not explicitly supply gcd(r,q₀)=1. An earlier assumption gcd(r,q)=1 would suffice because q₀ divides q. Without that context, the argument has not checked the definition's stated domain, although the finite-sum identity itself does not require coprimality.

  Source: "fix $r$ with  $(r,q_{0})=1$"

- **map_correction**: The definitions in eq:tilQis are a direct proof input: they justify replacing the rational quadratic phase by e_{q₀}(r u₀ f(x,y)). They are present in the setup but absent from the supplied dependency list. Both listed dependency edges are otherwise appropriate.

  Source: "so that $u^{2}/q=u_{0}/q_{0}$ in lowest terms, $(u_{0},q_{0})=1$."

Missing context: The definition of Upsilon and its decay or support and smoothness assumptions, sufficient to justify the stated Poisson formula and summation rearrangements.; The relevant part of eq:ffVdef establishing that f has integer coefficients, or otherwise establishing the modular periodicity used in the proof.; The parameter conventions establishing q≥1, nonzero even u, X≠0, and gcd(r,q₀)=1, typically through gcd(r,q)=1.; A dated source/version for the invoked Poisson theorem is not supplied. Its historical admissibility is not independently documented here. No external text was inspected or later result used; latent model knowledge is not dated historical evidence.

### eq:cSfbnd1 — gpt-6.1-sol

Delivery: completed; local status: defective.

The displayed odd-modulus evaluation conditionally yields the claimed bound. However, the proof expressly proposes including even moduli, and the bound with constant 1 fails at q0=2 for the normalized sum displayed. The omitted “above conditions” must be supplied to determine whether any hidden restriction excludes this counterexample. This is a local assessment, not a verdict on the paper’s main theorem.

Conditional inputs used: eq:ABCdef, eq:Fv, eq:disc, eq:SfEval

- **error**: The advertised even-modulus extension is false without additional restrictions or a changed constant. The proof identifies S_f with q0^(-2) times the complete sum of e_q0(r f(k,l)+nk+ml). Set q0=2, r=1, n≡A and m≡C modulo 2. Since f(k,l)≡Ak+Cl modulo 2, every summand equals 1. Thus S_f=1>2^(-1/2). This works for every integral form of the displayed shape, including primitive ones. It is a direct calculation, not an imported result.

  Source: "Assume for simplicity $(q_{0},2)=1$; similar calculations are needed to handle the $2$-adic case."

- **context**: The preceding definition and complete hypotheses are absent. The proof explicitly recalls (r,q0)=1, but the supplied statement does not specify the permitted moduli or restrictions on n,m. If earlier conditions exclude q0=2 or the chosen residues, that must be documented; otherwise the counterexample applies.

  Source: "With the above conditions,"

- **unverified**: Primitivity does not imply that the original coefficient C is a unit at every prime. For odd p, the case p dividing A and C but not B requires an invertible change of variables, not merely exchanging coordinates. The argument needs to state that reduction and its effect on the linear coefficients n,m. Binary primitivity itself also uses the prerequisite that each orbit quadruple is primitive, not merely the definition gcd(B_gasket)=1.

  Source: "we have that $(A,B,C)=1$;       \n          \n assume henceforth that $(C,q_{0})=1$, say."

- **context**: Conditional on the displayed odd-modulus evaluation, this final inequality is correct: all phase and symbol factors have modulus at most 1, and sqrt(tilde q0)/q0≤q0^(-1/2), since tilde q0=(a²,q0)≤q0. The square completions and the divisibility condition nC≡mB modulo tilde q0 are consistent with AC−B²=a². This does not establish the omitted unit-coordinate reduction or the even case.

  Source: "The claim then follows trivially."

- **error**: The argument permits q0=p^j, so the standard symbol in the stated Gauss-sum formula is the Jacobi symbol, not the Legendre symbol unless j=1. This is a notation correction rather than the substantive obstruction to the bound.

  Source: "where $({\\cdot\\over q_{0}})$ is the Legendre symbol."

- **map_correction**: These references concern the subsequently defined paired average S. They are applications/context, not proof inputs for the individual-sum bound.

  Source: "This sum also\nappears naturally\nin the minor arcs analysis, see \\eqref{eq:IQbnd1} and \\eqref{eq:IQbnd2}."

- **map_correction**: An explicit proof is present in the supplied slice despite proof_anchor_missing=true. That flag is a mapping limitation, not a proof defect. Moreover, eq:SfEval is an intermediate result inside this same proof, not an independently established prerequisite.

  Source: "\\begin{proof}\nWrite $\\cS_{f}$ for $\\cS_{f}(q_{0},r;n,m)$."

Missing context: The preceding definition of S_f, including its normalization, additive-character convention, and all conditions on q0,r,n,m and the form family.; The orbit-primitivity statement connecting primitivity of the gasket to primitive curvature quadruples.; The invertible coordinate reduction ensuring a unit quadratic coefficient for each odd prime power, with corresponding transformation of n,m.; Any omitted restriction that excludes the q0=2 counterexample; otherwise the even-modulus assertion cannot hold as stated.; The actual cited 2004 text and equation (3.38), rather than only its bibliography entry, if the exact Gauss-sum evaluation is to be accepted as an external input.

### eq:decayMtrx — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The estimate is attributed directly to Kontorovich–Oh, Proposition 5.3, but that proposition has not been supplied or verified. The following bisector-counting discussion is not its proof. For Θ≥2 the bound follows from Cauchy–Schwarz, provided the Sobolev norm dominates the Hilbert norm. The substantive range 1<Θ<2 requires verification of the cited result, particularly its treatment of invariant vectors and its exact decay exponent. The missing proof anchor is a mapping limitation, not an established proof defect.

Conditional inputs used: external:KontorovichOh2011

- **unverified**: This is a citation-based assertion, with no local derivation in the supplied scope. It remains necessary to inspect Proposition 5.3 and verify its group, representation hypotheses, parameter normalization, Sobolev order, implied-constant dependence, and exact exponent without an additional epsilon or polynomial factor. No defect follows merely from the absent proof anchor.

  Source: "\\begin{thm}[{\\cite[Prop. 5.3]{KontorovichOh2011}}]"

- **context**: The definition of the complementary-series parameter and its endpoint convention is missing. For 1<Θ<2, the trivial representation must be excluded by this hypothesis or separately. If 'complementary series' means only the nontrivial representations with 1<s<2, the trivial representation passes the stated exclusion but violates the conclusion: for unit vectors its coefficient is 1, whereas along a_t the asserted right-hand side tends to zero. Whether this is an actual omission depends on the manuscript's unsupplied conventions.

  Source: "Let $\\gT>1$ and $(\\pi,V)$ be a unitary representation of $G$ which does not weakly contain any complementary series representation with parameter $s>\\gT$."

- **context**: The target uses an undefined Sobolev norm. Relation evidence supplies a candidate involving first and second derivatives, but does not identify the Lie algebra basis, vector domains, or constant conventions. These are needed to check uniformity over all smooth vectors. The Frobenius exponent itself is consistent with Cartan coordinates: ||a_t||_F²=e^t+e^(-t), so the asserted decay is comparable to e^(-(2-Θ)t). For Θ≥2, Cauchy–Schwarz suffices if S(v)≥||v||₂, since every g in SL(2,C) has Frobenius norm at least √2.

  Source: "\\cS v\\cdot\n\\cS w"

- **map_correction**: The Vinogradov references occur after the target theorem ends, in a new subsection introducing a different ingredient. The supplied edges concern bisector counting and a Cartan-coordinate description, not a proof of the matrix-coefficient estimate. They should not be treated as dependencies of eq:decayMtrx.

  Source: "\\subsection{Effective Bisector Counting}"

- **context**: The recorded cutoff is 2012-05-24. The cited 2013 journal version cannot establish pre-cutoff availability. The preprint identifier suggests an earlier candidate, but the packet supplies neither its dated metadata nor its contents; availability of the needed statements in that version remains unverified. Model weights may retain later knowledge, but no later theorem or proof is used here to discharge an original obligation.

  Source: "\\newblock Princeton University Thesis 2012, {\\tt arxiv:1204.5498v1}."

Missing context: The statement of Kontorovich–Oh Proposition 5.3 in the cited 2011 version, including all hypotheses and norm conventions.; The manuscript's definition and parameter range of complementary series, including whether the trivial representation at the endpoint is covered or invariant vectors are otherwise excluded.; The complete definition of S, its Lie algebra basis, its domain on smooth vectors, and the allowed dependence of the implied constant on Θ and the representation.; Only if Vinogradov is proposed as an actual proof input: dated metadata and the relevant statements from arXiv:1204.5498v1. Its present edges appear incidental.

### eq:fincK — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied proof contains an incorrect completion-of-squares identity. A corrected elementary argument proves the boundedness of distinct equivalent forms, conditional on the asserted uniform coefficient bounds and a comparable to T. If the family counts representations or repeated forms, an additional bounded-multiplicity argument is required. This does not refute the lemma. No external theorem is imported; potentially later model knowledge is not treated as dated evidence.

Conditional inputs used: eq:ABCdef, eq:disc, eq:fFdef

- **error**: Since AC-B²=a², the correct identity is A'=C(i+gB/C)²+g²a²/C, not the displayed expression with 4a²/C. Consequently, the following inequality g²≤A'C/(4a²) is not justified. New elementary repair, separate from the supplied proof: assume |A|,|B|,|C|,|A'|,|C'|≤KT and a≥cT. Then AC=B²+a²>0 and |A|,|C|≥c²T/K. The form is definite, and equivalence preserves its sign, so the corrected identity gives |A'|=|C|(i+gB/C)²+g²a²/|C|. Hence g²≤|A'C|/a²=O(1), while (i+gB/C)²≤|A'|/|C|=O(1) and |B/C|=O(1), yielding i=O(1). Applying the same argument to C' bounds h and j. There are therefore only O(1) integral transformation matrices and distinct resulting forms. Primitivity and the determinant restriction on these matrices are not needed for this counting step.

  Source: "g^{2} {4a^{2}\\over C}"

- **context**: The proposed dependencies explain the intended size argument: the product-shell definition should bound the coefficients above, its e1 condition should give a>T/100, and eq:disc supplies AC-B²=a². However, the matrix norm and its relation to multiplication and the coordinates of γv0 are not supplied. Thus these uniform bounds remain conditional rather than established here. The unsigned nonnegative-square argument also presupposes positive definiteness; the sign-invariant new repair above avoids that additional sign assumption.

  Source: "A,B,C\\ll T,"

- **unverified**: The proof bounds distinct coefficient triples, not automatically entries in an indexed or repeated family. The supplied family discussion explicitly permits nonunique decompositions and is truncated while discussing repeated forms. If the cardinality counts distinct shifted polynomials, this issue disappears because a is fixed. If it counts pairs or group elements, a uniform bound on fibers over each shifted polynomial is still needed; the displayed coefficient argument does not establish it.

  Source: "the decomposition $\\g=\\g_{1}\\g_{2}$ in \\eqref{eq:fFdef} need not be unique"

- **map_correction**: The three supplied dependency edges are relevant conditional inputs, but the map omits eq:ffVdef, which defines the passage from family elements to unshifted and shifted polynomials. The counting convention for this passage is also necessary to interpret the target cardinality.

  Source: "\\ff_{\\g}(x,y):=\nf_{\\g}(x,y)\n-a_{\\g}"

Missing context: The matrix-norm definition and uniform estimates linking the two norm shells to |A|, |B|, |C| and |a|=O(T), with constants independent of T and the equivalence class.; The complete family passage specifying whether its cardinality counts distinct polynomials, group elements, or factorization pairs.; If multiplicities are counted, a uniform O(1) bound on the number of counted family entries producing any fixed shifted polynomial.

### eq:gls — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The spectral statement is consistent with the supplied geometrically finite, discrete, non-elementary, infinite-volume setup, but its substantive assertions are attributed to external results whose exact statements and dated versions are absent. The figure is not a proof dependency. The subsequent congruence-spectrum discussion also needs an explicit continuation of the hypothesis δ>1 and clarification when no second discrete eigenvalue exists. These are local verification and scope limitations, not a full-theorem verdict.

Conditional inputs used: 

- **unverified**: No proof or inspected external theorem is supplied for the spectral decomposition, finiteness of the subthreshold list, simplicity of its lowest eigenvalue, the δ>1 criterion, or the formula λ₀=δ(2−δ). The missing proof anchor is a mapping limitation, not itself a proof defect. Verification requires exact results covering geometrically finite, non-elementary, infinite-covolume discrete subgroups of SL(2,C), including any torsion or cusp qualifications.

  Source: "The spectrum above $1$ is purely continuous, and the spectrum below $1$ is purely discrete."

- **context**: Together with the preceding discreteness and geometric-finiteness assumptions, these are the stated hypotheses for the theorem; the additional arithmetic hypothesis appears only afterward. Conditional on the supplied conclusion δ<2, the proposed eigenvalue passes the elementary check: if 1<δ<2, then 0<δ(2−δ)<1. The implications relating geometric finiteness, covolume, and limit-set dimension are not proved in this packet.

  Source: "We assume that $\\G$ is non-elementary (not virtually abelian), so $\\gd>0$, and moreover that $\\G$ is not a lattice,"

- **map_correction**: The edge fig:lim → eq:gls comes from the application remark, not the proof of the general spectral theorem. The orbit illustration establishes neither spectral assertions nor the numerical dimension. This dependency should be classified as illustrative background rather than a proof input.

  Source: "In our application to the Apollonian group, the limit set is precisely the underlying gasket, see Fig. \\ref{fig:lim}."

- **unverified**: For the Apollonian application, the needed conclusion is δ>1; the numerical approximation is stronger than necessary. Neither a dimension estimate nor a proof identifying the relevant lifted group's limit set with the gasket is supplied. The illustration cannot establish these application prerequisites.

  Source: "\\gd\\approx 1.3...>1."

- **context**: The ensuing notation λ₀(q), λ₁(q), … presupposes δ>1, whereas the general setup also permits δ≤1. The added condition Γ<SL(2,Z[i]) alone does not supply δ>1. Even with δ>1, the theorem does not guarantee a second discrete eigenvalue. The intended restriction to the Apollonian application and the meaning of λ₁(q) when absent need clarification. Finite index follows directly from the finite reduction target; equality of base eigenvalues additionally uses finite-index invariance of the limit-set dimension and the cited spectral formula.

  Source: "As in \\eqref{eq:gls}, write"

- **context**: This is explicitly heuristic, not a proof of the theorem. For a precise construction, the displayed point indicators must represent Dirac masses, the weak-* topology must be on the compactification including the boundary, and convergence, boundary support, and the Poisson-kernel exponent must be specified. None of these later explanatory claims independently verifies eq:gls.

  Source: "Roughly speaking, $\\mu$ is the weak$^{*}$ limit as $s\\to\\gd^{+}$ of the measures"

Missing context: Exact cited theorem statements and dated source versions establishing the spectral assertions under all stated hypotheses, available by the recorded cutoff 2012-05-24.; The precise Apollonian subgroup/lift used in SL(2,C), together with support for geometric finiteness, its limit-set identification, and δ>1.; An explicit δ>1 restriction for the congruence-spectrum discussion and treatment of an absent second discrete eigenvalue.; If the Patterson–Sullivan construction is intended as more than exposition, its compactification, convergence statement, normalization, and Poisson-kernel formula.

### eq:modBndaEqAp — gpt-6.1-sol

Delivery: completed; local status: defective.

The prime-partition argument and final exponent comparison are sound conditional on a correctly formulated, well-defined intermediate bound. However, the printed intermediate bound uses a support condition inconsistent with the supplied evaluation of the quadratic sum, so it does not justify the subsequent use of integral L and L'. Additional unresolved prerequisites concern modular inverses, the prime 2, and the asserted extension to composite moduli. This is a local proof assessment, not a disproof of the lemma.

Conditional inputs used: eq:15, eq:Ldef, eq:cP1, eq:cP2, eq:cS1, eq:cSdef, eq:fmnfp, eq:modBndaEqAp1, eq:pr2, eq:tildQdef

- **error**: This indicator, appearing in both eq:cS1 and eq:modBndaEqAp1, disagrees with the supplied evaluation eq:SfEval, whose support is nC≡mB modulo tilde q_0. The latter condition is also required for L=(Cn−Bm)/tilde q_0 to be integral. The two conditions are not equivalent under the supplied hypotheses. Consequently, the intermediate bound as printed can discard supported terms and does not supply the integrality used later. The analogous primed indicator has the same problem.

  Source: "nC\\equiv 2mB(\\tilde q_{0})"

- **context**: The proof uses the inverse of a_1 modulo p^j. If v_p(a^2)>j, then a_1=a^2/p^j remains divisible by p, so this inverse does not exist. Eq:tildQdef guarantees invertibility only modulo q_1, which is 1 in this case. A convention or separate treatment for the entire coefficient involving (a^2,p^j) is missing. Invertibility of C and C' modulo the relevant prime powers is also needed but not supplied.

  Source: "a^{2}=a_{1}(a^{2},p^{j})"

- **context**: Conditional on integral L, the determinant identity, and invertible C, the left side of eq:15 already equals f(m,−n) modulo p^{ceil(j/2)}: C^{-1}[(AC−B²)m²+(Cn−Bm)²]=Am²−2Bmn+Cn². The primed identity is identical. Thus eq:fmnfp follows directly. Subtracting the common a is unnecessary; it also preserves the congruence because a=a'.

  Source: "and subtracting $a$ from both sides of \\eqref{eq:15}"

- **context**: This final inference checks out conditionally. For odd p in P2, noncongruence gives valuation at most ceil(j/2)−1≤j/2. For P1, the congruences imply that the product of p^{ceil(j/2)} divides the nonzero integer Z, giving eq:cP1. Writing R=q/q_0≥1, the resulting bound is R^{9/2}(a²,q_0)q^{-5/4}q_0^{1/8}Z^{1/2}=R^{35/8}(a²,q_0)q^{-9/8}Z^{1/2}, which is at most the claimed R^5 bound. Both a=a' and Z≠0 are used essentially.

  Source: "Combining \\eqref{eq:cP1} and \\eqref{eq:cP2} in \\eqref{eq:modBndaEqAp1} gives the claim."

- **unverified**: The passage from a prime-power calculation to the displayed uniform composite-modulus bound is asserted without supplying the CRT factorization, transformed local parameters, or control of accumulated constants. This remains an exact proof obligation, rather than an established dependency.

  Source: "which is valid now without the assumption\n                                          \nthat $q_{0}$ is a prime power."

- **context**: The statement supplied does not explicitly restrict q_0 to odd integers. The proof requires this restriction for the inverse of 4 and the odd-modulus evaluations. Either an inherited odd-modulus hypothesis or a separate 2-adic argument is needed.

  Source: "continuing to omit the prime $2$."

- **unverified**: The exact bound and its hypotheses have not been supplied or inspected. No external theorem is imported in this assessment. Its admissibility must be checked against the recorded cutoff, 2012-05-24. Model knowledge may include later developments and is not evidence of historical availability.

  Source: "Hence we again apply Kloosterman's $3/4$th bound to \\eqref{eq:cS1}"

Missing context: The definition of S_f and the inherited hypotheses ensuring that C and C' are units modulo q_0.; A consistent support condition linking eq:SfEval, eq:cS1, eq:modBndaEqAp1, and the integrality of L and L'.; The interpretation of inverse expressions when v_p(a²)>j, and the scope of the omission of the prime 2.; A CRT derivation of the composite-modulus estimate with uniform constants, together with the exact dated source/version for any external bound actually used.

### eq:modBndaNeqAp — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied proof contains an incorrect congruence indicator when substituting eq:SfEval into eq:cS1. This invalidates that displayed identity, but does not disprove the lemma's bound. Conditional on a correctly obtained Kloosterman/Salié estimate, the final algebra gives exactly the claimed powers of q and q0. The external estimate, the prime-power reduction, and the omitted 2-adic case remain unverified. This assessment uses direct algebra and supplied excerpts, not model knowledge as dated external evidence.

Conditional inputs used: eq:Ldef, eq:SfEval, eq:tildQdef, external:Kloosterman1927

- **error**: Both factors of 2 conflict with eq:SfEval, whose support condition is nC ≡ mB modulo tilde q0, and with L=(Cn−Bm)/tilde q0. The displayed replacement condition does not even ensure L is integral. As an algebraic check of the substitution, take q=q0=9, u0=1, a=a'=3, f=f'=10x²+2xy+y², and n=m=n'=m'=1. Then AC−B²=a² and the displayed coprimality conditions hold. Eq:SfEval gives |Sf|=1/3 for each of the six unit r, so the correlation is 2/3; the new indicator instead makes eq:cS1 zero. Membership of this example in the manuscript's unspecified family is not asserted; the example checks the claimed algebraic substitution.

  Source: "\\bo_{\nnC\\equiv 2mB(\\tilde q_{0})\n\\atop\nn'C'\\equiv 2m'B'(\\tilde q'_{0})\n}"

- **context**: The packet does not supply the CRT factorization, a restriction to odd q, treatment of the p=2 factor, or the earlier reduction making both C and C' units. These are prerequisites, not consequences of the supplied notation. The case q0=1 also needs a convention or separate treatment. The full definition of S is truncated in its defining excerpt.

  Source: "Observe  that $\\cS$ is multiplicative in $q$, so we again consider the prime power case $q=p^{j}$, $p\\neq2$; then $q_{0}$ is also a prime power, since $q_{0}\\mid q$. As before, we may assume $(C,q_{0})=(C',q_{0})=1$."

- **unverified**: The packet defines tilde q0 and tilde q0', but does not identify the un-subscripted tilde q and tilde q' used here. Also, the inverses originally occur modulo q1 and q1', whereas this phase is written modulo q0. Their lifted interpretation must be specified. In particular, when q1=1, a1 can share a prime factor with q0, so an inverse of a1C modulo q0 need not exist; the original modulo-1 phase nevertheless vanishes.

  Source: "\\overline{a_{1}'C'}\n(L')^{2}\n\\tilde q'\n             \n-\n\\overline{a_{1}C}\nL^{2}\n\\tilde q"

- **unverified**: The needed result is a bound |Σ* χ(r)e_q(Ar+B r^{-1})| ≪ q^(3/4)(A,q)^(1/4), with A=a'−a, arbitrary relevant B, odd prime-power q, and χ the product of the two induced quadratic characters. The source must cover degenerate coefficients and imprimitive/trivial characters. External text was not supplied or inspected. Availability record: available_from for this exact result is unresolved; date_evidence is the bibliography's 1927 publication year; date_basis is bibliographic publication year only; version is the cited Acta Math. 49 paper, uninspected. No later result is used to close this obligation under the 2012-05-24 cutoff.

  Source: "The term in brackets $\\big[\\cdot\\big]$  is a Kloosterman- or Sali\\'e-type sum, for which we have an elementary bound \\cite{Kloosterman1927} to the power $3/4$:"

- **unverified**: Even if multiplicativity is granted, prime-power bounds with an unspecified absolute constant do not automatically give the stated global ≪ bound: multiplication can introduce a factor C raised to the number of prime divisors. A uniform global estimate or an explanation controlling these local constants is required; inserting an unstated q^epsilon loss would change the displayed claim.

  Source: "Observe  that $\\cS$ is multiplicative in $q$"

- **map_correction**: The references to narrative:115416 and eq:cI42bnd describe later applications and motivation, not proof inputs for this lemma. Their incoming dependency edges should not be used to justify the lemma. Also, the supplied slice contains an explicit proof despite the missing-proof-anchor flag; that flag is a mapping limitation.

  Source: "In the case $a=a'$, \\eqref{eq:modBndaNeqAp} only saves one power of $q$, and in \\S\\ref{sec:QXT} we will need slightly more; see the proof of \\eqref{eq:cI42bnd}."

Missing context: Complete definition of S and all inherited restrictions on q, q0, u0, the forms, and the family F.; Earlier reductions establishing multiplicativity, handling p=2 and q0=1, and permitting C and C' to be units.; Definitions of tilde q and tilde q', inverse-lifting conventions, and the q1=1 convention.; A dated, inspected source location containing the exact required Kloosterman/Salié estimate and its uniformity hypotheses.; Justification that local constants yield the global bound without an additional arithmetic factor.

### eq:vgIs — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

Conditional on the supplied subgroup identification and orbit-to-curvature inclusion, the lemma follows from the preceding construction of ξ_{x,y}. Its polynomial identity and coefficient integrality check directly. No external theorem is needed for this local inference. The subsequent Bernays counting assertion is a separate, incompletely documented consequence, and the congruence-subgroup discussion is not part of this lemma's proof. Later results potentially present in model knowledge are not used as evidence.

Conditional inputs used: eq:ABCdef, eq:Fv, eq:G1

- **context**: The coprimality hypothesis supplies the required matrix in Λ(2): y is odd, and Bézout gives u y−2x v=1 with u odd; replacing (u,v) by (u+2xt,v+yt) makes v even. Conditional on the supplied identification of Λ(2)'s image with Ξ, ξ_{x,y} therefore belongs to Γ. For every γ∈Γ, ξ_{x,y}γv₀ lies in the supplied orbit, so its fourth coordinate is a gasket curvature by eq:setB. Neither positivity of a_γ nor primitivity of the gasket is needed for this local step.

  Source: "whenever $(2x,y)=1$"

- **context**: For an integral orbit vector, F=0 modulo 2 gives a+b+c+d even; hence a+b−c+d is even. Expanding the supplied w_{x,y} gives 4(a+b)x²+2(a+b−c+d)xy+(a+d)y²−a, exactly the asserted expression. The adjacent discriminant identity also checks: 4(B²−AC)=F(a,b,c,d)−4a²=−4a². The generators of Ξ change only circles numbered 2–4, supporting the adjacent fixed-circle and tangency observation under the supplied geometric interpretation.

  Source: "Note from \\eqref{eq:Fv} that $B_{\\g}$ is integral."

- **map_correction**: The relevant proof material precedes the lemma: eq:setB, eq:xiXYdef and eq:wxyDef. These are supplied but absent from the frozen dependency list. The missing proof anchor is a mapping limitation, not a mathematical defect. eq:ABCdef is an internal definition and eq:binQuad is the lemma's conclusion, not an independent premise.

  Source: "Then again by \\eqref{eq:setB}, we have shown the following"

- **unverified**: This downstream assertion is not needed for the lemma. The Bernays text has not been inspected. To verify the stated consequence, one needs an applicable theorem covering the actual restriction (2x,y)=1, not merely unrestricted primitive representations, and a justified positive-definite choice of form. The discriminant calculation alone does not supply positive definiteness without a≠0 and A>0. This is an outstanding obligation for the attached counting claim, not a defect in the curvature lemma.

  Source: "that the number of distinct primitive values \nup to $N$\n assumed by a           \n positive-definite binary quadratic form  is of order at least $ N(\\log N)^{-1/2}$, proving \\eqref{eq:SarBnd}."

- **map_correction**: The Fuchs and Matthews–Vaserstein–Weisfeiler references concern the following congruence-subgroup discussion. The Graham–Lagarias reference attached to the later complex spin-cover conjugation likewise does not prove this lemma. eq:SarBnd and Bernays concern a downstream counting consequence, so their edges should not be treated as inputs to the curvature identity.

  Source: "The quotients $\\G/\\G(q)$ have been determined             \ncompletely\nby Fuchs \\cite{FuchsThesis}"

Missing context: The subgroup identification and orbit-to-curvature inclusion are supplied premises, not independently established external results in this assessment.; For the ancillary counting claim: the exact Bernays theorem, including primitive-representation and congruence restrictions, and verification of its hypotheses for the chosen form.; For any proposed external import: a dated source/version containing the needed result by the recorded cutoff, 2012-05-24. Bibliographic years alone do not verify theorem content or the relevant version.

### lem:GGq — gpt-6.1-sol

Delivery: completed; local status: defective.

With Γ(q) interpreted as the ordinary congruence kernel and SO_F as the full determinant-one isometry group, part (2) is false: modulo 7, −I belongs to SO_F but not to the image of Γ. This is checked directly below, without importing an external theorem. Parts (1), (3), and the following admissibility remark remain unverified from this packet. The absent proof anchor is a mapping limitation, not itself a proof defect.

Conditional inputs used: 

- **error**: Direct countercheck at q=7, which satisfies (q,6)=1: write F(x)=xᵀAx with A=2I−J and B(x,y)=xᵀAy. In the Clifford algebra defined by xy+yx=2B(x,y), each standard basis vector e_i has square 1, and the displayed reflection satisfies S_i(x)=−e_i x e_i. Consequently every even word representing an element of Γ acts by conjugation with an even product g of these vectors. If ~ reverses products, then g~g=1. Now take the orthogonal basis u₁=e₁, u₂=e₂−e₃, u₃=e₂+e₃−2e₄, u₄=3e₁+e₂+e₃+e₄. Its squared norms modulo 7 are 1,4,5,2. If conjugation by g were −I, g would anticommute with every u_i. Expansion in the Clifford monomial basis then forces g=c u₁u₂u₃u₄: an even monomial anticommutes with u_i exactly when it contains u_i. Hence g~g=5c², which cannot equal 1 since 3=5⁻¹ is nonsquare modulo 7. Thus −I is absent from the congruence image, although it preserves F and has determinant 1. The image is therefore a proper subgroup of the finite group asserted in (2), so even the abstract isomorphism cannot hold. This is an independent elementary diagnostic, not an imported result or a repair.

  Source: "\\G/\\G(q)\\cong\\SO_{F}(\\Z/q\\Z)."

- **context**: The supplied excerpts do not define Γ(q). The countercheck uses Γ(q)={γ∈Γ:γ≡I mod q}, as suggested by the projection and preimage language. Supply the actual definition and the intended meaning of SO_F over finite rings. A nonstandard use of SO_F for a smaller spin-image group would materially change the statement, but is not documented here.

  Source: "(1) The quotient groups $\\G/\\G(q)$ are multiplicative"

- **unverified**: The thesis text and exact theorem location are absent. Thus the packet does not verify multiplicativity, either stabilization assertion, or whether the cited theorem actually names the full orthogonal group rather than a smaller congruence image. No external theorem is imported here. The recorded cutoff is 2012-05-24; the bibliography reports 2010, but the version containing the required result has not been inspected. Model knowledge cannot establish historical availability or substitute for dated evidence.

  Source: "\\begin{lem}[\\cite{FuchsThesis}]\\label{lem:GGq}"

- **map_correction**: The edge eq:locA → lem:GGq is not a proof-input edge. The quoted reference occurs in the following consequence remark, and eq:locA concerns one example gasket. It does not establish the general quotient-group assertions.

  Source: "This of course explains all local obstructions, cf. \\eqref{eq:locA}."

- **unverified**: This conclusion needs more than quotient stabilization stated without orbit analysis. One must show that the relevant coordinate classes lift to every higher 2- and 3-power, that primes ≥5 introduce no coordinate obstruction for the primitive isotropic root vector, and that prime-power choices combine. Also, the supplied setup only gives B ⊇ ⋃ⱼ⟨eⱼ,Γv₀⟩, while admissibility is defined using all curvatures. Equality of the relevant coordinate residue sets for Γ and the full Apollonian orbit is not supplied. These are remaining obligations, not established consequences in this packet.

  Source: "The admissible numbers are precisely those\n residue classes $(\\mod 24)$ which appear  as some entry in the orbit of $v_{0}$ under $\\G/\\G(24)$."

Missing context: The exact definition of Γ(q), the finite-ring group SO_F, and any distinction between the full orthogonal group and the spin image.; The precise Fuchs thesis theorem, page, hypotheses, deposited version, and dated evidence that this version was available by 2012-05-24.; Proof or an accurately stated cited result for part (1) and both assertions in part (3).; Orbit-transitivity, coordinate-lifting, and full-orbit versus even-subgroup coordinate-residue arguments needed for the admissibility remark.

### lem:kEllD — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The supplied proof is valid under the usual convention that d is a positive integer modulus. The determinant divisibility justifies both completing the square and the otherwise abbreviated assertion that C is invertible in Case 2. The construction works also at p=2 and produces coefficients independent of m,n. No external literature is needed or imported to close this obligation.

Conditional inputs used: 

- **context**: This uses both hypotheses, not primitivity alone: since p divides d and AC−B², p dividing A forces p to divide B. Then gcd(A,B,C)=1 forces p not to divide C. Thus the asserted inverse of C modulo p^e exists.

  Source: "If $(p,A)>1$, then by primitivity, $(p,C)=1$."

- **context**: After multiplying the original congruence by the inverse of A, the remaining coefficient is A^{-2}(AC−B²), which vanishes modulo p^e because p^e divides d. The same calculation with A and C interchanged proves Case 2. Neither calculation divides by 2, so there is no exceptional dyadic case.

  Source: "(m+\\bar A Bn)^{2}-\\bar A ^{2}B^{2}n^{2}+\\bar ACn^{2}"

- **context**: The assembly preserves the implication for every m,n: the global linear form agrees with the chosen local form modulo each p^e. Explicitly, put D_p=d/p^e, choose u_p with D_p u_p≡1 modulo p^e, and sum D_p u_p k_p and D_p u_p ℓ_p to obtain k and ℓ. Their squared linear form is divisible by every prime-power factor of d, hence by d. At each prime dividing d, one coefficient is congruent to 1, proving gcd(k,ℓ,d)=1. For d=1, taking k=1 and ℓ=0 suffices.

  Source: "By the Chinese Remainder Theorem, there are integers $k$ and $\\ell$ so that $k\\equiv k_{p}(\\mod p^{e})$, and similarly with $\\ell$."

### lem:line:1307 — gpt-6.1-sol

Delivery: invalid_assessment; local status: no assessment.

### lem:spec0 — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied sketch does not establish the claimed uniformity in gamma_1: its smoothing inserts a perturbation between gamma_1 and gamma, where conjugation can amplify it without bound. The translated bump also lacks the asserted uniform Sobolev control. This is a defect in the supplied proof, not a counterexample to the lemma. Spectral and external inputs remain conditional.

Conditional inputs used: eq:RepDecomp, eq:decayMtrx, eq:gl0Qgl0, eq:specGap, external:BourgainKontorovichSarnak2010, external:LaxPhillips1982

- **error**: This does not follow uniformly in gamma_1. Writing k=gamma_1 gamma gives gamma_1 g^{-1} gamma h=(gamma_1 g^{-1} gamma_1^{-1})kh. Small g need not give a uniformly small conjugated perturbation. Thus the asserted inner/outer shell tests with width 10 eta are unjustified. For gamma=gamma_1^{-1}, the unperturbed product is the identity, while the perturbed product contains precisely this uncontrolled conjugation. Membership gamma_1 in Gamma permits reindexing the full-group sum, but does not remove the amplification.

  Source: "both $f(\\g_{1}g^{-1}\\g h)$ and $f(\\g_{1}\\g)$ are $1$, so their difference vanishes."

- **error**: The eta^{-5} scaling is appropriate for an unshifted six-dimensional L2 bump with two derivatives. The matrix coefficient, however, also uses Psi_{q,gamma_1}=R(gamma_1)Psi_q. Right-action derivatives of this vector involve Ad(gamma_1^{-1}); no uniform bound for its required Sobolev norm is supplied. Consequently the eta^{-10} product bound, with a constant independent of gamma_1, does not follow.

  Source: "The functions $\\psi$ are bump functions in six real dimensions, so can be chosen \nto have second-order Sobolev norms bounded by $\\ll \\eta^{-5}$."

- **context**: This requires a simple ground state whose representation at every intermediate level is exactly the normalized lift from level one. Equality of lowest eigenvalues alone does not establish that assertion. Conditional on this lift statement, the index scaling is natural. The spectral-gap exclusion passes to intermediate subgroups through the covering-space inclusion; their normality is unnecessary.

  Source: "Of course the projection onto the base representation is just $[\\G:\\tilde\\G(q)]^{-1}$ times the same projection at level one"

- **unverified**: The supplied bibliography does not verify the claimed shell estimate, its hypotheses, or its norm normalization. The section switches from SL2(C) to SO_F; transferring the supplied matrix-coefficient decay and integrating it over the stated norm ball also requires the spin-cover norm comparison and Haar-volume growth. These prerequisites are not supplied.

  Source: "apply \\cite{LaxPhillips1982}, bounding the count by"

- **map_correction**: lem:spec1 is downstream, not a premise. The family definition eq:fFdef and narrative:105898 also belong to subsequent applications. eq:lemLHS and eq:lemRHS are parts of this target, not independent inputs. Despite proof_anchor_missing=true, an actual sketch is present in source_slice; the anchor flag is a mapping limitation, not an additional proof defect.

  Source: "After proving the lemma below, we will use the argument as a template for the more complicated statement."

- **context**: Conditional on eq:NqErr with uniform constants, choosing eta=Y^{-epsilon/11} gives Theta_0=delta-epsilon/11. This elementary final step is correct; it does not resolve the preceding uniformity errors.

  Source: "Optimizing $\\eta$ and renaming $\\gT_{0}<\\gd$"

Missing context: Definitions of the SO_F norm, its relation to the SL2(C) Frobenius norm, and the relevant Haar-ball growth.; The complete Sobolev norm definition and a valid uniform estimate for the actual translated vectors.; Ground-state simplicity, normalized lifting, and spectral decomposition for every intermediate subgroup.; The exact Lax–Phillips counting theorem and hypotheses needed for the shrinking shell estimate.; For the right-sided assertion, the norm's inversion symmetry or another explicit reduction.; Dated external theorem texts available by 2012-05-24. Model knowledge, including possible later knowledge, is not evidence of historical availability.

### lem:spec3 — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied proof contains an incorrect stabilizer-index estimate: conditional on the stated full orthogonal-group reduction, the orbit of a primitive Descartes vector has order p^3, not p^2, at good primes. The accompanying residue-fiber estimate and both spectral-error balances therefore fail as written. There is also an uncontrolled change of variables in the lifting argument. Several elementary transitions are valid, but they do not close these gaps. This is a local proof assessment, not a disproof of the lemma.

Conditional inputs used: eq:1, eq:2, eq:3, eq:Fuc, eq:G1G, eq:TT1T2, eq:cCis, eq:fFdef, eq:fdIs, eq:lemRHS, eq:qToT1, eq:wStar

- **error**: This contradicts the proposed full-group reduction in the standard Descartes setting. Direct finite-field check: at a good split prime p, the four-variable Descartes form is equivalent to the determinant on 2×2 matrices. Nonzero null vectors are rank-one matrices, numbering (p²−1)²/(p−1)=(p−1)(p+1)². Left/right SL(2) actions preserve the determinant and act transitively on these matrices. Thus, conditional on eq:Fuc and primitive null v0, the vector-stabilizer index is asymptotic to p³, not p². The distinction between a vector and its projective line is essential.

  Source: "[\\G:\\tilde\\G(q)]\\asymp q^{2}"

- **error**: The factor q also undercounts admissible vector-orbit cosets: an orbit of order p³ distributed among p curvature residues has average fiber of order p². Consequently the stated uniform O(p) fiber bound cannot hold. Using vector cosets instead produces a spectral error of order T1^δ p² T2^Θ0. To dominate this by T^δ/p requires p³≤T2^(δ−Θ0), which is not ensured by the advertised range p<T2^((δ−Θ0)/2). The same problem affects the final q0 argument.

  Source: "T_{1}^{\\gd}\\\nq\\\n\\left(\n\\frac1{q^{2}}\\\nT_{2}^{\\gd}\n+\nT_{2}^{\\gT_{0}}\n\\right)"

- **unverified**: Primitivity does not ensure that an existing coordinate is a unit modulo composite q; for example (2,3,0,0) is primitive but has no unit coordinate modulo 6. An integral coordinate change can address this, but its coefficients and the transformed row coefficients must be controlled. No such control is supplied, whereas the later height bound depends on it.

  Source: "Since $v$ is a primitive vector, after a linear change of variables we may assume that $(v_{1},q)=1$."

- **unverified**: An unrestricted denominator-cleared solution need not admit a prime of the prescribed size avoiding its coordinate gcd. A primitive normalization, with integral z*, needs justification. Moreover, Case 1 was formulated for v0, while its reuse here requires a uniform finite-field orbit/fiber estimate for every nonzero reduction of v*. Neither prerequisite is supplied.

  Source: "such that $v_{*}\\not\\equiv0(\\mod q_{0})$"

- **context**: This contradiction is valid conditional on the height estimate and modular normalization: q divides positive d, while d≪T1^(10^28) and q≥T1^(10^29), for sufficiently large T1. The numerical exponent check also passes: 8^31<10^28. Dropping the family restriction, rational solvability of a consistent rational linear system, and clearing denominators are valid. Converting a hypothetical q0-saving into a q-saving additionally uses T=N^(1/100), not merely T=T1T2.

  Source: "which is incompatible with \\eqref{eq:fdIs} and \\eqref{eq:qToT1}"

- **map_correction**: eq:spec3 is the target conclusion, not an independent proof input. Equations 1, 2, 3, fdIs, qToT1 and wStar are internal proof stages. The map also omits the essential scale relation eq:TXNis and the other parts of lem:GGq needed for composite moduli and primes 2 and 3.

  Source: "bound the left hand side of \\eqref{eq:spec3} by"

Missing context: Explicit definitions of F, v0, the matrix norm and δ; confirmation that v0 is primitive and F(v0)=0.; A valid uniform congruence orbit/fiber estimate and spectral-error calculation covering every q<N and every residue r.; Height-controlled coordinates for the lifting argument and justified normalization of its integral solution.; Exact external theorem statements and hypotheses supporting orbit counting and the effective arithmetic Bezout bound.; A dated source/version record for FuchsThesis. Its availability by the 2012-05-24 cutoff is not established here.

### lem:spec3 — claude-opus-5-5

Delivery: provider_failed_or_incomplete; local status: no assessment.

### lm_local — gpt-6.1-sol

Delivery: completed; local status: defective.

The supplied proof contains false intermediate assertions and an unstated congruence invariant needed for its 2-adic induction. This does not disprove the lemma. Conditional on the subgroup and unipotent premises, the p≥5 matrix calculation, unit-entry factorization, and more-than-half argument check algebraically. The exceptional-prime argument requires the corrections and missing definitions identified below.

Conditional inputs used: eq:unip, eq_Gamma1

- **error**: The ensuing identification with all integral determinant-one matrices having b≡0 mod 4 is false for the two displayed generators alone. Modulo 4, γ1 is the identity and γ2 is lower unipotent, so every generated matrix has both diagonal entries 1. The asserted right-hand side contains −I, whose diagonal entries are 3 modulo 4. An earlier definition including ± generators could resolve the discrepancy, but that definition is not supplied. The odd-prime reduction assertion does not by itself resolve this integral-group error.

  Source: "It is well-known and easy to check that the group generated by $\\g_1$ and\n$\\g_2$ is"

- **error**: This does not follow from the stated conditions h_i≡I mod 4, x_i≡0 mod 2^(m−4), and Tr(x_i)≡0 mod 2^m. For example, take h_i=[[1,0],[4,1]] and x_i=2^(m−4)E12. Their sum has determinant 1−2^(m−2), not 1 modulo 2^m. Likewise, the displayed product linearization discards terms involving (h_i−I)x_j that need not vanish under the stated bounds. The exact remaining obligation is to establish a sufficiently strong invariant for the chosen factors—such as h_i≡I mod 16—and verify that it is preserved throughout the induction. The analogous p=3 argument also needs an identity-modulo-3 invariant for its chosen factors.

  Source: "$\\det(h_i+x_i)\\equiv1 \\;\\mod 2^m$"

- **error**: As printed, this says 2^(m−1)E21≡E21 modulo 2^m, which is false for the relevant m≥8. The misplaced factor appears typographical: the intended right-hand side presumably has the factor 2^(m−1). The other five displayed 2-adic spanning identities check directly.

  Source: "2^{m-1}\\mat{0}{0}{1}{0}+\\g_3\n0\\g_3^{-1}+\\g_3^2\n0\\g_3^{-2}\n2^{m-1}\\equiv \\mat{0}{0}{1}{0} \\mod 2^m,"

- **error**: The ambient group order is 48·64^6, not 46·64^6. At modulus 2, reduction to SL(2,F2) has kernel of size 8, giving 6·8=48; each subsequent reduction has a traceless-matrix kernel of size 64. This numerical error alone does not invalidate the final constant: even 3·48·64^6 is less than 10^13. The kernel-containment argument must nevertheless be justified first.

  Source: "|\\SL(2,\\Z[i]/(2^7))|=46\\cdot64^6."

- **context**: The packet supplies the alternating-product description but not the definition of Γ2. Membership claims in A3, A12, and A36 require, in particular, the appropriate powers of γ3 to lie in Γ2. The final index-to-word-length step also requires Γ1 and Γ2 to generate the quotient. These are missing prerequisites, not established facts in this assessment.

  Source: "h_1,\\ldots h_k\\in \\Ga_2/\\Ga_2(q)"

- **map_correction**: The eq:unip dependency is an intermediate result inside this branch and must retain the restriction p≥5. It cannot support the p=2 or p=3 cases. The eq_Gamma1 edge is relevant to both branches, but its statement needs the generator/sign clarification noted above.

  Source: "\\begin{proof}[Proof of Lemma \\ref{lm_local} for $p\\ge5$]"

Missing context: The complete definitions of Γ1, Γ2, their congruence subgroups, and A_k, including any ± generator convention and the quotient-generation assertion.; A stated and proved congruence invariant validating determinant preservation and product linearization in the exceptional-prime inductions.; If the proof of eq:unip is to be certified rather than treated conditionally, dated source/version evidence for its four-square-theorem input, available by 2012-05-24. No external text was inspected; model recall alone is not dated historical evidence.

### lm_local — claude-fable-5-1

Delivery: provider_failed_or_incomplete; local status: no assessment.

### lm_transference — gpt-6.1-sol

Delivery: completed; local status: defective.

The stated hypotheses allow empty subgroup–generator intersections, making the asserted bound undefined. Subject to well-defined subgroup averaging operators and second eigenvalues, the supplied finite-group argument supports the claimed constant 1/(2k^2). No external theorem is needed for this local proof. The surrounding application to the Apollonian group is conditional and is not established by this assessment.

Conditional inputs used: eq_TSG1, eq_TSG2

- **error**: These hypotheses do not ensure that S∩G_i is nonempty. For example, take G cyclic of order 6 with generator a, S={a,a^{-1}}, G_1=⟨a^2⟩ and G_2=⟨a^3⟩. Then G=G_1G_2, but both intersections are empty. Their averaging operators divide by zero, so the displayed conclusion is undefined. Moreover, the supplied definition introduces λ'_1 only for generating sets, whereas S∩G_i need not generate G_i. Trivial subgroups also require a convention for the nonexistent second eigenvalue. These are statement/domain defects, not a counterexample to the intended nondegenerate inequality.

  Source: "Let $G_1,G_2,\\ldots,G_k$ be subgroups of $G$ such that\nfor every $g\\in G$ there are $g_1\\in G_1,\\ldots,g_k\\in G_k$\nsuch that $g=g_1\\cdots g_k$."

- **context**: The substantive proof steps check directly when the spectral quantities are defined. A real unit eigenfunction can be chosen because T is real symmetric, validating the ordered correlation inequality. Averaging gives a displacement at least √2; telescoping the k-factor product gives a subgroup displacement at least √2/k, hence ||f_2||²≥1/(2k²). For H=G_{i_0}, the restricted regular representation decomposes over right cosets Hx into copies of L²(H). Orthogonality to H-invariants means zero sum on every coset, justifying eq_TSG1 by the subgroup spectral bound. The complementary average is a contraction, giving eq_TSG2. Combining them and taking the minimum gives exactly the stated constant. Empty complementary averages should be omitted when their coefficient is zero.

  Source: "We write $f_0=f_1+f_2$ such that $f_1$ is invariant under the elements\nof $G_{i_0}$ in the regular representation $\\pi$ and $f_2$ is orthogonal\nto the space of functions invariant under $G_{i_0}$."

- **map_correction**: lm_generation is an input to an application of lm_transference, not to its proof. Likewise, th_sg is a downstream conclusion, not a premise of this lemma. Selberg, Brooks and the optional Bourgain–Varjú alternative concern subgroup gaps in that application. Diaconis–Saloff-Coste, Sarnak, Shalom and KLN are comparison or attribution references, not necessary proof inputs here.

  Source: "Lemma \\ref{lm_generation} enables us to apply Lemma\n\\ref{lm_transference} with $k=2\\cdot 10^{13}$"

- **unverified**: The external texts and their hypotheses have not been supplied or inspected. This sentence therefore does not establish the subgroup-gap inputs or the surrounding theorem. No external result is imported into the local assessment, and later model knowledge is not treated as dated evidence. Any separate reliance on these references, including the Bourgain–Varjú alternative, requires the exact theorem and hypotheses together with available_from, date_evidence, date_basis and version establishing availability by 2012-05-24.

  Source: "Now \\cite{Selberg1965} and \\cite[Theorem 1]{Brooks2007} provides us with    \nlower bounds"

Missing context: A stated domain or convention for empty S∩G_i, non-generating intersections, and second eigenvalues for trivial groups. Under the supplied definitions, the lemma does not cover all its allowed inputs.; For a separate review of the surrounding application: definitions and embeddings of Γ_1 and Γ_2, identification of their generating sets, and dated versions of the exact external subgroup-gap results. These are not prerequisites for the nondegenerate abstract proof.

### narrative:103198 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The target is a forward transition, not a mathematical statement: neither “the following” result nor the immediately preceding argument is supplied. The available setup supports elementary reindexing and fraction reduction, but cannot establish readiness to prove an unidentified result. This is a packet/mapping limitation, not an identified proof defect. No external results are imported under the 2012-05-24 cutoff; later knowledge potentially present in model weights is not treated as evidence.

Conditional inputs used: 

- **context**: The result introduced by this sentence is absent. Consequently, its hypotheses, conclusion, and required prerequisites cannot be identified or checked. No headline mathematical claim is established by this sentence alone.

  Source: "We are now in position to prove the following"

- **map_correction**: The supplied section setup ends at line 4105, while the target begins at line 4241. The intervening argument and following statement are missing. The narrative should be linked to those passages before its asserted readiness can be assessed; this observation proposes additional context without changing the frozen map.

  Source: "We are now in position to prove the following"

- **context**: Neither referenced quantity nor its desired bound is supplied. The displayed setup therefore cannot be checked against the section's stated analytic goal.

  Source: "our goal in this section being to bound \\eqref{eq:IQ0K0} and \\eqref{eq:IQ0}."

- **context**: For positive integers u and q, this follows directly by dividing numerator and denominator by gcd(u²,q). The parity reindexings also agree with the displayed congruence conditions: for even u, 2x runs through uZ; for odd u, it runs through 2uZ. Given the stated homogeneity, f(ux,uy)=u²f(x,y). These checks support only the preparatory identities, not any subsequent minor-arc estimate. The full parameter ranges and definition of f are not supplied.

  Source: "so that $u^{2}/q=u_{0}/q_{0}$ in lowest terms, $(u_{0},q_{0})=1$."

- **unverified**: The odd-u reindexing is displayed, but no subsequent estimates are provided for either parity. Whether the omitted argument applies uniformly to the odd case remains an exact outstanding obligation if the following result concerns the complete sum over u.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

Missing context: The theorem, proposition, or other statement immediately following the target transition.; The intervening source at lines 4106–4240, including any estimates intended to justify the transition.; The definitions and target bounds of the quantities referenced as eq:IQ0K0 and eq:IQ0.; The relevant setup from sec:outline, including parameter ranges and the definitions and properties of f, the family of forms, and the weight function.; If the following result covers all u, the argument establishing the required estimates for odd u as well as even u.

### narrative:104579 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The target announces estimates at the scale of eq:cEN2bnd, but supplies neither those estimates nor their derivation. The surrounding section concerns only q<Q_0, so the packet does not establish the full mean-square error bound. This is a missing-context and mapping limitation, not an identified mathematical contradiction. No external theorem is imported; later knowledge potentially present in model weights is not used as evidence under the 2012-05-24 cutoff.

Conditional inputs used: eq:cEN2bnd

- **unverified**: This is an announcement rather than a demonstrated inference. To verify it, the actual estimates must exhibit a positive power saving sufficient for the benchmark sum_{n<N}|E_N^U(n)|^2 << N T^{2(delta-1)} N^{-eta}. No such estimates occur in the supplied target or section setup.

  Source: "Finally, we prove the desired estimates of the strength \\eqref{eq:cEN2bnd}."

- **map_correction**: The reference to eq:cEN2bnd identifies the desired conclusion or comparison scale, not an established premise from which the target follows. The frozen source-reference edge should not be interpreted as proof dependence; using the bound itself to justify this announcement would be circular.

  Source: "the desired estimates of the strength \\eqref{eq:cEN2bnd}"

- **context**: The supplied scope covers one minor-arc regime. Estimates proved here could support the full error bound only after identifying this regime's contribution and combining it with bounds for the remaining regimes. That assembly is not supplied.

  Source: "\\section{Minor Arcs I: Case $q<Q_{0}$}\\label{sec:qQ0}"

- **context**: These restrictions qualify the major-term lower bound in the stated theorem. They do not qualify its separate displayed mean-square bound. Any eventual verification of the target must therefore control the stated error sum, not merely admissible integers satisfying the major-term estimate.

  Source: "For $\\foh N<n<N$ and admissible, $n\\in\\sA$, we have"

Missing context: Definitions and integration domains of eq:IQ0K0 and eq:IQ0, together with the estimates announced immediately after the target.; The Fourier/arc decomposition relating those integrals to the contribution of q<Q_0 to the mean-square error.; Definitions and permitted sizes of Q_0, K_0, U, X, T and N, including parameter inequalities that yield some eta>0 and the required uniformity of constants.; For a claim of the full eq:cEN2bnd rather than only this section's contributions, estimates for the other arc regimes and the argument combining all contributions.

### narrative:105898 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

Conditional on the stated expansion and suitable convergence, the local algebra is correct: Cauchy–Schwarz gives the factor U, squaring gives u^{-4}, conjugation produces the displayed phases, and the modular bracket matches eq:cSdef. Indeed, q0 divides q and (u0,q0)=1 follow directly from eq:tilQis. Summing over arcs gives the required upper bound even if arcs overlap. The final partition is by a'=a, not by equality of forms. However, the packet does not complete the odd-u case or supply the analytic prerequisites for rearranging the infinite sums. These transitions organize a second-moment calculation; they do not yet establish a quantitative minor-arc estimate. No external result or post-cutoff development is used; model training itself is not historically cutoff-limited.

Conditional inputs used: eq:IQdef, eq:RNRf, eq:cRfuIs, eq:cSdef, eq:ffVdef, eq:tilQis

- **context**: The supplied setup restricts the derivation of eq:cRfuIs to even u, whereas eq:cRsq and eq:IQbnd1 display an unrestricted sum over u<U. For odd u, the preceding lattice expression contains f(2xu,yu), rather than f(xu,yu). The displayed argument therefore verifies the even-u contribution conditionally, but the packet does not verify the analogous odd-u expansion and its subsequent treatment. This is an omitted case, not evidence that the asserted analogous treatment is impossible.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

- **unverified**: The expansion and separation into modular and archimedean brackets are valid for finite frequency truncations. Passing to the displayed infinite sums and interchanging them with the beta integral requires a convergence justification. The packet does not define the regularity and support of Upsilon, the finiteness of the family F, or the individual modular sums. A sufficient remaining check is absolute summability of the frequency expansion, uniformly over the beta interval for each of the finitely many outer parameters, together with finiteness of those outer sums.

  Source: "open the square, setting $\\ff'=f'-a'$."

- **context**: The subsequent calculation does use the squared L2 structure and retains correlations between distinct forms. However, the claimed insufficiency of the earlier pointwise estimate cannot be checked quantitatively without the desired bound for I_Q and the parameter relations. It is motivational prose here, not a consequence established by the displayed identities.

  Source: "It is no longer sufficient just to get cancellation in $\\hat \\cR_{f,u}$ alone, as in \\eqref{eq:hatRfuBnd}; we must use the fact that $\\cI_{Q}$ is an $L^{2}$-norm."

- **map_correction**: For this whole narrative target, eq:cRsq and eq:IQbnd1 are locally derived intermediate outputs, not independent premises establishing the passage. Their reference edges can record internal use but should not be counted as independent support. Likewise, identifying the modular bracket uses the definition eq:cSdef, not the subsequent modular estimate appearing in its attached excerpt.

  Source: "Insert \\eqref{eq:cRsq} into \\eqref{eq:IQdef} and\nopen the square, setting $\\ff'=f'-a'$. This gives"

Missing context: The odd-u analogue of eq:cRfuIs, including its normalization and frequency arguments, and confirmation that it supports the subsequent unrestricted-u treatment.; Definitions or hypotheses ensuring the frequency-sum rearrangements: regularity and support of Upsilon, finiteness of F, and the definition eq:cSfDef of the individual modular sums.; The intended quantitative bound for I_Q and parameter relations needed to assess the motivational claim that eq:hatRfuBnd is insufficient.

### narrative:109314 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The proposed diagonal/off-diagonal organization is supported at the bookkeeping level by the supplied expansion and decomposition. The announced power-saving bounds are not established in this packet. Equation eq:cEN2bnd supplies a comparison scale, not a proof of those bounds. No external results are imported; the recorded cutoff is 2012-05-24, and potentially later model knowledge is not used as evidence.

Conditional inputs used: eq:cEN2bnd

- **context**: These conditions are exhaustive and disjoint, so they support the announced separation of the expanded expression into two contributions. This checks the organizational transition, conditional on the preceding expansion and legitimate regrouping of its sums. It does not establish cancellation or a power saving in either contribution.

  Source: "where, once $\\ff$ is fixed,  we collect $\\ff'$ according to whether $a'=a$ (the ``diagonal'' case) and the off-diagonal $a'\\neq a$."

- **unverified**: This announces estimates but supplies neither their statements nor their proofs within the target scope. The remaining local obligation is to bound both contributions at the advertised scale N T^{2(delta-1)} N^{-eta}, for some positive eta and with the required parameter uniformity. Their absence here is a context limitation, not evidence that the estimates are false.

  Source: "We treat $\\cI_{Q}^{(=)}, \\ \\cI_{Q}^{(\\neq)}$ separately, starting with the former; we give bounds of the quality claimed in \\eqref{eq:cEN2bnd}."

- **map_correction**: The source-reference edge from eq:cEN2bnd should be understood as a benchmark/background reference, not a logical proof input establishing the diagonal or off-diagonal estimates. The supplied theorem statement is itself an unverified proposed premise.

  Source: "we give bounds of the quality claimed in \\eqref{eq:cEN2bnd}."

- **context**: The announcement concerns this Q-range, not the entire error term. The packet omits the definition of eq:IQdef, the parameter relations, and the subsequent estimates. Thus it does not establish uniformity over this range or explain how bounds here contribute to the full error second moment.

  Source: "\\section{Minor Arcs II: Case $Q_{0}\\le Q<X$}"

Missing context: The actual statements and proofs of the diagonal and off-diagonal bounds in the range Q_0 <= Q < X, including the quantifiers and uniformity of the positive saving exponent.; Definitions of I_Q and its two contributions, together with the inherited meanings and relations of Q_0, X, M, U, T, N, delta, the form family, and the q_0/u_0 notation needed to check the estimates.; If the announcement is intended to support the full bound eq:cEN2bnd, the relation between these integrals and the error second moment, including summation over Q and treatment of the other ranges.

### narrative:110408 — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The passage is locally supported as parameter algebra and a partition of the stated off-diagonal contribution, conditional on the supplied definitions. The two expressions for H agree, and the gcd conditions are disjoint and exhaustive. No estimate for either contribution is established here. No external theorem is imported; possible later knowledge in model weights is not used as evidence.

Conditional inputs used: eq:fuIs, lem:spec3

- **context**: Substituting U=Q₀^(η₀²/100) gives U^(10/η₀)=Q₀^((η₀²/100)(10/η₀))=Q₀^(η₀/10). The supplied positivity of η₀ permits cancellation. This checks the identity, not the eventual usefulness of this parameter choice.

  Source: "H=U^{10/\\eta_{0}}=Q_{0}{}^{\\eta_{0}/10}"

- **context**: These conditions partition the index pairs without overlap, including the boundary gcd(a,a′)=H in the second contribution. Keeping the existing condition a′≠a in both restricted sums yields the displayed decomposition by definition. The partition itself requires no counting estimate.

  Source: "corresponding to whether $(a,a')>H$ or $(a,a')\\le H$, respectively."

- **context**: The lemma supplies the provenance and positivity of η₀, conditionally on its unverified statement. Its congruence-counting bound is not applied in this passage, so its modulus range and parameter hypotheses do not justify any large-gcd estimate here. The supplied reference edge is appropriate as provenance, not evidence that the counting bound has been used.

  Source: "the constant $\\eta_{0}>0$ comes from Lemma \\ref{lem:spec3}."

- **context**: This announces the next step rather than proving a bound. The supplied scope supports only introducing H and splitting the contribution; it does not establish a saving for the large-gcd part or validate the eventual choice of H against downstream requirements.

  Source: "We deal first with the large $\\gcd$."

Missing context: The exact definition and normalization of the parent contribution I_Q^(≠) are not supplied beyond its description as the a′≠a portion. The partition is supported for that described sum; positivity, convergence, and subsequent estimates are not certified.; The proof of Lemma spec3 and its underlying parameter definitions are absent. Its counting conclusion remains an unverified premise and is unnecessary for the elementary transitions reviewed here.

### narrative:112352 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The target announces a small-gcd case but supplies neither its definition nor its treatment. The provided setup establishes a different decomposition, according to whether a'=a. The transition's coverage and contribution to the minor-arc estimate cannot be checked from this packet. This is a scope/context limitation, not an identified proof defect.

Conditional inputs used: 

- **context**: Neither the operands of the gcd nor the threshold defining 'small' are supplied. The intervening argument and subsequent treatment are absent, so one cannot check that this is the remaining case, that the cases exhaust the relevant sum, or that the promised estimate follows.

  Source: "Finally, we handle small $\\gcd$."

- **context**: This partition is exhaustive at the level of the stated indices, but it does not identify the later gcd partition or say which diagonal/off-diagonal contribution the target concerns. It therefore supplies background rather than support for the announced small-gcd treatment.

  Source: "where, once $\\ff$ is fixed,  we collect $\\ff'$ according to whether $a'=a$ (the ``diagonal'' case) and the off-diagonal $a'\\neq a$."

- **unverified**: The target sentence alone supplies no estimate linking this case to the density-one headline. No external theorem is imported to fill the gap. The applicable cutoff is 2012-05-24; model knowledge is not inherently date-filtered and is not being treated as evidence of historical availability.

  Source: "We prove that a set of density one satisfies the"

Missing context: The exact gcd expression, including its operands and any relevant divisibility restrictions.; The threshold defining the small-gcd range and the parameter hypotheses governing it.; The preceding case decomposition and estimates needed to verify the word 'Finally'.; The argument following the target, including the claimed bound and its connection to the relevant contribution to I_Q.

### narrative:114852 — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The stated combination is locally valid conditional on the five supplied, unverified premises. Substituting the off-diagonal decomposition into the first decomposition gives three contributions. Taking η to be the minimum of their three positive saving exponents yields I_Q ≪ N T^{2(δ−1)} N^{−η}. All five mapped dependencies are relevant. A uniform conclusion throughout Q₀ ≤ Q < X requires the component estimates to be uniform there. This assessment does not establish those estimates or any broader theorem. No external result is imported; latent knowledge of later work is not used as evidence.

Conditional inputs used: eq:cIQ11bnd, eq:cIQ12, eq:cIQ12bnd, eq:cIQ1break, eq:cIQ2bnd

- **context**: Together with the supplied off-diagonal equality, this reduces the conclusion to the three stated bounds. If their exponents are η₁, η₂, η₃ > 0, set η = min(η₁, η₂, η₃). For N ≥ 1, each N^(−ηᵢ) ≤ N^(−η), so summing preserves the claimed power-saving shape. No equality of the three exponents is required.

  Source: "\\cI_{Q}\\ll \\cI_{Q}^{(=)}+\\cI_{Q}^{(\\neq)},"

- **unverified**: Each component proposition supplies a positive saving exponent, but these statements are proposed premises, not established results in this review. The elementary combination does not verify their proofs. For a single estimate valid across the section's Q-range, their exponents, implied constants, and sufficiently-large-N thresholds must be independent of Q after fixing the permitted parameters.

  Source: "There is an $\\eta>0$ such that"

- **context**: The full statement announced by this sentence is outside the source_slice. Relation evidence shows its opening concerns Q₀ ≤ Q < X and a bound for I_Q. The supplied premises support that three-term power-saving conclusion, conditional on their validity and required uniformity; they do not by themselves support claims about summing over Q, other Q-ranges, or the paper's headline density theorem.

  Source: "we have proved the following"

Missing context: The complete statement immediately following the target sentence, to check its exact quantifiers and any additional conclusion.; For a range-uniform conclusion, confirmation that all three component bounds apply throughout Q₀ ≤ Q < X with compatible parameter choices, including the same H in the off-diagonal split, and with Q-independent saving exponents, implied constants, and asymptotic thresholds. Definitions of the underlying sums are not needed for the finite-sum inference, but their substantive bounds remain unverified.

### narrative:115416 — gpt-6.1-sol

Delivery: completed; local status: defective.

Conditional on the supplied formulas, the finite Fourier completion, Cauchy–Schwarz step, and identification of the modular bracket are correct for the displayed even-u model. However, opening the square produces the opposite beta-shift phase from the one printed in eq:IQbnd2. Thus the displayed transition is not justified as written. The odd-u extension and some support/range prerequisites also remain unverified. This is a local assessment, not a whole-theorem verdict. No external results are imported; model knowledge is not intrinsically date-filtered, and no later literature is used.

Conditional inputs used: eq:IQdef, eq:RNRf, eq:RfuNew, eq:cRffuIs, eq:cSdef, eq:cSfDef, eq:tilQis

- **context**: The completion identity checks directly, assuming the displayed sums converge and f is integer-valued with period q0 modulo q0. Expanding S_f and summing over n,m gives q0^(-2) times the two character sums, hence the indicators k≡x and ℓ≡y modulo q0. The surviving phase is e_{q0}(ru0 f(x,y)), as required by homogeneity and u²/q=u0/q0. There is no missing normalization. Also q0 divides q and gcd(ru0,q0)=1, including the harmless case q0=1.

  Source: "so that, using \\eqref{eq:cSfDef}, an elementary calculation gives"

- **context**: For positive integers u<U, |μ(u)|≤1 and there are at most U summands, so the factor U in eq:cRsq2 is justified. The beta integration interval depends on q, not r, permitting separation of the modular and archimedean factors. The modular bracket agrees exactly with eq:cSdef under the checked divisibility and coprimality conditions.

  Source: "Put \\eqref{eq:RfuNew} into \\eqref{eq:RNRf} and apply Cauchy-Schwarz in the $u$-variable:"

- **error**: This phase has the wrong sign for the displayed ordering λ_f times conjugate(λ_f'). In eq:cRsq2 the unprimed term contains e(-aβ), while the conjugated primed term contributes e(+a'β). Their product is e(β(a'-a)), not the printed e(β(a-a')). The modular factor e_q(r(a'-a)) already uses the former sign. Symmetry of the beta interval alone does not justify changing only this phase while leaving the lambda factors unchanged. The remaining obligation is to justify the printed inequality by a separate argument or correct this expansion and verify its subsequent use.

  Source: "e(\\gb (a-a'))"

- **unverified**: The checked completion uses eq:cRffuIs, which is supplied only for even u, whereas the sum in eq:cRsq2 runs over all u<U. For odd u the supplied starting expression has f(2ux,uy) and weight Υ(2ux/X), not the displayed even-u expression. The packet does not provide the corresponding completion or show that later modular estimates apply uniformly. This is an unverified extension, not a demonstrated contradiction.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

- **context**: Definitions of Υ and the parameter scales are absent. Even if Υ gives length about X/u, Q≥X does not alone imply this length is below q0=q/gcd(u²,q). Thus the narrative motivation is not established uniformly by the supplied inequalities. The finite Fourier identity itself does not require that length comparison. Support or convergence assumptions, finiteness of the form family, and coefficient integrality are also needed for the displayed expansions and rearrangements.

  Source: "the range of $x,y$ in \\eqref{eq:cRffuIs} is now such that we have incomplete sums"

- **map_correction**: The local definition eq:glfDef is an essential input omitted from the dependency list. Conversely, eq:RfuNew is derived inside this target scope: its reference edge is valid, but it should be understood as an internal intermediate, not an independently established premise. The final diagonal/off-diagonal split is bookkeeping, not a quantitative minor-arc estimate; its off-diagonal contribution is not automatically nonnegative.

  Source: "\\be\\label{eq:glfDef}"

Missing context: Definition and support or convergence properties of Υ, and finiteness or summability of the form family.; The omitted form-family definition eq:ffVdef, including the integrality hypotheses needed for reduction modulo q0.; Definitions and relationships of X, M, U and the intended meaning of the incomplete-sum comparison.; The odd-u completion and confirmation that the required modular estimates cover its modified quadratic form.; Definitions of I_Q^(=) and I_Q^(≠), particularly whether they denote signed contributions or absolute majorants.

### narrative:118709 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The sentence is an organizational announcement, not an off-diagonal estimate. The preceding decomposition supplies its referent, but the continuation needed to check the announced analysis is absent. No mathematical defect in the target sentence is identified, and it supports no minor-arc bound or local-global conclusion by itself.

Conditional inputs used: 

- **context**: This identifies the announced off-diagonal contribution with pairs satisfying a≠a′. Thus the transition has a clear local referent within the stated section range X≤Q<M. Choosing to discuss that contribution first requires no additional mathematical hypothesis.

  Source: "As before, decompose \n$\\cI_{Q}$ according to the diagonal ($a=a'$) and off-diagonal terms:"

- **unverified**: No subsequent off-diagonal argument is supplied. The packet therefore cannot establish that this contribution is actually treated first or that any estimate for it follows. This is a limitation of the bounded excerpt, not evidence of a proof defect.

  Source: "We handle the off-diagonal term first."

Missing context: The continuation immediately following the target, sufficient to identify the announced off-diagonal argument and its conclusion.; If an estimate is intended to be assessed, the precise definition of the off-diagonal contribution, its proposed bound, and the definitions and parameter assumptions used in that argument.

### narrative:119956 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

Conditional on the supplied lemmas and the intended convention \ff=f-a, the diagonal partition and applicability of eq:modBndaEqAp are locally supported. The packet does not establish the comparative claims that a=a' alone is insufficient or that the stronger estimate produces a useful additional saving after summation. No quantitative estimate for the new off-equality contribution is proved within this slice. No external result is imported; possible later knowledge in model weights is not treated as historical evidence.

Conditional inputs used: eq:cIQ3def, eq:modBndaEqAp

- **context**: The surrounding section treats X≤Q<M, so the stated range hypothesis of eq:cIQ3def is satisfied. Conditional on that lemma, its diagonal summation can be partitioned by equality or inequality of the two evaluated forms. This elementary partition requires no external theorem.

  Source: "Assume $Q\\ge X$."

- **context**: With the corresponding intended convention \ff=f-a, the diagonal condition a=a' gives \ff(m,-n)-\ff'(m',-n')=f(m,-n)-f'(m',-n'). Thus the unequal-value branch satisfies both explicit hypotheses of eq:modBndaEqAp. The unprimed convention is not explicitly defined in the packet, although the displayed primed convention strongly indicates it.

  Source: "As before, open the square, setting $\\ff'=f'-a'$"

- **context**: The two restrictions are disjoint and exhaustive. The displayed identity is therefore valid if these quantities denote the restricted contributions to the same diagonal expression. Their precise definitions, and whether they partition the original integral expression or the nonnegative majorant supplied by eq:cIQ3def, are not included. This is a definition/scope limitation, not a demonstrated algebraic error.

  Source: "\\cI_{Q}^{(=,=)}\n+\n\\cI_{Q}^{(=,\\neq)}"

- **unverified**: The supplied estimate can be applied on the unequal-value branch, but its usefulness depends on the factors (q/q0)^5, gcd(a²,q0), and |f(m,-n)-f'(m',-n')|^{1/2}. No baseline estimate, required saving, or uniform controls for these factors are supplied. Consequently, neither comparative assertion can be checked here. The exact remaining obligation is to show that this bound, after summation in eq:cIQ3def, improves the previous diagonal treatment sufficiently for the intended target.

  Source: "We no longer save enough from $a=a'$ alone. But recall that here more cancellation can be gotten from \\eqref{eq:modBndaEqAp}"

- **map_correction**: This sentence announces an estimate; it does not provide one. The third supplied relation includes subsequent text asserting a power saving under Q<XT, which lies outside the bounded source slice. The dependency edge is relevant to the announced method, but its extended evidence cannot establish that later quantitative conclusion within this review.

  Source: "We now estimate $\\cI_{Q}^{(=,\\neq)}$ using the extra cancellation in \\eqref{eq:modBndaEqAp}."

Missing context: Explicit definitions of \ff=f-a, q0, and the precise diagonal contributions being partitioned.; The preceding diagonal estimate and the numerical saving required, to assess the claim that a=a' alone is insufficient.; Parameter and family bounds controlling the arithmetic factors and evaluated-form difference, if the claimed additional cancellation is to be verified quantitatively.

### narrative:122162 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The cited counting proposition matches the stated equality condition and the section's diagonal restriction a=a'. Conditional on that proposition, it can bound the number of contributing index tuples. The packet does not establish that this counting bound yields savings for the weighted quantity I_Q^(=,=): the relevant weight estimates, parameter relationships, and comparison bound are missing. This is a limitation of the supplied local context, not a demonstrated proof defect.

Conditional inputs used: eq:eqeq

- **unverified**: The reference is relevant: eq:eqeq counts tuples satisfying precisely a'=a and ff(m,-n)=ff'(m',-n'). Its statement is supplied, but its proof is not assessed here. Conditional on its validity, for each fixed ff and a sufficiently large cutoff L it gives at most O_epsilon((TL)^epsilon(L^2+TL)) tuples. This supports an unweighted counting reduction, not yet the asserted analytic savings.

  Source: "We exploit this condition to get savings using \\eqref{eq:eqeq}."

- **context**: The fixed-form hypothesis can be matched by applying the proposition separately inside the outer ff-sum. The diagonal condition and equality condition also match. However, the applicable counting cutoff and its required largeness are not established. The displayed analytic sum uses indices below q_0, whereas M also appears as a section-level parameter. Applying the proposition with its cutoff equal to q_0 requires q_0 to be sufficiently large, or a separate treatment of smaller q_0. Definitions of T, q_0, and the family are absent.

  Source: "For large $M$ and  $\\ff=f-a\\in\\fF$ fixed,"

- **context**: The expression in eq:IQbnd2 is weighted by a modular correlation and an archimedean integral. A tuple-counting bound controls it only after suitable absolute-value or other weight estimates. Neither those estimates nor the precise definition and normalization of I_Q^(=,=) are supplied. Thus no quantitative saving for that quantity, or downstream headline estimate, follows from this packet alone.

  Source: "Yet again the sum has split into modular and archimedean components with the former being exactly equal to $\\cS$ in \\eqref{eq:cSdef}."

Missing context: Definitions of the family F, its multiplicities or cardinality, the forms f and ff=f-a, and the parameter T.; Definitions and relationships of q_0, Q, M, X, and u, including the effective ranges of n,m,n',m' and treatment of small counting cutoffs.; The definition of I_Q^(=,=) and its precise relation to the weighted expansion eq:IQbnd2.; Bounds for the modular and archimedean factors on the equality locus, followed by the sums over ff, q, and u.; The benchmark estimate and parameter inequalities against which the claimed savings are measured.

### narrative:123431 — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The cited decomposition and three component bounds conditionally yield the intended bound for the total contribution, with saving exponent equal to the minimum of the three positive exponents. The supplied archimedean calculation encodes M=XT, which makes the hypotheses Q<XT applicable throughout X≤Q<M. This assesses only the aggregation: the component estimates are unverified premises, and the complete following theorem is not included. No external result is imported; model background knowledge is not evidence of availability before the recorded cutoff.

Conditional inputs used: eq:cI3bnd, eq:cI41bnd, eq:cI42bnd, eq:cIQ312, eq:cIQ34

- **context**: Together with eq:cIQ312, this reduces the total to the three contributions bounded by eq:cI3bnd, eq:cI41bnd, and eq:cI42bnd. Writing their exponents as eta_3, eta_41, eta_42 and taking eta=min(eta_3,eta_41,eta_42)>0 gives I_Q ≪ N T^{2(delta−1)} N^{−eta}. There are only three terms, so this aggregation introduces no logarithmic loss. The component estimates are used conditionally, not established here.

  Source: "\\cI_{Q}\\ll \\cI_{Q}^{(=)}+\\cI_{Q}^{(\\neq)}."

- **context**: The off-diagonal estimate assumes X≤Q<M, while both diagonal estimates assume Q<XT. For positive scales, the displayed equality simplifies to TX²/(QM)=X/Q and hence M=XT. Under that supplied scale convention, Q<M gives the required strict inequality Q<XT, and Q=X is permitted. The defining equation eq:Mis is omitted, but its needed consequence is encoded in this calculation.

  Source: "|\\gb u^{2} f(x,y)|\\ll \\frac1{QM} u^{2} T\\left(\\frac Xu\\right)^{2}= \\frac XQ\\le 1."

- **map_correction**: The target slice ends before the announced conclusion. All five dependency edges are relevant to the aggregation; none is shown to be incorrect. However, the map should distinguish this transition from the following theorem and record the parameter relation used for range compatibility. The missing consequent is a scope/mapping limitation, not a demonstrated proof defect. The transition supports the total minor-arc estimate, not by itself the paper's density-one headline claim.

  Source: "we have the following"

Missing context: The complete following theorem, including its quantifiers and any uniformity assertion in Q, is needed to compare its exact wording with the aggregate estimate.; The explicit parameter definition eq:Mis would confirm the scale convention M=XT already encoded in the supplied calculation.; The proofs and standing hypotheses of the three component propositions are not supplied for verification; this assessment treats their statements as conditional premises.

### narrative:123918 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The generator changes and congruence compatibility check directly. The passage sets up, but does not prove, combinatorial expansion. Its decisive transition from expansion to a geometric spectral gap remains conditional on an uninspected external theorem and omitted geometric hypotheses. This is a bounded assessment of the narrative, not a verdict on the appendix's subsequent proof or the main theorem. No external theorem is admitted from model memory, which may contain later knowledge.

Conditional inputs used: eq_generators1, sec:specGap, thm:specGap, external:BourgainGamburdSarnak2011, external:BourgainVarju2011, external:SalehiVarju2011

- **context**: Direct multiplication verifies all three displayed conjugations. The second operation is conjugation by D=diag(-i,1), an invertible Gaussian-integer matrix. Thus the composite is an automorphism preserving reduction kernels modulo every integer q. It is also conjugation by a complex projective linear transformation, hence preserves the associated hyperbolic geometry. The passage therefore supplies more than an abstract group isomorphism, as needed for transferring congruence and spectral statements. The identification of the original generators with the Apollonian preimage remains a proposed premise.

  Source: "These are the image of (\\ref{eq_generators1}) under the product of two\nisomorphism: first conjugation by $A$\nand then multiplication of the off-diagonal elements\nby $-i$ and $i$."

- **unverified**: This is the essential external bridge. The cited statements are absent. Verify that their pre-cutoff version applies to infinite-volume Kleinian quotients of H^3, including torsion, rather than only compact covers or a two-dimensional setting. Supply and check the exact hypotheses, particularly those ensuring an isolated simple L2 ground state and a uniform comparison for this covering family. The compact Brooks–Burger comparison alone does not establish this extension.

  Source: "the\nequivalence can be extended to cover our example,\nsee \\cite[Theorems 1.2 and 2.1]{BourgainGamburdSarnak2011}."

- **context**: The supplied section lists only discrete eigenvalues below 1; it does not ensure two such eigenvalues exist for each q. Specify whether lambda_1 instead means the spectral infimum on the orthogonal complement of the ground state, allowing the continuous-spectrum threshold when necessary. Likewise, the trivial quotient at q=1 has no second Markov eigenvalue. These are definitional gaps, not counterexamples to the intended uniform-gap assertion.

  Source: "We denote by $\\gl_0(q)\\le\\gl_1(q)$ the two\nsmallest eigenvalues of $\\Delta$"

- **unverified**: Conditional on the stated theorem scopes, square-free expansion does not by itself cover all integer moduli. The first exclusion needs the relevant rational algebraic ambient group and density hypotheses: embedding Gaussian matrices into larger integral matrices does not automatically give Zariski density in the full larger special linear group. The historical survey's exact theorem scopes, finite-generation assumptions, and perfectness formulation remain unchecked because only bibliographic entries are supplied.

  Source: "the first one is not applicable to the Apollonian group, the second\none is restricted for the moduli."

- **unverified**: Within this slice this is an announcement, not an established estimate. Conditional on a later uniform combinatorial bound and a valid comparison theorem, it supports thm:specGap. It does not independently support thm:Main. The absence of the later expansion proof from this narrative packet is a scope limitation, not a demonstrated proof defect.

  Source: "We show that the congruence subgroups $\\bar\\Ga(q)$\nof the Apollonian group have combinatorial spectral\ngap"

- **map_correction**: The map resolves this reference to thm:Main even though source_from is sec:prelim. That is an incorrect attribution: the needed input is the preliminary group/spin-map identification, not the density-one curvature theorem. Also, thm:specGap is the announced conclusion and scope reference here, not an established proof premise.

  Source: "Recall from Section \\ref{sec:prelim} that the preimage of the Apollonian\ngroup under the homomorphism"

Missing context: The preliminary definitions of the Apollonian group, the spin homomorphism, and the identification of its preimage with the displayed generated group.; The exact pre-cutoff statements and hypotheses of BGS11 Theorems 1.2 and 2.1, with their applicability to this H^3 orbifold tower checked.; The geometric assumptions behind 'as above', including the ground-state and spectral-threshold facts used in the comparison.; Conventions for a missing second discrete eigenvalue, the trivial quotient, and whether quotient generators retain multiplicities.; The subsequent proof of the uniform combinatorial gap, if assessment beyond this introductory narrative is requested.

### narrative:13050 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The definitions and transition to the stated conjecture are internally coherent. Actual curvatures necessarily pass every congruence test; the converse for sufficiently large integers is explicitly conjectured, not proved here. Historical attributions and the geometric illustration remain unverified from the supplied evidence. No external theorem is imported and no later development is used.

Conditional inputs used: 

- **context**: Interpreting membership modulo q as existence of a congruent element of B, the definition means: for every positive integer q, there exists b_q in B with n congruent to b_q modulo q. Directly, B is contained in A, by choosing b_q=n. The witnesses may depend on q, so this definition does not establish the converse. The local-to-global transition is correctly presented as a conjecture.

  Source: "\\sA:=\\{n\\in\\Z:n\\in\\sB(\\mod q),\\text{ for all $q\\ge1$}\\}."

- **context**: The hypotheses of a fixed, primitive, integral gasket are explicit. The threshold for 'sufficiently large' may depend on that gasket; no uniform threshold is asserted. Allowing signed integers in A is consistent with a conjecture restricted to sufficiently large positive integers. Since B is a set, the conclusion concerns represented integers, not circle multiplicities.

  Source: "Then every sufficiently large admissible number is the curvature of a circle in $\\sG$."

- **unverified**: Only bibliographic records are supplied, so the precise attribution, formulation and hypotheses of the cited conjecture cannot be checked. The historical claims about Soddy and the initiation of Diophantine study likewise remain unverified. Listed publication years precede the recorded cutoff of 2012-05-24, but exact supporting passages and versions have not been inspected. These are remaining attribution obligations, not demonstrated mathematical errors.

  Source: "\\cite[p. 37]{GrahamLagarias2003}, \\cite{FuchsSanden2011}."

- **map_correction**: The cited literature supplies historical and thematic background here, not stated proof premises. Likewise, the figure reference is illustrative. The frozen source-reference edges can remain citation links, but should not be interpreted as establishing dependencies sufficient to prove the conjecture or the abstract's density-one claim.

  Source: "studying $\\sB$ with multiplicity (that is, studying circles), or without multiplicity (studying the integers which arise)."

- **context**: The image itself is absent. Its curvature labels and geometric construction cannot be checked from the caption alone. This does not obstruct the elementary set-theoretic checks above. The model may contain knowledge acquired after the historical cutoff; none is used as evidence in this assessment.

  Source: "\\includegraphics[width=    \n2in]{pic.pdf}"

Missing context: Exact passages supporting the conjecture attribution in Graham–Lagarias–Mallows–Wilks–Yan, p. 37, and Fuchs–Sanden, including the hypotheses of the versions cited.; Exact passages supporting Soddy's priority attribution and the historical description of the cited Diophantine literature.; For any external result subsequently used as a proof input: its exact statement and hypotheses, version, available_from, date_evidence and date_basis. Bibliographic years alone do not verify the needed content.; The image pic.pdf and the definition/construction of an Apollonian gasket and root quadruple, if verification of the illustration is required.

### narrative:144695 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The target slice contains only typesetting commands, not a mathematical assertion, proof, or narrative transition. There is therefore no local mathematical inference to assess. The target classification needs correction; this is a mapping limitation, not a proof defect. No external results are imported or validated.

Conditional inputs used: 

- **map_correction**: These commands select a bibliography style and define a formatting macro. Together with the page break, they exhaust the target slice. The label 'Narrative at line 5931' does not identify an assessable mathematical obligation.

  Source: "\\bibliographystyle{alpha}\n\n\\newcommand{\\etalchar}[1]{$^{#1}$}"

- **context**: This mathematical transition appears in the attached section setup, not in the target slice. It cannot be substituted for the selected target or treated as its proof. Its supporting arguments and cited results have not been assessed here.

  Source: "We show that the congruence subgroups $\\bar\\Ga(q)$\nof the Apollonian group have combinatorial spectral\ngap which implies Theorem \\ref{thm:specGap}"

Missing context: If a mathematical review was intended, provide a corrected target span containing the intended assertion or narrative transition and its proposed proof scope.

### narrative:47002 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The paragraph gives a coherent conditional spectral-theory setup, but the packet does not establish the Apollonian group's stated properties or supply the results needed for the strict Hausdorff-dimension bounds. The spin-cover statement also needs an identity-component qualification. The subsequent spectral theorem is outside this target and is not assessed. No external theorem is imported as verified; model recall cannot establish historical availability or theorem content.

Conditional inputs used: 

- **context**: The definition and signature of F are absent. For a real form of signature (3,1), SL(2,C) double-covers the identity component SO_F(R)^0, not all real points of SO_F. The passage therefore requires a component convention and an explanation of which subgroup is lifted. This may be omitted notation rather than a substantive defect.

  Source: "passing from $G=\\SO_{F}(\\R)$ to its spin double cover $G=\\SL(2,\\C)$"

- **unverified**: The image and caption do not establish discreteness, geometric finiteness, or a Schottky presentation. The packet does not define the relevant Apollonian subgroup, explain its passage to SL(2,C), or specify whether 'Schottky' permits parabolic elements. Those details are needed to check the application, rather than merely the abstract setup.

  Source: "(The Apollonian group is such, being a Schottky group, see Fig. \\ref{fig:lim}.)"

- **unverified**: The ambient boundary S^2 directly gives 0 <= delta <= 2. The strict inequalities require further input: positivity of limit-set dimension for a non-elementary discrete group, and the full-dimension/lattice implication under geometric finiteness. Geometric finiteness is supplied and must remain part of the latter inference; infinite volume alone does not justify it. No precise supporting theorem is included.

  Source: "We assume that $\\G$ is non-elementary (not virtually abelian), so $\\gd>0$, and moreover that $\\G$ is not a lattice,\nthat is, the quotient $\\G\\bk\\bH^{3}$ has infinite hyperbolic volume; \nthen $\\gd<2$."

- **context**: This is a setup statement, not a spectral conclusion. Subsequent spectral claims require the standard self-adjoint realization and sign/metric normalization. Torsion-freeness is not assumed: the quotient may be an orbifold, which is compatible with this setup but should not silently be treated as a manifold.

  Source: "The hyperbolic Laplacian $\\gD$ acts on the space $L^{2}(\\G\\bk \\bH^{3})$ of functions automorphic under $\\G$ and square integrable on the quotient; we choose the Laplacian to be positive definite."

- **map_correction**: These citations explicitly introduce the following result. The relation evidence extends into a spectral statement not contained in the target source_slice, so it cannot enlarge this obligation. Likewise, fig:lim is illustrative, not a proof dependency establishing geometric finiteness. The map should distinguish these roles; missing theorem excerpts are a mapping/context limitation, not themselves proof defects.

  Source: "The spectrum is controlled via the following, see \\cite{Patterson1976, Sullivan1984, LaxPhillips1982}."

Missing context: Definition and signature of F; the intended connected component of SO_F(R); and the subgroup/lift convention for Gamma.; A precise definition or presentation of the Apollonian subgroup used here, with support for discreteness, geometric finiteness, non-elementarity, and infinite covolume.; The convention for 'Schottky group', especially whether parabolic elements are allowed.; Exact pre-cutoff theorem statements and locations supporting delta > 0 and, under geometric finiteness, delta = 2 only for lattices; any use of the critical exponent also needs its identification with the stated Hausdorff dimension.; The ensuing spectral theorem and its precise hypotheses, if its conclusions are intended to be reviewed separately.; The cutoff is recorded as 2012-05-24. The supplied bibliography dates precede it, but theorem content and the versions containing the needed results have not been inspected.

### narrative:55546 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The return to the Descartes-form notation is locally consistent, and the supplied generators support the determinant-one definition of the orientation-preserving subgroup. The substantive transition—from a spectral gap to reduction of congruence-coset sums—is only announced. Neither the required spectral-gap statement nor the resulting counting estimate is supplied. This is a limitation of the bounded packet, not a demonstrated defect in the omitted argument. No external theorem has been imported to close the obligation.

Conditional inputs used: eq:Fdef, narrative:47002

- **context**: The algebraic setup checks directly: the matrix of F is 2I−J, with eigenvalues 2,2,2,−2. Each supplied generator is integral, preserves F, and has determinant −1. Consequently, the determinant-one subgroup consists of elements represented by even-length words. These checks support the notation, but establish no spectral or counting assertion.

  Source: "$\\G=\\cA\\cap G$, the orientation preserving Apollonian subgroup"

- **unverified**: No spectral-gap theorem or coset-sum formula appears in the packet. A checkable reduction needs the summand or counting family, the coset convention, the main-term normalization, the error term, and its dependence on the modulus. If uniformity over congruence levels is intended, a gap for one quotient alone does not supply it. The exact remaining obligation is to state the applicable gap and derive the asserted coset comparison with all required uniformity.

  Source: "First we use the spectral gap to see that summing over a coset of a congruence group can be reduced to summing over the original group."

- **map_correction**: The supplied edge to narrative:47002 reaches only the opening setup of the referenced section, not its spectral-gap tools. It is a relevant background edge but does not represent the full proposed proof input. Likewise, eq:Fdef supports the quadratic-form notation, not the congruence-coset reduction. The omitted theorem anchors should be mapped separately when available.

  Source: "Equipped with the tools of                   \n        \n\\S\\ref{sec:preII}, we isolate here some consequences"

- **context**: The transfer back from the spectral section requires a precise group identification: SL(2,C) double-covers the identity component SO_F^+(R), not all of the displayed determinant-one real orthogonal group. Moreover, the full reflection group A cannot literally be a subgroup of SL(2,C). The intended application should specify the orientation-preserving subgroup, its lift, and compatibility of the relevant quotients and congruence subgroups. This is an omitted identification, not by itself a refutation of the announced reduction.

  Source: "passing from $G=\\SO_{F}(\\R)$ to its spin double cover $G=\\SL(2,\\C)$."

- **context**: Most of that section is absent. Its hypotheses about geometric finiteness, non-elementarity and infinite volume are proposed premises, not established facts in this packet. Their applicability to the target subgroup, together with any additional critical-exponent or congruence hypotheses of the omitted tools, remains to be checked.

  Source: "we import all the notation from the previous section."

Missing context: The exact spectral-gap theorem, including its group, spectral parameter, modulus range, exceptional levels or primes, and uniformity constants.; The next counting or coset-comparison statement and its proof, including the summation weight or region, index normalization, error term and parameter ranges.; The definition of Gamma(q), ordinarily the kernel of reduction modulo q in the stated integral matrix representation, and its compatibility with any spin-group formulation.; The precise lift from the orientation-preserving Apollonian subgroup to SL(2,C), and verification or explicit acceptance of all hypotheses needed to apply the omitted spectral tools.; For any external theorem actually used: its exact statement and hypotheses, available_from, date_evidence, date_basis and version, establishing availability by 2012-05-24. The citation keys alone do not provide that record. Model knowledge is not intrinsically date-filtered; no undated recollection has been used as proof evidence here.

### narrative:68030 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The announced use in the major-arcs analysis is supported by the explicit application of Lemma spec1 at eq:fMdecomp. Whether spec1 is a slight generalization of spec0 cannot be checked because its statement and proof are absent. The supplied dependencies remain conditional premises. No external theorem is imported, and model training knowledge is not treated as dated evidence under the 2012-05-24 cutoff.

Conditional inputs used: lem:spec0, eq:fMdecomp

- **context**: The comparison requires the missing statement of spec1. Spec0 concerns unweighted norm-ball counts for fixed gamma_1 in Gamma, q >= 1, and a subgroup satisfying Gamma(q) < tildeGamma(q) < Gamma, as Y tends to infinity. It asserts an exponent below delta, uniformity in q and gamma_1, and both multiplication orders. To verify the announced generalization, one must identify which hypotheses and uniformities spec1 preserves and how its weighted family specializes to, or extends, this counting statement.

  Source: "Next we need a slight generalization of Lemma \\ref{lem:spec0}"

- **unverified**: This explicitly supports the promised downstream use, but does not independently establish the application. The omitted lemma must control the phase-weighted sum over F intersected with a stabilizer coset, uniformly over the variables being summed and integrated. Its parameter restrictions must hold throughout the beta integration and q < Q_0 range. The missing exponent definition and subgroup-index bound are also needed to check the stated aggregate error O(T^{Theta_1} K_0^2 Q_0^4/N). Spec0 alone does not supply these weighted estimates.

  Source: "Applying Lemma \\ref{lem:spec1} to the latter sum, using the definition of $\\gT_{1}$ in \\eqref{eq:gT1def}, and recalling the estimate \\eqref{eq:G0qBnd}  gives"

- **map_correction**: The eq:fMdecomp reference is a forward application anchor, not a mathematical premise proving the announced generalization. Its edge should be understood as downstream-use evidence. The spec0 reference identifies the precursor statement, not a sufficient proof of spec1. These are role corrections to the proposed dependency interpretation, not changes to the frozen map.

  Source: "which will be used in the major arcs analysis, see \\eqref{eq:fMdecomp}."

Missing context: The complete statement and relevant proof scope of Lemma spec1, including all restrictions on K, T_2, beta, x, y, q, and coset representatives.; Definitions of the family F, its multiplicities if any, the phase f_gamma, the norm, and the scales N, T, T_2, X, K_0, and Q_0.; The definition eq:gT1def, the index estimate eq:G0qBnd, and the Fourier cutoff properties needed to check uniform applicability and error aggregation.; The group action and stabilizer definitions needed to verify that the congruence subgroups used downstream satisfy the subgroup hypotheses.; If the missing argument imports external counting or spectral-gap results, their exact statements, hypotheses, versions, available_from dates, date_evidence, and date_basis must establish availability by 2012-05-24; no such results are certified here.

### narrative:71322 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The passage announces a counting estimate at scale N/K and its subsequent use in the major arcs. Neither the estimate nor that application is supplied, so neither transition can be verified. The cited theorem is an intended downstream consumer, not an established premise for the narrative. This is a bounded evidence limitation, not a demonstrated proof defect. No external result is imported; potentially later model knowledge is not used as evidence.

Conditional inputs used: 

- **unverified**: The following lemma and its proof are absent. Consequently, the packet does not specify the counting measure, interval or smoothing window, expected count, error term, or uniformity needed to substantiate 'equidistribution' at the asserted scale. The exact remaining obligation is to compare the complete counting estimate with this description under all its stated hypotheses.

  Source: "The following is our last counting lemma, showing a certain equidistribution among the values of $\\ff_{\\g}(2x,y)$ at the scale $N/K$."

- **unverified**: Only the cited theorem's statement is supplied. Its lower bound for the main term does not establish where or how the announced counting estimate is used. Checking this transition requires the relevant major-arc calculation and verification that its choices of parameters satisfy the counting lemma's hypotheses.

  Source: "This bound is used in the major arcs, see\nthe proof of Theorem  \\ref{thm:cMNis}."

- **map_correction**: The supplied edge from thm:cMNis to this narrative records a source reference, but should not be read as a proof-input dependency. The prose describes the counting bound as an input to the theorem's proof, not the theorem as an input to the counting bound. Retain the citation relationship separately from mathematical dependency.

  Source: "This bound is used in the major arcs"

- **context**: The setup identifies the orientation-preserving Apollonian subgroup, but the imported notation is not supplied. Definitions of the polynomial f_gamma, the actual family of gamma being counted, and the relationships among N, K, X, T and T_2 are needed. The fixed primitive integral gasket is specified in the introductory context, but that alone does not determine these objects.

  Source: "Moreover,                                                                                                          \nwe import all the notation from the previous section."

Missing context: The complete immediately following counting lemma, including its formula, proof, implied-constant dependencies and uniformity ranges.; Definitions of f_gamma, the counting family and its weights or multiplicities, and all scale parameters. The relation evidence mentions N/2<n<N, 1<K<=T_2^(1/10), and x,y asymptotic to X; their applicability cannot be checked without the full statement and parameter setup.; The portion of the proof of Theorem thm:cMNis that applies the counting estimate, including the major-arc expression and the resulting lower-bound calculation.; Theorem thm:RNU, referenced by the supplied theorem statement, if the properties required of the singular-series function are needed to audit that application.

### narrative:73512 — gpt-6.1-sol

Delivery: invalid_assessment; local status: no assessment.

### narrative:86590 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The passage announces a saving for the equal-parameter, equal-value subcase and attributes it to supplementary lemmas rather than to \cS itself. The packet supplies neither the relevant definitions nor those lemmas, so the asserted transition cannot be verified. This is a scope limitation, not an identified proof defect. No external result is imported; latent model knowledge is not treated as evidence of historical availability.

Conditional inputs used: 

- **context**: The parameters a,a', forms f,f', variables m,n,m',n', and their ranges are not defined in the supplied excerpts. Consequently, the hypotheses identifying this subcase cannot be checked, nor can one determine what quantity must exhibit a saving or how large that saving must be.

  Source: "Finally we need some  savings in the case $a=a'$ and $f(m,-n)=f'(m',-n')$."

- **unverified**: Neither \cS and its preceding estimates nor the supplementary lemmas are supplied. The remaining obligation is to show that the subsequent lemmas apply under both displayed equalities and yield the quantitative saving required by the surrounding argument. The passage supports only an announcement of that strategy, not its execution or the density-one headline claim.

  Source: "This will no longer come from $\\cS$ itself, but from the following supplementary lemmata."

Missing context: Definitions and permitted ranges of a,a',f,f',m,n,m',n', including any structural restrictions on the forms.; Definition of \cS, the expression being estimated, its normalization and scale parameters, and the preceding case analysis explaining why this subcase remains.; Statements and applicable proofs of the supplementary lemmas, together with the calculation converting their conclusions into the required saving.

### narrative:92045 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The sentence announces two transitions: combining preceding lemmata into an estimate, and using that estimate in the proof of eq:cI41bnd. Neither transition can be checked because the lemmata, collected estimate, and application are absent. The supplied proposition identifies the intended downstream claim but is not a verified premise. This is a source-coverage limitation, not an identified mathematical defect. No external results are imported; later model knowledge is not evidence for this assessment under the 2012-05-24 cutoff.

Conditional inputs used: 

- **unverified**: The packet supplies neither the referenced lemmata nor the statement and proof of the collected estimate. Consequently, their hypotheses, compatibility, and sufficiency for the announced aggregation cannot be checked.

  Source: "Finally we collect the above lemmata into  our desired estimate"

- **unverified**: This identifies an intended downstream application, not a demonstrated inference. The exact remaining obligation is to exhibit the collected estimate and the step in the proposition's proof where it supplies the required bound.

  Source: "essential in the proof of \\eqref{eq:cI41bnd}"

- **context**: The downstream proposition explicitly assumes Q<XT and asserts a power saving as N tends to infinity. Definitions of the integral and parameters, their admissible ranges and relationships, and the permitted dependence of eta and the implied constant are absent. Thus applicability under Q<XT and the claimed positive power saving cannot be checked. The introductory fixed primitive integral gasket does not supply these missing analytic hypotheses.

  Source: "Assuming $Q<XT$, there is some $\\eta>0$ such that"

- **map_correction**: The dependency-list entry eq:cI41bnd should not be treated as a proof input to this narrative. The sentence presents that proposition as a downstream beneficiary of the missing estimate. The reference edge records an asserted application; it does not establish the aggregation or the proposition. If the graph convention is 'claim depends on input,' an edge from the proposition toward the estimate may be appropriate, but this prose alone is not the estimate or its proof.

  Source: "essential in the proof of \\eqref{eq:cI41bnd}"

Missing context: Statements of the 'above lemmata,' including every hypothesis needed to combine them.; The precise 'desired estimate' and its proof, with definitions of its objects and parameter ranges.; The relevant portion of the proof of eq:cI41bnd showing how that estimate yields the stated bound under Q<XT, including the parameter relationships ensuring a fixed eta>0.

### narrative:93454 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The Möbius rewriting, unfolding, Fourier factorization, and Q0^4 error count are locally correct conditional on the supplied counting premises. The packet does not fully verify the scale and subgroup hypotheses needed to apply Lemma spec1, or the stated parameter normalization. This passage supports the displayed modular–archimedean decomposition, not yet the announced major-arc lower bound. No external theorem is imported; later model knowledge is not treated as evidence, and external availability by the 2012-05-24 cutoff is not certified here.

Conditional inputs used: eq:G0q, eq:G0qBnd, eq:Q0K0intro, eq:Uis, eq:cMNUdef, eq:cMNdef, eq:cRNhatIs, eq:cRNhatUis, eq:fMis, eq:ffToInProd, eq:gT1def, eq:hatFuncN, eq:spec1, eq:spec2, lem:spec1, lem:spec3

- **context**: This transition is valid for integer n and integer-valued forms: periodicity removes the integer translates, and compact support of the hat function justifies unfolding. The unrestricted divisor sum equals the indicator of gcd(2x,y)=1; retaining u<U gives the truncated version exactly. The smoothing support keeps the relevant x,y sums finite and within the size range required by spec1.

  Source: "making a change of variables $\\gt=r/q+\\gb$, and unfolding the integral from $\\sum_{m}\\int_{0}^{1}$ to $\\int_{\\R}$"

- **context**: Conditional on applying spec1 with K=K0, this error is correct: each coset contributes O(T^{Theta1}K0), integration contributes O(K0/N), and summing over reduced residues and cosets costs at most sum_{q<Q0} q·q^2=O(Q0^4). The main term factors because the rational phase is constant on each stabilizer coset. Fourier inversion gives the stated W; the potential sign reversal is harmless because the hat transform is even. No cancellation is needed.

  Source: "O\\left({T^{\\gT_{1}}\\over N}K_{0}^{2}Q_{0}^{4}\\right)"

- **unverified**: The lemma requires 1<K<=T2^{1/10}. Here K=K0=T^{(delta-Theta1)/10}, so the exact outstanding scale check is T^{delta-Theta1}<=T2. The supplied packet omits the defining T,T1,T2 relations and numerical bounds needed to establish this. The beta support satisfies the lemma's strict inequality except at endpoints, where the hat vanishes; that causes no problem.

  Source: "Applying Lemma \\ref{lem:spec1} to the latter sum"

- **context**: The supplied spec1 and spec2 statements assert only Theta<delta, not that their maximum exceeds 1. The normalization therefore needs supporting context. One cannot automatically enlarge the exponent in spec2, since it appears in a positive lower-bound term. Also, compatibility of the chosen U with U=N^u requires the omitted T-versus-N scaling. In contrast, normalizing eta0 to lie below 1 is legitimate by decreasing the positive exponent in spec3.

  Source: "1<\\gT_{1}<\\gd\n\\ee\nto be the larger of the two."

- **context**: The coset decomposition is valid, including multiplicities in F. For the application of spec1, however, the exact condition G1G is not supplied; an attached passage asserts that the stabilizer satisfies it but does not expose the condition. Constancy of the rational phase also requires that pairing with w_{x,y} preserve congruences modulo q, for example because w_{x,y} is integral. Its definition is omitted. The index estimate remains an unverified proposed premise.

  Source: "As in \\eqref{eq:G0q}, let $\\tilde\\G(q)$ be the stabilizer of $v_{0}(\\mod q)$."

- **map_correction**: The map converts a reference to sec:outline into an edge from thm:Main. That is not a proof-input edge supported by this sentence. Likewise, cMNUbnd is the announced goal, not a premise used to derive fMdecomp. The passage supplies neither positivity nor approximation of the truncated singular series, nor the subsequent transfer to M_N^U.

  Source: "We return to the setting and notation of \\S\\ref{sec:outline} with the goal of establishing \\eqref{eq:cMNUbnd}."

- **map_correction**: Spec2 is used here only to select a common exponent, not through its counting lower bound. Eq:spec1 and lem:spec1 duplicate the same premise. Eq:fMis and eq:gT1def are definitions within the target itself, so their edges should not be read as independent supporting results. These are mapping distinctions, not proof defects.

  Source: "First recall the two numbers $\\gT<\\gd$ appearing  in \\eqref{eq:spec1}, \\eqref{eq:spec2}"

Missing context: The T,T1,T2,N definitions and bounds establishing T^{delta-Theta1}<=T2 and making the chosen U a positive fixed power of N.; Support for choosing the two counting exponents so that their maximum lies strictly between 1 and delta.; The exact subgroup condition eq:G1G and its verification for the stabilizer.; The definition of w_{x,y}, or an explicit congruence-preservation statement sufficient to make the rational phase constant on stabilizer cosets.

### narrative:98161 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The target announces a transfer of an earlier bound to the Möbius-truncated major-arc term, with exceptions. The supplied representation identifies the truncation difference, but neither the earlier bound nor an estimate controlling that difference is included. The transition is therefore unverified, not demonstrably defective. No external theorem is imported; later knowledge in model weights is not used as evidence against the recorded cutoff of 2012-05-24.

Conditional inputs used: 

- **context**: The antecedent of “the same bound” is absent. The packet skips the intervening text between the major-arc setup and this announcement. Consequently, the bound's direction, scale, uniformity, integer range, and possible admissibility restriction cannot be checked. “Most of the time” also requires an explicit exceptional-set estimate and its reference population. This is a limitation of the supplied scope, not evidence of a proof defect.

  Source: "Next we derive from the above that the same bound holds for $\\cM_{N}^{U}$ (most of the time)."

- **unverified**: The supplied formula makes the difference M_N(n)−M_N^U(n) the weighted sum with inner factor ∑_{u|(2x,y), u≥U} μ(u), with the same x,y-dependent factor 𝔐_{x,y}(n). Since these Möbius coefficients have both signs, truncation gives no automatic ordering between the two major-arc terms. A quantitative estimate for this difference, strong enough at the scale of the omitted bound outside a quantified exceptional set, remains necessary. None is supplied.

  Source: "where in the last sum, $u$ ranges over $u\\mid (2x,y)$ (resp. and $u<U$)."

- **map_correction**: The dependency list is empty despite the transition relying on the definitions of both major-arc terms, their shared representation, an earlier bound, and a truncation comparison. These are candidate missing inputs, not established premises. The upstream references to spectral counting alone do not supply the local transfer estimate.

  Source: "Let $\\cM_{N}^{(U)}(n)$ denote either $\\cM_{N}(n)$ or $\\cM_{N}^{U}(n)$ from \\eqref{eq:cMNdef}, \\eqref{eq:cMNUdef}, respectively."

Missing context: The intervening statement and proof containing the bound referred to as “the same bound,” including all hypotheses and constants.; The precise meaning of “most of the time”: the range of n, whether n must be admissible, and the exceptional-set size.; The subsequent argument estimating M_N−M_N^U, including any averaging norm and its conversion to the claimed exceptional-set estimate.; The definitions of the weights and major-arc terms needed to justify the displayed summations and any tail estimates. The parameter choices Q_0, K_0, and U are supplied, but their adequacy for the transfer cannot be checked without the comparison estimate.

### narrative:99181 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The displayed algebra is locally correct, conditional on finite or absolutely convergent sums. Reversing the truncated divisor sum and using \ff=f-a gives the stated Fourier decomposition. For even u, the substitutions x_old=(u/2)x and y_old=uy are bijective; for odd u, they are x_old=ux and y_old=uy. Homogeneity gives f(ux,uy)=u²f(x,y), and dividing u² and q by their gcd gives the asserted reduced fraction without requiring (u,q)=1. The minor-arc objectives agree with the supplied reduction. However, the opening claim that the major-arc bound has been established cannot be checked from the supplied proof scope. This is a context limitation, not an identified proof defect.

Conditional inputs used: eq:IQ0, eq:IQ0K0, eq:cEN2bnd, eq:cMNUbnd, eq:cRNhatUis, eq:ffVdef

- **unverified**: The preceding argument establishing this bound is not supplied. Its exact remaining obligation is the lower bound \cM_N^U(n)≫\fS(n)T^{\gd-1} for admissible N/2<n<N, outside a set of size O(N^{1-\eta}), with the stated parameter choices. The section setup supplies a modular/archimedean decomposition but not the estimates and transfer needed for this conclusion. The claim can therefore be accepted only conditionally here.

  Source: "This establishes \\eqref{eq:cMNUbnd}, and hence completes our Major Arcs analysis"

- **context**: The rearrangement is valid for finite sums, or under absolute convergence. The packet does not define the family \fF or the support/decay of \gU sufficiently to verify this prerequisite. No analytic estimate is needed for the rearrangement once that prerequisite holds. The shift a remains attached to its corresponding form, as required.

  Source: "\\eqref{eq:cRNhatUis} and reverse orders of summation"

- **unverified**: Both displayed parity-dependent reindexings are correct. This does not by itself verify that all subsequent estimates also hold for odd u. That remaining obligation is to establish the needed estimates for the displayed sum involving f(2ux,uy), with the same required uniformity and savings. No failure of that assertion is demonstrated by this packet.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

- **map_correction**: The supplied edge from thm:Main originates from a reference to sec:outline, not to the main theorem. The main theorem is a downstream objective, not an input to this local calculation. Likewise, the references to eq:cMNUbnd, eq:cEN2bnd, eq:IQ0K0 and eq:IQ0 principally identify a completed goal or future goals; they should not be interpreted as proofs of those estimates.

  Source: "We keep all the notation of \\S\\ref{sec:outline}"

Missing context: The proof immediately preceding the opening sentence, including the major-arc lower bound, truncation transfer, exceptional-set estimates, and their parameter hypotheses.; Definitions ensuring that \fF and the weighted lattice sums are finite, or a justification of absolute convergence.; The later estimates needed to substantiate the assertion that the odd-u case is handled similarly. The target itself supplies only its correct initial reindexing.

### th_sg — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The supplied prose outlines a plausible strategy but does not establish the uniform combinatorial gap: the two announced transfer lemmas are absent, and the external spectral-gap inputs remain unverified. The missing proof anchor is a mapping limitation, not itself a proof defect. Assessment uses the recorded cutoff of 2012-05-24. No external texts or later results were used; model knowledge itself is not historically date-filtered.

Conditional inputs used: external:Brooks1986, external:Brooks2007, external:SarnakToLagarias, external:Selberg1965

- **unverified**: This is the decisive transition, but neither lemma nor its application is supplied. Generation by two subgroups with expanding congruence images does not by itself establish a uniform gap for the whole quotient family. The remaining obligation is a quantitative transfer argument whose constants are independent of q, covering all moduli, including prime powers and exceptional primes.

  Source: "We transfer the combinatorial spectral gap property\nof $\\Ga_1$ and $\\Ga_2$ to the Apollonian  group $\\bar\\Ga$\nand conclude Theorem \\ref{th_sg}.\nThis is done in following two Lemmata:"

- **context**: These are announced prerequisites, not proved here. Direct matrix checking does show that H=[[1,2i],[0,1]] fixes gamma_1 by conjugation and sends gamma_2 to gamma_3, so Gamma_2=H Gamma_1 H^{-1}; H and its inverse are integral over Z[i], making this conjugacy compatible with reduction modulo q. This supports treating the subgroups together, but does not establish finite covolume or the arithmetic/congruence identification needed to invoke Selberg.

  Source: "As we will see later, $\\bG_1$ and $\\bG_2$ are isomorphic to $\\SL(2,\\R)$.\nMoreover $\\Ga_1$ and $\\Ga_2$ are lattices inside them."

- **map_correction**: The supplied setup describes Brooks1986 as covering compact manifolds. That edge is therefore not independently sufficient for the noncompact lattice application proposed here. Brooks2007 is the proposed noncompact comparison input; its exact hypotheses, direction of implication, and uniformity for this congruence family must be checked. The four mapped references also do not account for the missing subgroup-to-group transfer lemmas.

  Source: "From here we can deduce the combinatorial spectral gap using\nBrooks \\cite[Theorem 1]{Brooks1986} (see also \\cite[Theorem 1]{Brooks2007}, where\nthe non-compact case is considered.)"

- **context**: For q=1 the quotient is trivial, so the displayed eigenvalue convention supplies no second eigenvalue lambda'_1(1). A convention that the gap assertion is vacuous for trivial quotients, or an explicit restriction to nontrivial quotients, is needed. This is an endpoint-definition issue rather than evidence against the substantive expansion claim.

  Source: "There is an absolute constant $c>0$ such that $\\gl_1'(q)<1-c$ for all $q$."

Missing context: The two announced lemmas, their proofs, and their application yielding a q-independent gap for the fixed generating set bar S.; Proof that Gamma_1 is the required finite-covolume arithmetic subgroup, and identification of its induced congruence kernels with a family covered by the cited geometric-gap theorem.; Exact Selberg theorem and noncompact geometric-to-combinatorial comparison theorem, including hypotheses, constants, and source versions containing the needed results before 2012-05-24.; A convention for lambda'_1(q) when the congruence quotient is trivial.

### th_sg — gemini-4-argon

Delivery: completed; local status: needs_context.

Theorem th_sg is the main combinatorial spectral gap theorem of the Appendix. Because proof_anchor_missing is true, the supplied source_slice contains only the statement of Theorem th_sg and the introductory outline that defines the subgroups \Ga_1 and \Ga_2 and defers the proof to the 'following two Lemmata' after line 5483. Consequently, verifying Theorem th_sg requires the omitted remainder of the Appendix containing those two lemmata and the concluding deduction of Theorem th_sg.

Conditional inputs used: external:Brooks1986, external:Brooks2007, external:SarnakToLagarias, external:Selberg1965

- **context**: The attached prose is a narrative outline rather than a complete proof of Theorem th_sg. It explicitly defers the proof of Theorem th_sg to two subsequent lemmata (and any concluding argument) located after line 5483, outside the supplied source_slice.

  Source: "We transfer the combinatorial spectral gap property\nof $\\Ga_1$ and $\\Ga_2$ to the Apollonian  group $\\bar\\Ga$\nand conclude Theorem \\ref{th_sg}.\nThis is done in following two Lemmata:"

- **map_correction**: The reference edge from external:SarnakToLagarias to th_sg arises from the candidate prose following the theorem statement. In the text, Sarnak (2007) is cited for historical attribution of a structural observation that the author states will be proved later in the section ('As we will see later...'), while the actual proof inputs to th_sg are the two subsequent lemmata not yet in the map.

  Source: "As we will see later, $\\bG_1$ and $\\bG_2$ are isomorphic to $\\SL(2,\\R)$.\nMoreover $\\Ga_1$ and $\\Ga_2$ are lattices inside them.\nThis feature of the\nApollonian group was pointed out by Sarnak \\cite{SarnakToLagarias}."

- **unverified**: The prose sketches why congruence quotients of \Ga_1 and \Ga_2 have combinatorial spectral gaps by invoking Selberg (1965) for the geometric spectral gap of congruence subgroups of lattices in SL(2,R) and Brooks (1986, Theorem 1; 2007, Theorem 1) for the equivalence with combinatorial spectral gap in the non-compact case (note \Ga_1 and \Ga_2 contain the parabolic element \g_1, so their quotients are non-compact). All three external sources predate the 2012-05-24 cutoff (published in 1965, 1986, and 2007 respectively), but their external texts are not supplied in the packet and it remains to check the subsequent lemmata to see whether this deduction is formalized there or used directly as an unexpanded premise.

  Source: "Due to a result going back to\nSelberg \\cite{Selberg1965}, $\\Ga_1$ and $\\Ga_2$ have geometric spectral gaps with\nrespect to the congruence subgroups.\nFrom here we can deduce the combinatorial spectral gap using\nBrooks \\cite[Theorem 1]{Brooks1986} (see also \\cite[Theorem 1]{Brooks2007}, where\nthe non-compact case is considered.)"

Missing context: The remainder of the Appendix after line 5483 (char 131279), specifically the statements and proofs of the 'following two Lemmata' and the concluding deduction of Theorem th_sg from them.; Exact statements and hypotheses of Selberg (1965) and Brooks (1986, Theorem 1; 2007, Theorem 1) if the subsequent lemmata rely on the prose paragraph in lines 5469-5476 as the sole justification for the combinatorial spectral gap of \Ga_1 and \Ga_2.

### thm:CircMeth — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The theorem is locally supported as a conditional assembly of the five supplied major- and minor-arc estimates. The Fourier definitions give the decomposition, the two major-arc theorems give the main-term bound, and Parseval plus the three minor-arc theorems give the error bound after absorbing the logarithmic number of dyadic blocks. This does not establish those dependency theorems. The missing proof anchor is a mapping limitation, not a demonstrated proof defect.

Conditional inputs used: eq:Q0is, eq:IQ0K0, eq:IQ0, eq:IQdef, thm:cMNis, thm:cMNtoMNU, thm:IQ0, thm:IQX, thm:IQM, thm:RNU

- **context**: This transition is correct: adding the two defining integrals cancels the cutoff, and Fourier orthogonality recovers the truncated representation function. The supplied exponential sum has finite support in its summation variables. Parseval applies to the resulting square-integrable periodic function; bounding the sum over all integer n also bounds the stated sum over n<N.

  Source: "so that \\eqref{eq:RNcMcE} obviously holds."

- **context**: The weighted estimate requires nonoverlapping cutoff spikes. This follows from the supplied parameters: writing a=δ−Θ1, the supplied bounds give 0<a<1 and Q0=N^(a/2000). Thus 2K0Q0²/N=2Q0⁴/N tends to zero, while Q0³M/N tends to zero because M=N^(101/200). Consequently the spikes are disjoint and their widths fit inside the relevant small-denominator approximation windows. Away from their supports the weight is 1; Dirichlet coverage supplies the remaining regions up to a null set. Overlap between approximation regions is harmless for this upper bound.

  Source: "where we have dissected the circle into the following regions (using that $|1-\\ft(x)|=|x|$ on $[-1,1]$):"

- **unverified**: Conditional on these estimates holding uniformly in their stated Q-ranges, the minor-arc conclusion follows. If η* is the minimum of their saving exponents and that of thm:IQ0, there are O(log N) blocks, giving an error bound with any fixed exponent smaller than η*. Taking a further minimum with the exceptional-set exponent in thm:cMNtoMNU supplies one η for both conclusions. The dependency proofs are not provided or verified here.

  Source: "see Theorems \\ref{thm:IQX} and \\ref{thm:IQM}, respectively."

- **map_correction**: Only the specification of the singular series is needed from thm:RNU; its representation lower bound must not be treated as an input proving CircMeth. Likewise eq:RNcMcE, eq:cMNUbnd and eq:cEN2bnd are the target's own conclusions, not independent premises. The references to eq:nZbnd and eq:nmRest supply an analogy and parameter motivation, respectively, rather than proofs of this theorem.

  Source: "The singular series $\\fS(n)$ is the same as in Theorem \\ref{thm:RNU}."

- **context**: The immediately attached proof establishes the downstream implication CircMeth⇒RNU, not CircMeth itself. Its power-saving count uses the singular-series lower bound and an arbitrarily small ε; the displayed squared estimate requires the usual relabelling of ε. This attachment therefore does not close the target's dependency proofs.

  Source: "Proof of Theorem \\ref{thm:RNU} assuming Theorem \\ref{thm:CircMeth}:"

- **context**: The outline supports the assembly described above, not verification of the later estimates. No external text or theorem is imported in this assessment. The recorded cutoff is 2012-05-24. Model knowledge cannot itself be temporally filtered, so possible later knowledge is not used as evidence.

  Source: "This completes our outline of the rest of the paper."

Missing context: Proofs of thm:cMNis, thm:cMNtoMNU, thm:IQ0, thm:IQX and thm:IQM, including their prerequisite hypotheses and any historically admissible external inputs.; Explicit confirmation that the minor-arc estimates have saving exponents and implied constants uniform over their stated Q-ranges.; The omitted preamble defining macros such as \foh, and the conventional restriction of r to reduced residue representatives modulo q in the periodized cutoff.

### thm:IQM — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The supplied packet states the large-denominator estimate but does not supply its proof or the preceding diagonal/off-diagonal bounds needed to establish it. The missing proof anchor is a mapping limitation, not evidence that the theorem is false. The closing paragraph identifies IQM, IQ0 and IQX as inputs to the error-energy bound, not as proofs of one another. There is also a sign inconsistency in the supplied setup. No external result is imported under the recorded 2012-05-24 cutoff; although later knowledge may remain in model weights, it is not used to discharge this obligation.

Conditional inputs used: thm:IQ0, thm:IQX

- **unverified**: This states the target but supplies no derivation. The section setup only reaches a diagonal/off-diagonal decomposition. The exact remaining obligation is to bound both resulting contributions by N T^{2(delta-1)} N^{-eta}, accounting for the u, q, frequency and form sums, uniformly over the asserted Q-range. Neither IQ0 nor IQX covers this range.

  Source: "If $X\\le Q<M$, then there is some $\\eta>0$ so that"

- **context**: The definition of I_Q is absent, as are the parameter relations and hypotheses on the forms, weights and truncations. Thus the hypotheses X <= Q < M and N tending to infinity cannot be checked against the actual integral. For the subsequent summation, eta and the implied constant must be sufficiently uniform in Q; the statement alone does not document that uniformity.

  Source: "In this section, we continue our analysis of $\\cI_{Q}$ from \\eqref{eq:IQdef}"

- **error**: In the displayed expansion IQbnd2, this archimedean phase has the opposite sign from direct multiplication of the factors in cRsq2: e(-a beta) times the conjugate of e(-a' beta) equals e(beta(a'-a)). The modular phase in IQbnd2 already uses a'-a. No compensating change of variables is supplied. This is an inconsistency in the attached setup, not by itself a disproof of IQM.

  Source: "e(\\gb (a-a'))"

- **map_correction**: These references describe a downstream assembly. They do not support edges IQ0 -> IQM, IQX -> IQM, cEN2bnd -> IQM or Main -> IQM. The proposed proof direction is instead IQ0, IQX and IQM jointly toward cEN2bnd, followed by additional reductions toward Main.

  Source: "Finally, Theorems \\ref{thm:IQ0}, \\ref{thm:IQX},  and \\ref{thm:IQM} together complete the proof of \\eqref{eq:cEN2bnd}, and hence Theorem \\ref{thm:Main} is proved."

- **unverified**: Conditionally on the three estimates, this transition still requires an inequality controlling the Fourier error energy by these integrals, coverage of all minor arcs, and control of the number of Q-blocks. For polynomially bounded M and logarithmically many blocks, uniform positive savings can absorb the logarithm after decreasing eta; those prerequisites are not supplied. The further conclusion Main also requires the major-arc lower bound and the representation/truncation reductions, not just the error-energy estimate.

  Source: "together complete the proof of \\eqref{eq:cEN2bnd}"

Missing context: The proof preceding thm:IQM, especially the final bounds for I_Q^{(=)} and I_Q^{(neq)} and their parameter restrictions.; Definitions eq:IQdef, eq:IQ0K0 and eq:IQ0, and the Fourier/Parseval inequality connecting those integrals to eq:cEN2bnd.; Definitions and asymptotic relations for X, M, T, U, Q_0, K_0 and delta, including the allowed Q-blocks and uniformity of eta and implied constants.; Definitions eq:tilQis and eq:cSdef, the family of forms and its coefficient bounds, and the smooth weight hypotheses needed for completion and subsequent estimates.; For the closing headline inference only: established major-arc bounds, the singular-series lower bound, and the reductions connecting the truncated representation function to curvatures.

### thm:IQX — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The packet states the desired power-saving estimate but supplies no proof of it. The section setup gives a conditional algebraic reduction to diagonal and off-diagonal contributions; it does not bound either contribution. Missing definitions, parameter relations, and subsequent estimates prevent verification. The absent proof anchor is a mapping limitation, not evidence that the theorem is defective.

Conditional inputs used: 

- **map_correction**: The target slice contains only the theorem statement and whitespace. The attached section setup precedes the target and cannot be treated as its complete proof. No dependency or proof-reference edges are supplied; the proof location and its actual inputs remain unidentified.

  Source: "\\begin{thm}\\label{thm:IQX}"

- **context**: The definition of the quantity being bounded is omitted. Also missing are the meanings and allowed ranges of N, T, X, M, U, Q_0 and delta; the family of forms; and the definitions of the modular and archimedean factors. The standing assumption of a fixed primitive integral gasket does not supply these analytic prerequisites.

  Source: "Keeping all the notation from the last section,  we now turn our attention to the integrals $\\cI_{Q}$ in \\eqref{eq:IQdef}."

- **unverified**: The factor U is consistent with Cauchy–Schwarz for a sum containing O(U) integer indices. This requires the omitted summation convention and preceding representation. Conditional on those identities and justified sum/integral interchanges, opening the square produces the displayed conjugations and phases a'-a. The packet does not provide the convergence or truncation information needed to verify these operations fully.

  Source: "applying Cauchy-Schwarz in the $u$-variable:"

- **unverified**: Partitioning pairs according to a'=a or a'≠a is exhaustive, but the two contributions are not explicitly defined or estimated here. Because the expanded expression contains complex terms, one must also specify whether these contributions are signed subsums, absolute values of subsums, or nonnegative majorants. The remaining substantive obligation is to bound their combined contribution by N T^{2(delta-1)} N^{-eta}, uniformly over the asserted Q-range.

  Source: "\\cI_{Q}\\ll \\cI_{Q}^{(=)}+\\cI_{Q}^{(\\neq)},"

- **context**: Verification requires the parameter choices as N tends to infinity, the quantifier governing eta across the Q-range, and the permitted dependence of the implied constant. None is specified in this packet. In particular, no supplied estimate explains how a positive saving survives losses involving U or the family of forms.

  Source: "For $Q_{0}\\le Q<X$, there is some $\\eta>0$ such that"

Missing context: The actual proof of thm:IQX, including the diagonal and off-diagonal estimates and their combination.; Definitions and parameter restrictions for I_Q, Q_0, X, M, U, T, N and delta, including their dependence on N.; Definitions of the form family, a, q_0, u_0, J_f and S_f, together with the identities referenced in the section setup.; Support, decay or convergence statements justifying expansion and interchange of sums and the beta-integral.; Any external results used by the missing proof, with exact statements, hypotheses and versions available by 2012-05-24. No external result is imported in this assessment; model background knowledge alone cannot certify historical availability.

### thm:IQX — gemini-4-argon

Delivery: completed; local status: needs_context.

Theorem thm:IQX is stated at the end of Section sec:QX as the culmination of the preceding analysis, with only a page break following it. While the section setup (lines 4410-4517) provides the initial Cauchy-Schwarz step and the decomposition I_Q << I_Q^{(=)} + I_Q^{(\neq)} in (eq:cIQ12), the entire body of the argument bounding I_Q^{(=)} and I_Q^{(\neq)} (lines 4518-4837) is omitted from the packet and no dependencies are supplied. Verification requires the missing text from lines 4518-4837 as well as the parameter definitions from earlier sections.

Conditional inputs used: 

- **context**: Theorem thm:IQX is stated at the very end of Section sec:QX (immediately before \newpage) without a following proof environment. Its derivation relies on the omitted text of Section sec:QX between lines 4517 and 4838, where the diagonal and off-diagonal terms in (eq:cIQ12) are analyzed.

  Source: "\\begin{thm}\\label{thm:IQX}\nFor $Q_{0}\\le Q<X$, there is some $\\eta>0$ such that \n$$\n\\cI_{Q}\\ll N\\, T^{2(\\gd-1)}\\, N^{-\\eta},\n$$\nas $N\\to\\infty$.\n\\end{thm}"

- **map_correction**: The section setup decomposes I_Q into I_Q^{(=)} and I_Q^{(\neq)}, but the subsequent estimates for these two pieces (lines 4518-4837) are omitted from the packet and no dependency nodes for them are supplied.

  Source: "Decompose   \\eqref{eq:IQbnd1} as\n\\be\\label{eq:cIQ12}\n\\cI_{Q}\\ll \\cI_{Q}^{(=)}+\\cI_{Q}^{(\\neq)},\n\\ee\nwhere, once $\\ff$ is fixed,  we collect $\\ff'$ according to whether $a'=a$ (the ``diagonal'' case) and the off-diagonal $a'\\neq a$."

- **context**: The definitions and parameter relations for I_Q, Q_0, Q, X, N, T, and \delta from earlier sections are referenced but not included in the bounded context.

  Source: "Keeping all the notation from the last section,  we now turn our attention to the integrals $\\cI_{Q}$ in \\eqref{eq:IQdef}."

Missing context: Lines 4518-4837 of Section sec:QX, which contain the bounds for the diagonal contribution I_Q^{(=)} and off-diagonal contribution I_Q^{(\neq)} and the concluding argument for Theorem thm:IQX.; The definition of I_Q in equation (eq:IQdef) and the definitions/growth relations of the parameters N, T, \delta, Q_0, Q, and X as N \to \infty.

### thm:Vin — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The packet identifies a proposed external proof input but does not supply its statement or the reduction establishing the asserted uniform sector estimate. The radial normalization checks directly. Coordinate choices, Patterson–Sullivan normalization, and the spectral-gap parameter require clarification. The normalizer description contains an elementary error. These issues do not establish that the counting theorem is false; the missing proof anchor is a mapping limitation. No later theorem is used to close the obligation.

Conditional inputs used: eq:gDecomp, eq:muPS, external:Vinogradov2013

- **unverified**: Theorem 2.2 is not supplied or inspected, so its exact statement, hypotheses, normalization, and error term remain unverified. Historical record for this proposed input: available_from=unresolved; date_evidence="Princeton University Thesis 2012, arxiv:1204.5498v1"; date_basis=bibliographic preprint identifier, indicating April 2012 but without an inspected submission record; version=arXiv v1, contents unverified. The 2013 journal reference is after the 2012-05-24 cutoff and cannot alone justify the original argument. The needed result must be located in the pre-cutoff version. Model knowledge is not dated evidence.

  Source: "The following theorem follows easily              \nfrom \\cite[Thm 2.2]{Vinogradov2013}."

- **unverified**: This is stronger than a separate asymptotic for each fixed sector. The remaining obligation is to show that the cited theorem directly covers arbitrary caps and intervals with this uniformity, or to supply a quantitative approximation argument controlling all their boundaries uniformly. Likewise, the packet does not establish a single exponent Θ<δ depending only on the stated spectral gap.

  Source: "The implied constant does not depend on $\\Phi,\\Psi,$ or $\\cI$."

- **error**: The displayed diagonal group M is the centralizer, not the full normalizer. Directly, w=[[0,1],[-1,0]] belongs to SU(2), is not in M, and satisfies wa_tw^{-1}=a_{-t}. For t>0, the usual residual ambiguity in the positive Cartan decomposition is by M. Thus the normalizer terminology is incorrect, although this alone does not refute the intended counting statement.

  Source: "We have the Cartan decomposition $G=KA^{+}K$, unique up to the normalizer $M$ of $A$ in $K$."

- **context**: Elements of K/M cannot literally be multiplied as matrices. Representatives, or a specified section K/M→K, are needed to define m(g); changing those representatives changes its angular coordinate. The section and its regularity must match the external theorem. In addition, the decomposition is stated only outside K, whereas the target sums over every γ∈Γ, including the identity. Since a discrete subgroup intersects compact K finitely, an explicit convention can address these exceptional terms, but none is supplied.

  Source: "g=s_{1}(g)\\cdot a(g)\\cdot m(g) \\cdot s_{2}(g)^{-1}."

- **context**: The Patterson–Sullivan measure must be based at the point compatible with the chosen K-boundary identification, with normalization matched to c_δ. The approximate description by orbital measures does not specify that compatibility. An arbitrary change of basepoint changes the boundary density, generally not merely its total mass, so this cannot automatically be absorbed into one scalar coefficient.

  Source: "$\\fo$ is any fixed point in $\\bH^{3}$."

- **context**: The supplied setup proposes discreteness, geometric finiteness, non-elementarity, infinite covolume, and the inherited restriction Γ<SL(2,Z[i]); the target additionally requires δ>1. These are premises here, not established facts. The packet omits the intervening spectral-gap definition and theorem, so the exact gap hypothesis and its relation to Θ cannot be checked.

  Source: "Then under the above hypotheses on $\\G$ (in particular $\\gd>1$)"

- **context**: The elementary radial conversion is consistent: ||a_t||²=e^t+e^{-t}. For T>2, the cutoff is t<arcosh(T/2)=log T+O(T^{-2}). Thus converting an e^{δt} main term gives T^δ(1+O(T^{-2})); with δ<2, this normalization introduces no growing main-term discrepancy. This check does not establish the angular estimate.

  Source: "$\\|\\cdot\\|$ is the  Frobenius norm"

Missing context: A dated record and the actual text of arXiv:1204.5498v1, especially Theorem 2.2 and equation (3.4), showing that the required result was available by 2012-05-24.; The precise Cartan sections, their exceptional sets, the M-coordinate convention, and treatment of Γ∩K.; The Patterson–Sullivan basepoint and normalization compatible with K, together with the spectral-gap definition used to determine Θ.; A direct citation or derivation establishing the uniform error for all spherical caps and M-intervals. The missing proof anchor itself is not evidence of a proof defect.

### thm:cMNtoMNU — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The truncation argument is conditionally sound for admissible n, but the packet does not establish several estimates needed by its displayed L1 bound. The principal missing input is a uniform bound for the finite modular factor for every pair occurring in the discarded Möbius tail; the stated bound for the completed singular series does not itself supply this. The lattice-tail count and parameter-error absorption check directly. Completing the exceptional-set argument also requires the omitted scale relation and a power-growth statement for U. No supplied dependency is treated as established.

Conditional inputs used: eq:Q0is, eq:cMNUn, eq:cMNbnd, eq:fMdecomp, eq:fSbnd, eq:nZbnd

- **unverified**: The second displayed inequality requires a bound such as |S_{Q0,x,y}(n)| ≪ε N^ε, uniformly over the supported x,y, including those with gcd(2x,y) ≥ U. Equation fSbnd bounds the completed singular series S(n), not this finite factor. A completed-series bound alone does not control partial sums without a tail or absolute-convergence estimate. Moreover, the transitivity passage used earlier to remove x,y must apply to these nonprimitive pairs, or a separate uniform estimate is needed. The relevant congruence-orbit hypotheses are omitted, so applicability cannot be checked.

  Source: "using \\eqref{eq:fSbnd} and \\eqref{eq:Q0is}."

- **context**: Reducing this expression to O(T^δ) requires both #F ≪ T^δ, with the intended multiplicities, and the uniform sampling bound (K0/N) Σ_{1≤n<N} hat(t)((a−n)K0/N) ≪ 1. Positivity is stated in the surrounding excerpt, but the definition and decay of hat(t), the requisite scale K0/N, and the upper cardinality bound for F are not supplied.

  Source: "\\sum_{\\ff\\in\\fF}\n{K_{0}\\over N}\n\\left[\n\\sum_{n<N}\n\\hat\\ft"

- **context**: The parameter absorption is correct: writing Δ = δ−Θ1 > 0 gives K0²Q0⁴T^Θ1 = T^(Θ1+2Δ/5) = T^(δ−3Δ/5) ≤ T^δ. Also, for nonzero y on support of size O(X), swapping the u and y sums bounds the lattice tail by Σ_{U≤u≤CX} O(X/u)O(X/u) ≪ X²/U; the condition u | 2x changes only an absolute constant. These checks support the last inequality once the modular and sampling inputs are supplied.

  Source: "K_{0}^{2}Q_{0}^{4}T^{\\gT_{1}}"

- **context**: For admissible n, conditional on the supplied lower bounds, let D(n)=|M_N(n)−M_N^U(n)|. Outside D(n) ≥ (c/2)S(n)T^(δ−1), the desired lower bound follows from M_N(n) ≥ cS(n)T^(δ−1). The displayed L1 estimate and S(n) ≫ε N^(−ε) give an exceptional count ≪ N^(2ε)TX²/U. Obtaining a power saving requires TX² ≍ N and U ≥ N^κ for some κ>0. U is defined in the packet, but the required relation between T and N is not.

  Source: "The rest of the argument is identical to that leading to \\eqref{eq:nZbnd}."

- **unverified**: The referenced theorem is stated for N/2<n<N without an admissibility restriction, whereas its singular series vanishes at non-admissible n. The L1 transfer using a positive singular-series lower bound proves the assertion only for admissible n. It does not establish M_N^U(n) ≥ 0 for most non-admissible n. The surrounding major-arcs objective explicitly concerns admissible n, so the intended scope should be supplied rather than assumed.

  Source: "the bound \\eqref{eq:cMNbnd} holds with $\\cM_{N}$ replaced by $\\cM_{N}^{U}$"

- **map_correction**: The edge from eq:nZbnd records a proof-method analogy, not a sufficient numerical premise for this target. Its earlier argument concerns different functions and exceptional sets. Direct proof inputs omitted from the proposed dependency list include the definition of U, the scale relation TXNis, and the sampling/cardinality estimates.

  Source: "The rest of the argument is identical to that leading to \\eqref{eq:nZbnd}."

- **unverified**: This external text has not been inspected. If used to discharge the modular estimate, its exact result, hypotheses, available_from, date_evidence, date_basis, and version remain unresolved against the recorded cutoff 2012-05-24. No external theorem is imported in this assessment. Model training may contain later knowledge; that knowledge is not being used as historical evidence.

  Source: "See, e.g. \\cite[\\S4.3]{BourgainKontorovich2010}."

Missing context: A uniform finite-modular-factor estimate for all x,y in the discarded Möbius tail, including its congruence-orbit hypotheses and any required tail estimate.; The definition and decay properties of hat(t), and a uniform normalized sampling bound.; The definition and upper cardinality estimate for F, including multiplicities.; Equation TXNis and the T-versus-N scaling needed to make U a fixed positive power of N.; Clarification whether the target is restricted to admissible integers.; A dated, version-specific source record for any external result actually used to close the modular obligation.

### thm:specGap — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The supplied packet does not contain the announced Appendix proof. Conditional on the spectral premises, the excerpts describe spectra at individual levels but do not establish a gap uniform in q. The statement also needs clarification of its inherited dimension hypothesis and of λ₁(q) when no second discrete eigenvalue exists. These are bounded contextual and mapping issues, not a verdict against the theorem in its full setting. No external theorem or later development is imported; my stored knowledge is not chronologically filtered and is not used to fill the missing argument.

Conditional inputs used: eq:glQs, eq:gls

- **unverified**: The actual proof is explicitly located outside the supplied excerpts. Its absence is a mapping limitation, not evidence of a defective proof. The remaining obligation is to establish one ε(Γ)>0 valid for every positive integer q, rather than merely isolation of the base eigenvalue at each fixed level.

  Source: "This is proved in the Appendix by P\\'eter Varj\\'u."

- **context**: The supplied setup assumes geometric finiteness, discreteness, non-elementarity, infinite covolume, and Γ<SL(2,Z[i]); it gives 0<δ<2 but does not explicitly assume δ>1. Conditional on this spectral premise, when δ≤1 there is no discrete base eigenvalue to which the displayed theorem can refer. Clarify whether an earlier hypothesis restricts Γ to δ>1 or whether another interpretation of λ₀ is intended.

  Source: "The latter is empty unless $\\gd>1$"

- **context**: This enumeration presupposes a second discrete eigenvalue below 1. Even the supplied δ>1 spectral premise only provides a base eigenvalue; it does not guarantee a second one. The definition of λ₁(q), including levels with only the base eigenvalue, is missing. This also affects q=1.

  Source: "0<\\gl_{0}(q)<\\gl_{1}(q)"

- **unverified**: Accepting this supplied equality conditionally identifies the common base, but supplies no uniform separation above it. Likewise, discreteness at each level would give only level-dependent gaps; it does not establish that their infimum over q is positive.

  Source: "\\gl_{0}(q)=\\gl_{0}=\\gd(2-\\gd)."

- **map_correction**: The eq:gls and eq:glQs reference edges arise in a subsequent representation-theoretic discussion. That transition describes individual level decompositions, not uniform exclusion of complementary-series parameters approaching the base parameter. Treat these edges as spectral setup, not as a proof of the gap.

  Source: "Obviously, a similar decomposition holds for $L^{2}(\\G(q)\\bk G)$, corresponding to \\eqref{eq:glQs}."

- **map_correction**: This citation supports the following representation-theoretic interpretation, not the preceding theorem. The Cowling–Haagerup–Howe citation likewise introduces subsequent mixing estimates; the supplied slice states no such estimate, only a Sobolev norm. These reference locations do not establish either citation as a proof input for thm:specGap.

  Source: "By the Duality Theorem of Gelfand, Graev, and Piatetski-Shapiro \\cite{GelfandGraevPS1966}"

Missing context: The Appendix statement and proof corresponding to thm:specGap, with all hypotheses and its connection to the main-text formulation.; An explicit inherited δ>1 hypothesis, or clarification of the spectral notation outside that range.; The definition of λ₁(q) when there is no second discrete eigenvalue below 1.; An argument covering every positive integer q, including prime powers and any exceptional levels, with a constant depending only on Γ.; For any external result needed by the Appendix: its exact theorem and hypotheses, verification of applicability, and available_from, date_evidence, date_basis, and version establishing availability by 2012-05-24. The supplied bibliography alone does not provide those theorem-level checks.

## Wave 1

eq:cI3bnd, eq:cI42bnd, eq:cIQ12bnd, eq:cIQ1def, eq:hatRfuBnd, eq:nmUpToM, lem:spec1, lem:spec2, lm_generation, thm:RNU

### eq:cI3bnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The displayed estimation is algebraically correct conditional on the supplied lemmas, the ensemble bound |F| ≪ T^δ, uniform coefficient bounds |a| ≪ T, and a modest upper bound on δ. These additional prerequisites are not established in the packet. No local arithmetic defect was found, including at Q = X. This is not a verdict on the dependency proofs. Model knowledge may include later developments; no external result or later development is used here.

Conditional inputs used: eq:Mis, eq:TXNis, eq:cIQ3def, eq:fuIs, eq:modBndaNeqAp, eq:tilQis

- **context**: The elementary loss calculation checks out: (q/q0)^2 ≤ u^4, and the square root of the two gcd factors is at most |aa'|. For a ≠ a', gcd(a−a',q) ≤ |a−a'|. The u^4 cancels the weight u^−4. Counting O(U) values of u, O(Q) moduli, and O((UQ/X)^4) frequency quadruples yields U^6 X^−1 Q^(11/4) T^(2δ+5/4), assuming the ensemble bounds below. Since Q < XT, this is at most U^6 X^(7/4) T^(2δ+4), exactly as claimed.

  Source: "\\tilde q:=(u^{2},q)"

- **unverified**: The second displayed inequality uses an unstated bound |F|^2 ≪ T^(2δ), together with |a|, |a'| ≪ T and |a−a'| ≪ T. The contextual discussion announces an order-T condition for a_gamma, but the packet does not define F or establish its size and its relation to those coefficients. If positivity of a and a' is not part of that definition, the first displayed upper bound should be read with |aa'|.

  Source: "T^{2\\gd}"

- **unverified**: The modular lemma is supplied only with this notation-dependent qualification. The section setup identifies its modular component with S, but the definitions of S, the normalized sums S_f, and the permitted family of forms are absent. Its applicability to the forms and all frequencies in eq:cIQ3def therefore remains conditional, rather than independently verified.

  Source: "With the above  notation,"

- **context**: This exponent is correct. Combining the supplied definitions gives U^6 = N^[3(δ−Θ1)η0^2/100000]. Thus the remaining factor is N^[−59/800 + 3(δ−Θ1)η0^2/100000]. A positive saving follows provided (δ−Θ1)η0^2 < 7375/3. The packet gives 1 < Θ1 < δ and 0 < η0 < 1, but no upper bound on δ. The intended geometric range would readily suffice, but its definition or bound must be supplied rather than imported.

  Source: "X^{-1/4}T^{5}=N^{-59/800}"

- **map_correction**: The final step also uses eq:Q0is to turn the definition of U into a power of N. That definition appears inside the supplied eq:fuIs context but has no separate incoming edge. The ensemble size and coefficient estimates are additional omitted proof inputs. These are mapping/context limitations, not established proof defects.

  Source: "so together with \\eqref{eq:fuIs}, this is clearly a substantial power savings."

Missing context: The definition and counting estimate for F sufficient to justify |F|^2 ≪ T^(2δ), or an explicitly controlled variant.; The identification of each coefficient a with the order-T coefficient announced in the ensemble construction, including its sign if the displayed factor aa' is used literally.; Definitions of S, S_f, and the family of forms, sufficient to check the hypotheses and uniformity of eq:modBndaNeqAp in this application.; The definition or an upper bound for δ ensuring (δ−Θ1)η0^2 < 7375/3.

### eq:cI42bnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

Conditional on the two supplied lemmas, the displayed algebra is consistent, including X^{-1/8}T^{35/8}=N^{-29/1600}. The section supplies Q≥X, and a=a' makes the stated inequality of shifted-form values equivalent to the inequality required by eq:modBndaEqAp. However, the packet omits the growth restriction on U and the ensemble and modulus definitions needed for the intermediate estimates. Consequently, the claimed power saving is not yet locally established. All three supplied dependency edges are relevant; their premises have not been independently established. No external result is imported: the recorded cutoff is 2012-05-24, and model recall is not treated as dated evidence.

Conditional inputs used: eq:TXNis, eq:cIQ3def, eq:modBndaEqAp

- **unverified**: The final factor is N^{-29/1600}U^{13}T^{ε}. Thus a positive saving requires U^{13}T^{ε}≪N^{29/1600−η} for some η>0. For example, if U≪N^κ, one needs 13κ+ε/100<29/1600. No definition or growth restriction for U is supplied. This is the exact outstanding obligation at the final transition, not an arithmetic error in the displayed N-exponent.

  Source: "so we have again a power savings, as claimed."

- **context**: The modular reduction needs q₀|q and q/q₀≤u² to replace (q/q₀)^5 by u^{10}. It also needs a≠0 and |a|≪T. Then (a²,q₀) can be majorized by a divisor sum over divisors of a² that divide q; summing q≈Q contributes O(Q) per divisor, and the elementary divisor bound gives T^{ε}. The definition of q₀ is absent. The introductory requirement a_γ≈T is stated, but its link to every indexed form parameter a is not supplied.

  Source: "\\sum_{\\tilde q_{1}\\mid a^{2}\\atop \\tilde q_{1}\\ll Q}"

- **context**: The next displayed line replaces this unrestricted pair sum by a factor T^{2δ}. This needs an ensemble cardinality estimate such as #F≪T^δ, or an estimate with arbitrarily small losses absorbed into T^{ε}, counting any multiplicities. Neither the definition of F nor that estimate is included. Dropping a'=a after applying an a'-independent nonnegative majorant is otherwise legitimate.

  Source: "\\sum_{\\ff,\\ff'\\in\\fF}"

- **context**: The value bound requires coefficient control for every form in F, including its constant term. Such control is asserted here but cannot be checked without the form construction. Conditional on that control and the preceding inputs, put L=UQ/X: summing u^{6} gives U^{7}, the four frequency variables give L^4, and the value-difference factor gives T^{1/2}L. The result is U^{13}X^{-2}T^{2δ−1/2+ε}Q^{31/8}. Using Q<XT yields exactly the displayed X²T^{2δ−1}·X^{-1/8}T^{35/8}U^{13}T^{ε}.

  Source: "$\\ff(m,n)\\ll T (UQ/X)^{2}$ and $Q<XT$."

Missing context: The definition and N-growth restriction of U, sufficient to make N^{-29/1600}U^{13}T^{ε} a fixed negative power of N.; The omitted modulus definition eq:tilQis, establishing q₀|q and q/q₀≤u².; The construction of F and its cardinality estimate, including multiplicities.; The uniform coefficient bounds for forms in F and the identification of their parameter a with the stated nonzero quantity of order T.; The definition of the subpiece I_Q^(=,≠), confirming that its restrictions are precisely a=a' and unequal form values as used in the first proof line.

### eq:cIQ12bnd — gpt-6.1-sol

Delivery: completed; local status: defective.

Conditional on the counting lemma and omitted definitions, the intended gcd reduction is sound. However, the displayed proof drops coprimality restrictions needed for its modulus count and asserts a weighted-sum estimate not valid throughout the supplied range 0<eta_0<1. Additional context is also required to convert the resulting parameter saving into N^{-eta}. This is a local proof assessment, not a verdict on the proposition itself. No external result or later development is used; possible later knowledge in model training is not evidence here.

Conditional inputs used: eq:His, eq:fuIs, lem:spec3

- **error**: The preceding estimate requires controlling Q^{-1/4} sum_{d<=CQ} d^{-3/4-eta_0}. Direct summation gives O(Q^{-eta_0}) only for eta_0<1/4; at eta_0=1/4 there is a logarithm, and for eta_0>1/4 the bound is O(Q^{-1/4}). In the last case, even the d=1 term prevents the asserted O(Q_0^{-eta_0}) estimate when Q=Q_0 tends to infinity. The supplied parameter definition assumes only 0<eta_0<1. An explicit sufficiently small choice of the lemma's exponent is missing.

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

- **unverified**: For the actual gcd variables, the pairwise-coprimality assertion is correct: writing d=(a-a',q), one has gcd((a,q),d)=h, and similarly for a'. Thus the actual lcm is h*g_1*g_1'*tilde_g. But the displayed enlarged divisor sums omit these coprimality restrictions before replacing the number of q by O(Q/(g_1*g_1'*tilde_g)). That replacement is not valid for unrestricted tuples: g_1=g_1'=tilde_g=p and h=1 gives lcm p rather than p^3. The restrictions must remain in force through the counting step. This is an omission in the displayed argument, not a failure of the actual-gcd identity.

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

- **context**: The packet does not contain eq:cIQ1def or the precise definition of this contribution. Consequently, the initial equality with the positive arithmetic sum cannot be checked. The neighboring large-gcd argument starts with an upper bound. Independently, the subsequent elementary inequality sqrt(gcd(a^2,q))<=gcd(a,q) is valid.

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

- **context**: This application is conditional on identifying the form-indexed family, including multiplicities, with the gamma-indexed family in the lemma, with a=<e_1,gamma v_0>. Every modulus tilde_g must satisfy 1<=tilde_g<N; Q<X alone does not establish this without the missing scale relations. The divisor bounds absorbed into T^{epsilon} also require nonzero a,a' of polynomially bounded size. Once the indexing is justified, the outer cardinality bound T^delta follows from the supplied lemma at modulus 1.

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

- **context**: Conditional on the asserted Q_0^{-eta_0} estimate, the parameter algebra checks: U^6 H^{9/4} Q_0^{-eta_0}=Q_0^{-c}, where c=31*eta_0/40-3*eta_0^2/50>0 for 0<eta_0<1. Since Q_0=T^kappa with kappa=(delta-Theta_1)/20>0, sufficiently small epsilon leaves a T-power saving. The claimed normalization and N-power saving additionally require X^2*T=N and T to grow at a fixed positive power of N; these relations are not supplied.

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

Missing context: The definition or preceding bound eq:cIQ1def, fixing the meaning and normalization of I_Q^{(neq,<=)}.; Definitions identifying the two uses of the family F and preserving multiplicities, together with nonvanishing and polynomial size bounds for a and a'.; The scale relations eq:TXNis, sufficient both for every counting modulus to be below N and for converting the final T-saving into N^{-eta}.; An explicit choice eta_0<1/4 before fixing U and H, or another justified estimate replacing the displayed weighted-sum bound.; Confirmation that pairwise coprimality remains imposed until after the q-count is bounded.

### eq:cIQ1def — gpt-6.1-sol

Delivery: completed; local status: locally_supported.

The displayed estimate follows conditionally from the supplied dependency statements. The modulus reduction, frequency count, power U^6, and archimedean integral bound are consistent. This does not establish the dependencies: uniform frequency truncation and the modular estimate’s applicability to both diagonal and off-diagonal pairs remain prerequisites requiring context.

Conditional inputs used: eq:IQbnd1, eq:Mis, eq:cJfbnd, eq:modBndaNeqAp, eq:nmRest, eq:tilQis

- **context**: The modulus simplification is valid: q0=q/(u^2,q), so (q/q0)^2≤u^4. Since q0 divides q, each gcd involving q0 is bounded by its counterpart involving q. The four frequency variables each have O(u) possible values under eq:nmRest. Consequently the remaining u-factor is U sum_{1≤u<U} u^(-4)u^4 O(u^4)=O(U^6). This checks the claimed power without establishing the modular or truncation premises.

  Source: "\\left({q/ q_{0}}\\right)^{2}"

- **map_correction**: The final integral bound needs neither M=XT nor Q<X once the preceding displayed inequality is accepted. For any b>0, splitting at beta0=1/(TX^2) gives integral_{-b}^b min(X^2,1/(|beta|T))^2 d beta≤4X^2/T. Thus eq:Mis is an upstream input to the frequency reduction, rather than a necessary direct input to this final integration. Q<X is compatible with the section’s setup and frequency analysis; no further restriction on Q is needed for this integral estimate.

  Source: "The claim then follows immediately from \\eqref{eq:Mis} and $Q<X$."

- **unverified**: The proof uses eq:nmRest as a uniform effective cutoff throughout |beta|<1/(qM). The packet does not quantify the summed discarded tail or show that it is absorbed by the claimed bound. In particular, the stationary-frequency condition alone does not justify discarding all nonstationary frequencies near beta=0 without also controlling the Fourier scale 1/X. The exact remaining prerequisite is a uniform truncation or weighted-tail estimate whose four-frequency cost is O(u^4). This is a limitation of the unverified input, not an algebraic error in the target deduction.

  Source: "has negligible contribution unless"

- **context**: The source asserts the required identification, but eq:cSdef and the preceding hypotheses of eq:modBndaNeqAp are absent. They are needed to check normalization, coprimality, and uniformity in n,m,n',m'. The quoted modular lemma states no explicit a≠a' restriction, so its label alone does not exclude the diagonal. Conditional on applicability to a=a', that case is valid using (0,q)=q.

  Source: "with the former being exactly equal to $\\cS$ in \\eqref{eq:cSdef}."

- **context**: No external theorem is imported to establish this premise. The cited text’s exact statement, hypotheses, version, and availability by the recorded cutoff 2012-05-24 have not been verified. Later knowledge cannot be excluded from model weights, but none is used as evidence to close this obligation.

  Source: "By (non)stationary phase (see, e.g., \\cite[\\S8.3]{IwaniecKowalski}),"

Missing context: The definition eq:cSdef and full hypotheses preceding eq:modBndaNeqAp, including applicability when a=a'.; A uniform, summable frequency-tail estimate for eq:nmRest over the entire beta interval, together with the cutoff function’s support and smoothness assumptions.; The upstream form-size and discriminant hypotheses supporting eq:cJfbnd, including uniformity of its implied constant over the family.; If the stationary-phase citation is to establish a prerequisite rather than remain conditional: its exact theorem and hypotheses, available_from, date_evidence, date_basis, and version.

### eq:hatRfuBnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The final algebra is correct conditional on the displayed Poisson identity, exponential-sum bound, integral estimate, and uniform control of the discarded Poisson tail. The packet does not supply all hypotheses needed for those applications or quantify the tail. The citation to the family-cardinality bound does not justify the discriminant lower bound. No counterexample to the proposition is established by this bounded review.

Conditional inputs used: eq:Mis, eq:cJfIs, eq:cJfbnd, eq:cRfuIs, eq:cSfbnd1, eq:disc, eq:nmRest, eq:tilQis

- **unverified**: Nonstationary phase supplies decay, not an exact frequency cutoff. The proof must bound the sum of all discarded terms uniformly by O(u/(sqrt(q)|beta|T)). After scaling x,y by X, the relevant frequency spacing is X/(u q_0). The supplied packet does not give sufficient parameter inequalities or a quantitative remainder estimate to verify this truncation, particularly when |beta|TXu q_0 is small.

  Source: "has negligible contribution unless"

- **map_correction**: This cardinality bound, eq:fFTbnd, cannot imply |a| >> T for an individual form. The relevant candidate input is the coordinate cutoff in eq:fFdef, together with the identification a_gamma = <e_1,gamma v_0>. That identification is not explicitly supplied. The discriminant identity itself gives |discr(f)| = 4a^2, conditional on its stated premise.

  Source: "\\#\\fF_{T}\\ll T^{\\gd}."

- **context**: The gradient estimate requires uniform coefficient bounds, for example |A|+|B|+|C| << T on the support x,y in [X,2X]. The packet omits the coefficient definitions and norm/scale relations needed to check this. The discriminant lower bound alone does not imply this upper bound.

  Source: "\\ll\n|\\gb|\\cdot |\\nabla f|\\ll |\\gb|\\cdot TX,"

- **context**: The hypotheses and normalization of eq:cSfbnd1 are omitted. Conditional on a reduced r/q, the supplied reduction does verify gcd(r u_0,q_0)=1, as required for a coprime numerator. Any additional conditions on f and q_0 remain unchecked.

  Source: "With the above conditions,"

- **context**: The displayed Poisson formula and proof cover the even-u lattice. If the proposition includes every positive u, its odd-u application requires checking the lattice with spacings 2u and u, including the resulting integral normalization and complete-sum bound. This adaptation is asserted but not supplied.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

- **context**: This transition checks directly: O(u^2) retained pairs cancel the prefactor u^(-2), giving O(1/(sqrt(q_0)|beta|T)). Since q_0=q/gcd(u^2,q) and sqrt(gcd(u^2,q))<=u, the claimed bound follows. This calculation does not establish the preceding truncation or its error.

  Source: "from which the claim follows, using \\eqref{eq:tilQis}."

Missing context: The complete parameter regime relating X,T,N,U,Q_0,q,u and beta, including whether beta is nonzero; the displayed right-hand side is undefined at beta=0 without an explicit convention.; Definitions identifying a_gamma with the first coordinate of gamma v_0 and establishing uniform bounds for A_gamma,B_gamma,C_gamma.; The definition of cS_f and all hypotheses preceding eq:cSfbnd1.; A quantitative, summable nonstationary-phase remainder compatible with the claimed bound, and the uniform hypotheses behind eq:cJfbnd.; The odd-u calculation if the proposition is intended to include odd u.; The exact applicable statement and hypotheses from the cited 2004 edition of Iwaniec–Kowalski; the external text was not supplied or inspected.

### eq:nmUpToM — gpt-6.1-sol

Delivery: completed; local status: defective.

Conditional on lem:kEllD and the intended finite summation range, the fixed-gcd counting argument and final numerical estimate are sound. However, the displayed enlargement to all divisors w of d1 introduces undefined modular inverses. This is a localized indexing defect, not a counterexample to the claimed bound. No external results are imported; although model knowledge may postdate the 2012-05-24 cutoff, it is not used as historical evidence here.

Conditional inputs used: lem:kEllD

- **error**: The inverse of ell/w modulo d1/w is defined when w is the previously fixed value gcd(ell,d1), but not for every divisor w of d1. Some added indices do not even satisfy w|ell; others give a nonunit. For example, k=1, ell=2 and d=d1=6 satisfy gcd(k,ell,d)=1, but the added term w=1 requires the nonexistent inverse of 2 modulo 6. Thus this displayed multiple sum is not well-defined. The remaining obligation is to state a valid indexing or residue-class convention for the enlarged sum.

  Source: "\\sum_{w\\mid d_{1}}\n\\sum_{m,n<M}\\bo_{\\{m\\equiv0(\\mod w)\\}}\\bo_{\\{ n\\equiv-\\overline{\\frac \\ell w}\\frac mw k(\\mod \\frac{d_{1}}w)\\}}"

- **context**: This step is correct with w fixed as stated. Since w divides both ell and d, the supplied coprimality gives gcd(k,w)=1. Once w|m, division by w leaves ell/w invertible modulo d1/w, so n occupies exactly one residue class. The two resulting counting factors are therefore justified for this fixed gcd.

  Source: "Let $w=(\\ell, d_{1})$; then $mk\\equiv0(w)$ implies $m\\equiv0(w)$ since $(k,\\ell,d)=1$."

- **context**: The final numerical estimate is valid for positive divisors and M>=1. Expanding gives M^2/d1 + M/w + wM/d1 + 1. Here d|d1^2 implies d1>=sqrt(d), while 1<=w<=d1, giving O(M^2/sqrt(d)+M) per pair. There are at most tau(d)^2 pairs. The elementary bound tau(d)^2 <<_epsilon d^epsilon follows directly from prime factorization: for sufficiently large primes, (a+1)^2<=p^(epsilon*a), and the finitely many smaller primes contribute a bounded factor.

  Source: "\\left(\n{M\\over w}\n+1\n\\right)\n\\left(\n{wM\\over d_{1}}\n+1\n\\right)"

- **context**: The estimate requires a finite range such as 0<=m,n<M or 1<=m,n<M, and a positive integer modulus d. These conventions are not explicitly supplied. If m,n range over all integers below M, the count need not be finite; for negative or zero d, the displayed right-hand side is not defined as intended.

  Source: "\\#\\{m,n<M:Am^{2}+2Bmn+Cn^{2}\\equiv0(d)\\}"

- **unverified**: The dependency statement supplies exactly the uniform implication and coprimality needed, under the same coefficient and divisibility hypotheses. Its proof is not included, so this assessment uses it only conditionally. The proposed dependency edge is appropriate; the packet does not establish the dependency itself.

  Source: "As in Lemma \\ref{lem:kEllD}, $A,B,C$ and $d$ determine   $k,\\ell$"

Missing context: Explicit integer domains, positivity of d, and the lower bounds on the m,n summation range.; A valid interpretation or corrected indexing of the enlarged w-sum, ensuring every displayed modular inverse exists.; The proof of lem:kEllD, if an unconditional assessment rather than a conditional local assessment is required.

### lem:spec1 — gpt-6.1-sol

Delivery: completed; local status: defective.

The initial coset reparametrization is correct, but the subsequent kernel evaluation and smoothing ranges use incompatible group products. Consequently, the supplied proof does not establish the stated estimate, even conditional on Lemma spec0. The claimed boundary-strip estimate and uniform smoothing bounds also require additional justification. This is a bounded assessment of the supplied argument, not a verdict that the lemma is false. No external theorem or later development is used to close these obligations.

Conditional inputs used: eq:G1G, lem:spec0, eq:fFdef, eq:ffToInProd, eq:FqIs, eq:fgIs, eq:cNq, eq:reg1Lem, eq:reg2Lem, eq:reg3Lem, eq:NqErr, eq:TT1T2, eq:cCis

- **error**: With the newly defined f, the desired inner sum is Σ_{γ₂′∈tildeΓ(q)} f(γ₀γ₂′). The supplied kernel definition instead makes F_q(γ₁γ₀⁻¹,e)=Σ f(γ₀γ₁⁻¹γ₂′). These are not the same expression. The subsequent ranges likewise use ‖γ₁γ₀⁻¹γ₂′‖ instead of the previously derived ‖γ₁⁻¹γ₀γ₂′‖, and use ⟨e₁,γ₁γ₀⁻¹γ₂′v₀⟩ instead of ⟨e₁,γ₀γ₂′v₀⟩. No stated hypothesis identifies these products.

  Source: "such as replacing \\eqref{eq:cNq} by\n$F_{q}(\\g_{1}\\g_{0}^{-1},e)$."

- **unverified**: The new remaining range includes a strip around the additional boundary ⟨e₁,γ₀γ₂′v₀⟩=T/100. The supplied reg3Lem concerns radial norm shells; it does not supply a uniform count for this linear-functional strip. Boundedness of f controls each summand, not the number of points in that strip. The exact outstanding estimate is a power-saving boundary-strip count, after fixing γ₁, of the strength used in the displayed T₂-error.

  Source: "In the remaining range, \\eqref{eq:reg3Lem} remains unchanged, using $|f|\\le1$."

- **unverified**: The phase estimate requires a perturbation bound of size O(ηTX²); then |β|<K/N and TX²=N give O(ηK). Definitions and bounds for w_{x,y} and the perturbation geometry are absent. Moreover, the inherited smoothing inserts a small element between a potentially large coset representative and the lattice variable. Uniformity in arbitrary γ₀ requires control of conjugation and translated Sobolev norms, not merely the unweighted counting statement of spec0. The restriction 1<K≤T₂^{1/10} does not by itself provide those controls.

  Source: "for a net contribution to the error of $\\ll \\eta K T^{\\gd}$."

- **context**: The asserted equality between the original sum and the double sum requires factorization multiplicity to be retained. It is not an equality for a set of distinct products. The excerpt begins acknowledging multiplicities but truncates the convention; the full family/summation definition is needed.

  Source: "the decomposition $\\g=\\g_{1}\\g_{2}$ in \\eqref{eq:fFdef} need not be unique"

- **context**: Conditional on the displayed error A=ηKT₂^δ+T₂^{δ−ε}η⁻¹⁰, its optimization is correct: η=T₂^{−ε/11}K^{−1/11} gives A≪T₂^{δ−ε/11}K^{10/11}. If this is a uniform per-γ₁ bound and the outer count is O(T₁^δ), summation gives T^{δ−εC/(11(C+1))}K^{10/11}≤T^ΘK with Θ<δ. Thus the final exponent conversion is consistent, but does not establish the preceding error estimate.

  Source: "Optimizing $\\eta$ and renaming $\\gT$ gives the bound $O(T_{2}^{\\gT}K^{10/11})$"

- **map_correction**: The eq:spec1 → lem:spec1 edge is a reference to the target conclusion, not an independent proof input. The kernel and smoothing equations are template references; their applicability to the new weight remains an obligation.

  Source: "giving \\eqref{eq:spec1}."

Missing context: The complete multiplicity convention for the family F and its sums.; Definitions and quantitative bounds for the norm, w_{x,y}, v₀ and δ; the uniform spectral-gap, matrix-coefficient, Sobolev and integration estimates invoked by the template.; A uniform linear-functional boundary-strip counting estimate, including its hypotheses and dependence on γ₁.; Control of smoothing and Sobolev constants independent of q and γ₀, with any T₁-loss explicitly accounted for.; The cited external theorem-bearing text and dated version needed to check applicability by the recorded cutoff 2012-05-24. Model weights can contain later knowledge; none is used here as historical evidence.

### lem:spec2 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The transpose reformulation and spin-map norm comparison are locally checkable. The supplied sketch does not establish the uniform positive mass of the counting region, control the cap-partition errors, or justify the additional positive T^Theta term. Essential definitions and the relevant external arguments are absent. This is a bounded assessment of an incomplete justification, not a counterexample to the lemma.

Conditional inputs used: eq:iota, eq:gDecomp, eq:Vin, thm:Vin, external:BourgainKontorovichSarnak2010

- **context**: The asserted product-sum identity requires the definitions of the family F, its multiplicities, and f_gamma(2x,y)=<w_{x,y},gamma v_0>. These are not supplied. Conditional on that identity, moving gamma_1 to the first vector by transpose gives exactly the displayed region R.

  Source: "Write the left hand side of \\eqref{eq:spec2} as"

- **context**: This comparison is supported by the displayed spin matrix, not merely by quadraticity. Its four corner entries are, up to sign, the squared moduli of the four complex matrix entries. Consequently ||iota_0(g)||_F >= ||g||_F^2/2; the quadratic formulas give the reverse bound up to a constant. Fixed invertible conjugation preserves comparability.

  Source: "\\text{$\\|g\\|^{2}\\asymp T$ gives $\\|\\iota(g)\\|\\asymp T$, }"

- **unverified**: A lower count first requires a positive Patterson–Sullivan-product/Lebesgue mass for an inner approximation to this parameter-dependent region. No calculation shows mass of order T_2^delta/K, either uniformly in gamma_1 or on a sufficiently large subfamily. In particular, compatibility of the norm shell, curvature cutoff, and target n is not established.

  Source: "Then chop $\\tilde R$"

- **unverified**: The supplied theorem counts cap-by-cap angular boxes with a radial cutoff, not arbitrary regions R. The sketch gives no partition resolution, number of boxes, boundary loss, or accumulated counting error. Those estimates must remain uniform for N/2<n<N, x,y asymp X, and 1<K<=T_2^(1/10), and must yield a power saving after summing over gamma_1. The full group hypotheses, their applicability to the spin preimage, and coordinate-section conventions are also omitted.

  Source: "and apply Theorem \\ref{thm:Vin}."

- **unverified**: This is a lower bound with an additional positive term, not an error term. An estimate of the form cT^delta/K-O(T^theta) does not by itself imply it. One must show error absorption throughout the stated K-range and choose a fixed Theta<delta for which T^Theta is dominated by the resulting lower bound, or separately prove the extra contribution.

  Source: "{T^{\\gd}\\over K}\n+\nT^{\\gT}"

- **unverified**: The cited section is not supplied, so its hypotheses and transfer from the cited setting cannot be checked. The Vinogradov2013 citation also lacks a dated version available by the recorded cutoff, 2012-05-24; its year label alone neither establishes nor disproves timely availability. Model knowledge may contain later developments, but none is used here as proof evidence.

  Source: "The same argument as in \\cite[\\S5]{BourgainKontorovichSarnak2010} then leads to \\eqref{eq:spec2}, after renaming $\\gT$; we suppress the details."

- **map_correction**: The eq:spec2 edge points back to the target's own displayed conclusion; it is not an independent premise. Likewise, eq:Vin and thm:Vin are two anchors for the same counting assertion, not separate supporting results.

  Source: "Write the left hand side of \\eqref{eq:spec2} as"

Missing context: Definitions of F, f_gamma, w_{x,y}, e_1, v_0, the norm, and whether F records products with multiplicity.; Relations among N, X, T, T_1 and T_2, and the precise allowed ranges behind x,y asymp X.; The complete hypotheses on Gamma and the spectral gap, their transfer to its spin preimage, and conventions making the angular and M coordinates well defined.; A uniform inner-region mass estimate and quantitative cap/radial partition argument, including all boundary and counting errors.; An explicit exponent calculation establishing the claimed positive T^Theta contribution.; The relevant BKS10 section and a dated pre-cutoff Vinogradov version containing the precise counting result used.

### lm_generation — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The local-to-global argument is valid conditional on lm_local and simultaneous CRT lifting for both factor groups Γ₁ and Γ₂. The supplied dependency lm_local alone does not provide that lifting property. The packet omits Γ₂'s definition and does not justify the asserted factor-group decompositions. There is also a notation error: the simultaneous lifts must belong to quotients modulo q, not the undefined p^m. No counterexample to the target lemma is established.

Conditional inputs used: lm_local

- **unverified**: This is the essential additional prerequisite. For each j=1,2, the proof needs surjectivity of Γ_j/Γ_j(q) → ∏_k Γ_j/Γ_j(p_k^{m_k}), with distinct primes p_k and positive exponents m_k. CRT for the ambient coefficient ring does not automatically imply this for an arbitrary subgroup. The packet asserts, but does not justify, the required subgroup property.

  Source: "Since $\\Ga_1/\\Ga_1(p^m)$ and $\\Ga_2/\\Ga_2(p^m)$ are the direct product\nof local factors"

- **context**: Γ₂ is not defined in the supplied excerpts, and the congruence kernels Γ_j(q) are not explicitly defined. An explicit congruence description of Γ₁ appears later in the proposed scope, but no corresponding description or congruence-compatible identification for Γ₂ is supplied. These definitions are needed to check the simultaneous-lifting assertion.

  Source: "there are $g_1,\\ldots, g_{10^{13}}\\in\\Ga_1/\\Ga_1(q)$ and\n$h_1,\\ldots, h_{10^{13}}\\in\\Ga_2/\\Ga_2(q)$"

- **error**: Here p and m are not defined in the general-modulus proof. The displayed congruences concern all prime-power factors of q, and the subsequent conclusion requires elements modulo q. These quotient labels must therefore be modulo q. This is a localized notation error, not evidence that the lemma itself is false.

  Source: "find elements $g_1,\\ldots, g_{10^{13}}\\in\\Ga_1/\\Ga_1(p^m)$ and\n$h_1,\\ldots, h_{10^{13}}\\in\\Ga_2/\\Ga_2(p^m)$"

- **context**: This final inference checks out conditional on the factor-group CRT property and lm_local. Reduction embeds Γ̄/Γ̄(q) into the product of its prime-power images: an element in every prime-power kernel is congruent to the identity modulo their product q. Simultaneous lifting of each alternating factor gives the reverse containment for A_{10^{13}}. Applying lm_local to each prime-power factor then proves the target. For q a prime power, lm_local directly supplies the conclusion.

  Source: "hence all these containments must be equality."

- **map_correction**: The supplied lm_local → lm_generation edge is appropriate but incomplete as a dependency account. The argument additionally uses CRT-surjectivity for both factor groups. The proof of lm_local appearing in the source slice is not certified by this bounded assessment; lm_local is used only as the supplied unverified premise.

  Source: "Using Lemma \\ref{lm_local}"

Missing context: Definitions of Γ₂ and of Γ_j(r), including their embeddings into Γ̄/Γ̄(r).; A proof or source anchor establishing Γ_j/Γ_j(q) ≅ ∏_k Γ_j/Γ_j(p_k^{m_k}) for j=1,2 and arbitrary prime factorizations of q.; In particular, a congruence description or congruence-compatible identification of Γ₂ sufficient to verify that CRT property.

### lm_generation — claude-opus-5-5

Delivery: provider_failed_or_incomplete; local status: no assessment.

### thm:RNU — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The exceptional-set reduction from the proposed circle-method estimates is conditionally valid, with a harmless epsilon-bookkeeping correction. It proves the representation lower bound outside a power-saving exceptional set, provided the singular series already has the stated positivity and lower-bound properties. Those properties are not independently established in this packet. The proof of Theorem Main appearing between the statements is downstream, not a proof of this target. No external results are imported; model knowledge alone is not used to certify historical availability under the recorded 2012-05-24 cutoff.

Conditional inputs used: thm:CircMeth, eq:cMNUbnd, eq:cEN2bnd

- **error**: For the same fixed epsilon used in the preceding pointwise inequality, squaring requires N^{-2 epsilon}, not N^{-epsilon}, in the denominator. This does not invalidate the power-saving conclusion because epsilon is arbitrary. New local repair, separate from the displayed calculation: write eta_0 for the exponent in CircMeth and assume the stated singular-series bound with epsilon=eta_0/4. On Z, the decomposition and R<M/2 imply |E|>M/2, hence |E| is bounded below by a positive constant times N^{-eta_0/4}T^{delta-1}. Summing squares gives |Z|=O(N^{1-eta_0/2}). Adding the O(N^{1-eta_0}) major-term exceptions preserves a power saving. Outside their union, R>=M/2 implies the target representation lower bound.

  Source: "{|\\cE_{N}^{U}(n)|^{2}\n\\over \nN^{-\\vep}T^{2(\\gd-1)}}"

- **unverified**: The reduction uses the singular-series lower bound on admissible integers, but this sentence does not independently demonstrate its existence, nonnegativity, vanishing restriction, or uniform lower bounds. If CircMeth is intended to include all these properties as part of its proposed premise, the reduction is supported conditional on that interpretation. Otherwise, the singular-series portion of the target remains an additional obligation; the L2 argument cannot establish it.

  Source: "The singular series $\\fS(n)$ is the same as in Theorem \\ref{thm:RNU}."

- **context**: The supplied major-term estimate and singular-series properties are only stated for N/2<n<N. The restriction must therefore remain within that interval. This suffices for the target as stated; the paragraph does not justify a claim for all admissible n<N.

  Source: "We restrict our attention to the set of admissible $n<N$ so that \\eqref{eq:cMNUbnd} holds"

- **map_correction**: eq:RNUbnd is the target's own representation conclusion, not an independent proof input. Its supplied edge to thm:RNU should be understood as a statement/reference edge, not evidentiary support. The decomposition eq:RNcMcE, already contained in CircMeth, is an essential actual input.

  Source: "\\be\\label{eq:RNUbnd}\n\\cR_{N}^{U}(n)\\gg \\fS(n) T^{\\gd-1},\n\\ee"

Missing context: An independent definition and proof anchor for the singular series, or an explicit statement that the proposed CircMeth premise includes all singular-series properties asserted in RNU.; In particular, the uniform bound S(n) >= c_epsilon N^{-epsilon} on admissible N/2<n<N, together with nonnegativity and the stated restriction on vanishing, remains unverified by this packet. No inspection of the proofs of the supplied dependency statements has been performed.

## Wave 2

eq:cIQ11bnd, eq:cIQ2bnd, eq:eqeq, thm:IQ0, thm:Main, thm:cMNis

### eq:cIQ11bnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The divisor-sum argument supports the claimed intermediate estimate conditionally on the supplied lemmas and missing family/range assumptions. There is a harmless strict-inequality error in the lcm comparison. The final N-power saving additionally requires the omitted relation among T, X, and N. No external results are imported; later-trained model knowledge is not treated as evidence of availability by the recorded cutoff, 2012-05-24.

Conditional inputs used: eq:His, eq:cIQ1def, eq:fuIs, eq:spec3

- **error**: The strict inequality is false when n=m. Elementary correction (new local repair): for positive integers, [n,m]=nm/(n,m) and (n,m)≤sqrt(nm), so [n,m]≥sqrt(nm). This non-strict inequality suffices: writing L=[d,d'], the q-sum is O(1/L), and sqrt(dd')/L≤1. Thus the typo does not invalidate the estimate.

  Source: "where we used $[n,m]>(nm)^{1/2}$."

- **context**: The section supplies Q0≤Q<X, satisfying the displayed lemma's Q<X hypothesis. However, the lemma as stated bounds the entire off-diagonal contribution, not explicitly its gcd-restricted subpieces. The first line of this proof needs its pairwise/localized version. The preceding expansion suggests such a version may be available, but the lemma's proof and precise definition of the restricted contribution are omitted.

  Source: "Assume $Q<X$. For $\\square\\in\\{=,\\neq\\}$, we have"

- **context**: The divisor manipulations require nonzero integer coefficients a,a' of polynomially bounded size in T. Under these conditions, replacing exact gcd conditions by divisibility only enlarges the nonnegative majorant; the two divisor counts contribute T^ε. The later sum over h|a contributes another divisor factor, which can be absorbed by rescaling ε. The required coefficient bounds are not supplied.

  Source: "Writing $(a,a')=h>H$,"

- **unverified**: Conditionally on eq:spec3, the application gives at most T^δ h^{-η0}, hence T^δ H^{-η0}, provided every relevant modulus satisfies 1≤h<N. It also requires the forms indexed here to correspond to the gamma-family in eq:spec3 with the same counting multiplicities and coefficient a'=⟨e1,gamma v0⟩. With that identification, eq:spec3 at q=1 also supplies the outer family bound O(T^δ). These prerequisites and the lemma's specified family parameters are not fully documented in the packet.

  Source: "Apply \\eqref{eq:spec3} to the innermost sum, getting"

- **context**: The parameter algebra checks: U^6 H^{-η0}=U^{-4}=Q0^{-η0²/25}=T^{-c}, where c=(δ−Θ1)η0²/500>0 using the supplied definition of Q0. Thus the proved bound is X² T^{2δ−1+ε−c}. Its ratio to N T^{2(δ−1)} is (X²T/N)T^{ε−c}. To obtain N^{-η}, one still needs the omitted scale relation. For example, if the source states N=TX² and T=N^τ for fixed τ>0, any ε<c yields η=τ(c−ε)>0. Those scale assumptions are not established by this packet.

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

- **map_correction**: The listed dependencies omit the definition making Q0 a fixed positive power of T. They also omit the T,X,N normalization needed for the proposition's stated scale. These are additional proof inputs, not consequences of eq:His and eq:fuIs alone.

  Source: "\\be\\label{eq:Q0is}\nQ_{0}= T ^{(\\gd-\\gT_{1})/20},"

Missing context: Definitions of a, the family of forms, and its multiplicity-preserving relationship to the gamma-family in eq:spec3; verification that the family parameters meet that lemma's hypotheses.; Bounds ensuring a,a' are nonzero integers of polynomial size in T and every divisor modulus h used in eq:spec3 is less than N.; The definition of the gcd-restricted contribution and the pairwise/localized estimate underlying eq:cIQ1def.; The statement of eq:TXNis, including a fixed positive-power relationship between T and N sufficient to convert the T-saving into N^{-η}.

### eq:cIQ2bnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The divisor-sum manipulation and final power saving check conditionally on the supplied premises. The remaining obligation is to verify from the omitted ensemble definitions that the form sums are controlled, with their actual multiplicities, by the gamma-count in eq:spec3, and that 0<|a|≪T uniformly. No local arithmetic error is identified. No external result is imported; the recorded cutoff is 2012-05-24, and pretrained knowledge is not intrinsically date-filtered.

Conditional inputs used: eq:TXNis, eq:cIQ1def, eq:fuIs, eq:spec3

- **context**: For a'=a, eq:cIQ1def gives this factor exactly, since (0,q)=q. For nonzero a, use (a²,q)≤Σ_{d|a², d|q}d. Each d≪Q divides O(Q/d) integers q≍Q, so the q-sum is O(τ(a²)). Prime factorization gives τ(a²)≪ε T^ε when |a|≪T, after adjusting ε. Thus the displayed divisor step is valid under the announced size condition; a=0 must be excluded.

  Source: "{(a^{2},q)\\over q}"

- **context**: Equality implies this congruence, so enlarging the nonnegative counting sum is valid. In the section range Q₀≤Q<X=N^(99/200)<N, the modulus floor(Q₀) lies in [1,N) for large N and is comparable to Q₀. Equation spec3 then supplies the inner bound T^δ/Q₀^η₀, provided its gamma-family controls the form-family with the required multiplicities. The outer bound #F≪T^δ follows from spec3 itself at q=1; no additional counting theorem is needed. The formal ensemble and form definitions needed to check that transfer are absent.

  Source: "Recalling that $a=a_{\\g}=\\<e_{1},\\g v_{0}\\>$, replace the condition $a'=a$ with $a'\\equiv a(\\mod \\lfloor Q_{0}\\rfloor)$, and apply \\eqref{eq:spec3}:"

- **context**: This announces precisely the size property needed for the divisor estimate. The excerpt of the spec3 proof also mentions the restriction a>T/100, supporting nonvanishing. However, eq:fFdef, the norm definition, and the formal gamma-to-form construction are not supplied, so uniformity of 0<|a|≪T over the actual indexed sums cannot be independently verified here.

  Source: "We further need the technical condition that in the $T$-ball, the value of $a_{\\g}=\\<e_{1},\\g\\, v_{0}\\>$ (see \\eqref{eq:vgIs}) is of order $T$."

- **map_correction**: Equation Q0is is an essential additional input, although it appears inside the excerpt labeled reference:eq:fuIs rather than among the dependency IDs. Put α=(δ−Θ₁)/20>0 and κ=η₀−6η₀²/100>0, using 0<η₀<1. The displayed estimate becomes N T^{2(δ−1)}T^{ε−ακ}. Taking ε=ακ/2 and using T=N^(1/100) gives the claimed bound with η=ακ/200>0. The four existing dependency edges are relevant; this is an omitted parameter-definition edge, not a proof defect.

  Source: "Q_{0}= T ^{(\\gd-\\gT_{1})/20},"

Missing context: The formal definition eq:fFdef and the gamma-to-form construction, including multiplicities, sufficient to show that both total form counts and fixed-a congruence counts are bounded by the corresponding counts in eq:spec3.; The norm and coefficient definitions, including eq:vgIs, establishing uniformly that a is a nonzero integer and |a|≪T for every indexed form.

### eq:eqeq — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The counting strategy conditionally supports the claimed bound, but the packet omits the family definitions and a uniform representation estimate needed to justify its applications. There is also a factor-of-four mismatch in the congruence-lemma hypothesis, repairable by an elementary reduction stated below. The supplied dependencies remain unverified premises. No external theorem is imported; possible later knowledge in model training is not treated as historical evidence under the 2012-05-24 cutoff.

Conditional inputs used: eq:cKzBnd, eq:fincK, eq:nmUpToM

- **context**: The packet does not define the family F, its coefficient bounds, its definiteness or primitivity conditions, or the relation of a to the discriminant. These are necessary to check both class-counting hypotheses and the congruence-counting hypothesis. A definition of the finite integer box denoted by m,n<M is also needed.

  Source: "For large $M$ and  $\\ff=f-a\\in\\fF$ fixed,"

- **unverified**: This uniform representation estimate is a separate proof input, not supplied by any of the three dependency statements. Its constant must be controlled uniformly over the varying forms f' and the parameter T. A bound expressed in terms of the represented integer alone does not yield the displayed M^epsilon estimate without further argument. An adequate (TM)^epsilon bound would also suffice after exponent rescaling, but is not established here.

  Source: "it is elementary that there are  $\\ll_{\\vep} M^{\\vep}$ values of $m',n'$ with $f(m,-n)=f'(m',-n')$."

- **map_correction**: eq:cKzBnd uses 'determinant', whereas eq:fincK uses discriminant -4a^2. Under standard conventions these are different invariants. Its edge to this proof is conditional on clarification that the class-counting lemma concerns the same forms and equivalence relation as eq:fincK. This may be terminology rather than a substantive defect.

  Source: "of determinant $-4a^{2}"

- **map_correction**: Under the usual convention f=Ax^2+2Bxy+Cy^2 with discriminant -4a^2, one has AC-B^2=a^2. The proof sums over d dividing 4a^2, so the stated lemma does not directly cover every summand. New local repair, conditional on primitivity: put d0=gcd(d,a^2). Then d/d0<=4, the solutions modulo d form a subset of those modulo d0, and the supplied lemma gives N(d)<=N(d0)<<d^eta(2M^2/sqrt(d)+M). Thus the required extension follows with an absolute constant. Replacing B by -B preserves both hypotheses.

  Source: "Given large $M$, $(A,B,C)=1$ and $d\\mid AC-B^{2}$,"

- **unverified**: eq:cKzBnd contributes a factor z^eta, where z=f(m,-n). Absorbing this into (TM)^epsilon requires a uniform polynomial upper bound for z in T and M, or another argument. No coefficient-size bound implying this is supplied. The class-counting statement also requires positive, sufficiently large z; positivity and treatment of any exceptional small values must be checked.

  Source: "(TM)^{\\vep}\n\\sum_{m,n<M}\n(f(m,-n),4a^{2})^{1/2}"

- **context**: If the box includes (0,0), then z=0 occurs and eq:cKzBnd, stated for a large integer z, is inapplicable. For positive-definite forms, this tuple can contribute one solution for each f' with a'=a, requiring a separate family-size estimate. If the intended domain excludes the origin, that convention should be supplied.

  Source: "\\sum_{m,n<M}"

- **context**: The final arithmetic summation is valid conditionally on a being a nonzero integer with |a|<<T. Indeed, the preceding expression is bounded by tau(4a^2)(M^2+2|a|M), apart from the small divisor powers supplied by eq:nmUpToM. Elementary divisor estimates and choosing smaller intermediate epsilon values absorb these factors into (TM)^epsilon. This does not resolve the earlier missing hypotheses.

  Source: "from which the claim follows since $a\\ll T$."

Missing context: Definition of F, the coefficient convention for f, the equivalence relation, definiteness and primitivity, and the precise determinant/discriminant identity.; Uniform coefficient-size bounds implying |f(m,-n)| is polynomially bounded in TM, together with the parameter range and justification of |a|<<T.; A proof or an admissibly dated source for the uniform representation estimate, with its exact hypotheses and constant dependence.; The integer-box convention and, if necessary, a separate estimate for zero or other values outside the stated range of eq:cKzBnd.

### thm:IQ0 — gpt-6.1-sol

Delivery: completed; local status: needs_context.

Conditional on the supplied exponential-sum estimate applying uniformly and on the missing counting and scale inputs, the argument gives both claimed bounds. The elementary integrations are sound, although one displayed coarse-bound transition needs an unstated parameter comparison. No counterexample or unconditional local defect is established. The review uses no imported external theorem; model knowledge may include later developments, but none is used as evidence beyond the recorded 2012-05-24 cutoff.

Conditional inputs used: eq:IQ0, eq:IQ0K0, eq:Q0is, eq:RNRf, eq:fuIs, eq:hatRfuBnd

- **map_correction**: The triangle inequality and sum over u are correct, but the second inequality additionally requires the total number of terms in the family, counted with its intended multiplicities, to be O(T^δ). Indeed, summing u<U contributes O(U²), leaving #F/T. This counting input and the definition of F are absent from the packet and dependency list. This is an omitted map input, not evidence that the counting bound is false.

  Source: "\\sum_{\\d< U}\n\\sum_{\\ff\\in\\fF}\nu\n(\\sqrt{q}|\\gb|T)^{-1}\n\\ll\nU^{2}\nT^{\\gd-1}\n(\\sqrt{q}|\\gb|)^{-1}"

- **context**: The supplied inequalities δ>Θ₁>1 and 0<η₀<1 do imply Q₀U⁴/K₀ = T^{-c}, where c=(δ-Θ₁)(1-η₀²/25)/20>0. They do not alone imply an N-power saving. One also needs a fixed positive-power lower bound T≥N^τ, or an equivalent scale relation. Under that condition, η=τc is admissible. No relation between T and N is supplied.

  Source: "Q_{0}= T ^{(\\gd-\\gT_{1})/20},\n\\qquad\nK_{0}=Q_{0}^{2}."

- **context**: The printed passage from this coarse bound to the final bound requires Q₀M≪N/K₀, equivalently Q₀K₀M≪N; the scale of M is missing. This is not an intrinsic obstruction to the integral estimate. New local repair, separate from the displayed justification: interpreting an empty integration region as zero, the symmetric integral of |β|^{-2} over K₀/N<|β|<1/(qM) equals 2 max(N/K₀−qM,0), hence is at most 2N/K₀. Since the number of reduced residues is φ(q)≤q, summing φ(q)/q over q<Q₀ gives O(Q₀), directly yielding the claimed final bound without the extra M term.

  Source: "\\left({\nN\\over K_{0}}+{Q_{0}M}\\right)"

- **unverified**: The theorem sums over all u<U. The supplied bound eq:hatRfuBnd is accepted only as a proposed premise, but its phrase 'With the above notation' inherits setup not fully present here. Its applicability must cover odd as well as even u, every family member, and both integration ranges, uniformly in the varying parameters. In particular, if its β-range stops at 1/(qM), using it throughout |β|<K₀/N requires a parameter comparison. The packet does not establish those inherited scope conditions.

  Source: "From now on, we focus exclusively on the case $u$ is even, the other case being handled similarly."

Missing context: The definition of the family F, including multiplicities, and a source statement giving #F≪T^δ.; The relation between T and N ensuring T≥N^τ for some fixed τ>0, with δ−Θ₁ fixed and positive.; The full inherited hypotheses and uniformity range of eq:hatRfuBnd, including its coverage of odd u and both small-denominator integration regions.; The definition and scale of M, including Q₀K₀M≪N if retaining the printed coarse-bound domination or if needed for the exponential-sum estimate's domain.

### thm:Main — gpt-6.1-sol

Delivery: completed; local status: defective.

The conditional exceptional-set argument has the correct Möbius-tail estimate and exponent arithmetic. However, the proof applies Theorem thm:RNU to all admissible n<N although its conclusion is stated only for a restricted interval. The resulting complement estimate is unsupported as written. Effective computability of the final exponent also requires quantitative inputs not supplied here. These are local assessments of the displayed reduction, not a verdict on the full theorem.

Conditional inputs used: thm:RNU, eq:RNUbnd, eq:fFTbnd, eq:Uis, eq:TXNis, eq:binQuad, eq:ffToInProd, eq:fFdef

- **error**: Theorem thm:RNU controls only \foh N<n<N, whereas Z and W are defined over admissible n<N. Its exceptional-set bound therefore does not establish this displayed estimate outside the stated interval. Complements must also be understood relative to the admissible domain. A separate scale-covering argument is required for the up-to-N conclusion; none is supplied in this proof.

  Source: "Note also from Theorem \\ref{thm:RNU} that $|Z\\cap W^{c}|\n\\le |W^{c}|\\ll N^{1-\\eta}$."

- **context**: The Möbius-tail bound is elementary and valid conditional on eq:fFTbnd counting the ensemble with the same multiplicities as the representation sums. The smoothing support gives X≤2x,y≤2X, hence u≤2X. For each u, the two divisibility conditions admit O(X/u) choices each, including the factor gcd(2,u)≤2. Summing X²/u² gives O(X²/U). Positivity and boundedness of the fixed smooth weight justify removing it in this upper bound.

  Source: "T^{\\gd}            \n{X^{2}\\over U}"

- **context**: On the interval actually covered by thm:RNU, the algebra is correct: the tail estimate and singular-series lower bound give O(N^{1−η_R}+N^{1+ε−u}) exceptions, where U=N^u. Taking ε=u/2 gives exponent saving min(η_R,u/2)>0. No positivity of the truncated representation function outside the good set is needed. The implication from a nonzero untruncated representation to an actual curvature is supported conditionally by eq:binQuad.

  Source: "which\n is a power savings since $\\vep>0$ is arbitrary."

- **unverified**: The supplied statement of thm:RNU asserts existence of η_R>0, not its effective computability. The parameter u likewise depends on spectral-gap and counting exponents. Effectivity of these positive exponents must be supplied to justify the stronger target qualification. Ineffective constants in the N^{−ε} singular-series lower bound would not, by themselves, prevent computing the exponent.

  Source: "$O(N^{1-\\eta})$, where $\\eta>0$ is effectively computable."

- **unverified**: No external theorem is imported in this assessment; eq:fFTbnd and thm:RNU remain proposed premises. For the cited Vinogradov input, available_from is unknown, date_evidence is only the supplied citation label, date_basis is unverified citation metadata, and version is unknown. A version containing the needed result available by 2012-05-24 is required before historical admissibility can be confirmed. Model knowledge is not intrinsically date-filtered; no later knowledge is used here to close this obligation.

  Source: "The following theorem follows easily              \nfrom \\cite[Thm 2.2]{Vinogradov2013}."

- **map_correction**: The historical density bounds, figures, and methodological inspiration citations are not direct premises of the displayed reduction. Its operative inputs are the representation definitions, curvature implication, ensemble count, parameter identities, and thm:RNU. The edge with source_from rmk:locA should identify that remark rather than silently substituting lem:GGq.

  Source: "The history of this problem is as follows."

Missing context: The definition of the macro \foh and the omitted introductory assumptions on the fixed gasket, including the applicable integrality/primitivity conditions and formal meaning of admissibility.; A supplied argument passing from the restricted interval in thm:RNU to all positive admissible integers up to N, with uniform estimates at the required scales.; Effective quantitative versions of the exceptional exponent in thm:RNU and the spectral/counting parameters determining u.; Confirmation that eq:fFTbnd bounds the same weighted or multiplicity-counted ensemble used in the representation sums.; Dated, version-specific evidence for any external result actually used upstream, especially the cited Vinogradov theorem, before the recorded 2012-05-24 cutoff.

### thm:Main — gemini-4-argon

Delivery: invalid_assessment; local status: no assessment.

### thm:cMNis — gpt-6.1-sol

Delivery: completed; local status: needs_context.

The archimedean estimate and final power saving are conditionally consistent, but the supplied proof does not quantify the passage from the truncated modular sum to the infinite singular series. Transitivity, local densities, parameter-range compatibility, and primitive-pair counting also require omitted context. The all-n formulation additionally requires a sign argument when the singular series vanishes. This is a bounded assessment, not a verdict on the theorem.

Conditional inputs used: eq:Fuc, eq:Q0is, eq:TXNis, eq:cMNUn, eq:fMdecomp, eq:hatFunc, lem:spec2

- **unverified**: The decomposition contains the finite sum S_{Q0}, not the Euler product S. Convergence and bounds for S alone do not justify replacing S_{Q0}. A uniform estimate implying S_{Q0}(n) >= c S(n) for admissible N/2<n<N is still required. No truncation-error estimate is supplied.

  Source: "extend the sum on $q$ to all natural numbers,  and use multiplicativity to write the sum\nas an Euler product."

- **context**: This requires the relevant dual-orbit statement for w_{x,y} modulo every q, with its coprimality hypotheses. The full Möbius sum restricts to gcd(2x,y)=1, but that restriction is not stated here. Equation Fuc covers only moduli coprime to 6; transitivity and local factors at 2 and 3 require additional justification. The switch from tilde-Gamma(q) to Gamma_0(q) in the Euler product also needs their definitions or an explanation of equivalent averaging.

  Source: "use the transitivity of the $\\g_{0}$ sum to replace $\\<w_{x,y},\\g_{0} v_{0}\\>$ by $\\<e_{4},\\g_{0} v_{0}\\>$"

- **context**: The window requires K=2K0. The hypothesis N/2<n<N matches, but x,y asymptotic to X depends on the omitted cutoff definition. Also 2K0<=T2^(1/10) must be checked. Writing a=delta-Theta1 and T2=T^{C/(1+C)}, this requires 2T^{a/10}<=T^{C/[10(1+C)]}; a<C/(1+C) suffices asymptotically. The supplied data do not establish this inequality.

  Source: "using Lemma \\ref{lem:spec2}."

- **error**: The Fourier transform vanishes at every nonzero integer, so global strict positivity is false. Nonnegativity is sufficient for the displayed lower bound. The other inequality is correct: on |y|<1/2 the squared sinc is greater than 4/pi^2>2/5.

  Source: "specifically that $\\hat\\ft>0$ and $\\hat\\ft(y)>2/5$ for $|y|<1/2$"

- **unverified**: The lower bound needs an admissibility qualification whenever S can vanish. More importantly, the target includes non-admissible n: if S(n)=0, it asserts M_N(n)>=0. An approximation with an unsigned O-error does not establish that sign. Neither the supplied major-arc definition nor the final error estimate supplies this missing argument.

  Source: "N^{-\\vep}\\ll_{\\vep} \\fS(n)\\ll_{\\vep} N^{\\vep},"

- **context**: Conditional on nonnegative cutoff weights, weighted primitive-pair mass comparable to X^2, and S_{Q0}>=cS, the scaling works. There are O(X^2) contributing pairs, so the decomposition error is O(T^{Theta1-1}Q0^8)=O(T^{delta-1-3a/5}), while the main scale is S(n)T^{delta-1}. Since T=N^{1/100}, the proposed admissible lower bound S(n)>>N^{-epsilon} absorbs this error for epsilon<3a/500. The required support, positivity, and primitive-pair mass are not supplied.

  Source: "Putting everything into  \\eqref{eq:fMdecomp} and then into \\eqref{eq:cMNUn} gives \\eqref{eq:cMNbnd}"

- **map_correction**: eq:cMNbnd is the target conclusion, not an independent proof input. Likewise, thm:RNU specifies the desired singular-series properties; its representation lower bound must not be used to prove this intermediate theorem.

  Source: "gives \\eqref{eq:cMNbnd}"

Missing context: Definitions of w_{x,y}, Gamma_0(q), the relevant orbit action, and Upsilon, including support and positivity.; Uniform local-factor computations, convergence, positivity on admissible integers, and a quantitative singular-series truncation estimate, including primes 2 and 3.; A compatible bound relating delta-Theta1 and C, weighted primitive-pair counting, and a sign argument for the claimed non-admissible cases.; Dated exact external statements and versions supporting the classical singular-series argument. The recorded cutoff is 2012-05-24. No external theorem was imported here; model knowledge alone cannot certify historical availability.

### thm:cMNis — claude-opus-5-5

Delivery: provider_failed_or_incomplete; local status: no assessment.

## Wave 3

eq:cI41bnd

### eq:cI41bnd — gpt-6.1-sol

Delivery: completed; local status: needs_context.

Conditional on the supplied dependency statements and omitted notation and scale bounds, the displayed summation argument is algebraically consistent and yields I_Q^(=,=) ≪_ε N^ε U^4 X^2 T^δ. The packet does not supply enough information to verify the initial restriction, the gcd and family-counting estimates, or the final power saving. The eq:gls dependency is incorrectly mapped from a reference to eq:dim. No external theorem is imported; later knowledge potentially present in model weights is not used to fill these gaps.

Conditional inputs used: eq:cIQ3def, eq:eqeq, eq:modBndaNeqAp

- **context**: The packet defines the split by a=a' but not the second equality in this notation. The first displayed estimate additionally restricts to ff(m,-n)=ff'(m',-n'); its validity requires the missing definition of this contribution. The section supplies Q≥X, so the explicit hypothesis of eq:cIQ3def is satisfied within the section's range.

  Source: "\\cI_{Q}^{(=,=)}"

- **context**: At a=a', the stated modular estimate gives (q/q0)^2 (a^2,q0)/q, since (0,q)=q. The displayed bound follows if q0 divides q and (q/q0)^2≤u^4. Neither the definition of q0 nor these consequences is supplied. The omitted 'above notation' must also be checked to ensure the modular lemma allows a=a'.

  Source: "u^{4}\n{(a^{2},q)\\over q^{5/4}}q^{1/4}"

- **unverified**: The divisor step is valid conditionally: (a^2,q)≤Σ_{d|a^2,d|q}d, and for d≪Q there are O(Q/d) multiples in q∼Q. Thus the weighted q-sum is O(Q τ(a^2)). Absorbing this into Q N^ε requires nonzero a of polynomially bounded size. The next line also requires #F≪T^δ, up to an absorbable loss. These prerequisites are absent.

  Source: "\\sum_{\\tilde q_{1}\\mid a^{2}\\atop\\tilde q_{1}\\ll Q}"

- **context**: The application of eq:eqeq correctly counts all four integer variables for each fixed ff; no additional factor for n,m is needed. Its hypotheses still require the frequency range to be covered by a sufficiently large bound K≍UQ/X, and (TK)^ε to be absorbable into N^ε. Expanding the resulting line gives N^ε[U^4 XQ T^(δ−1)+U^3 X^2 T^δ]. For Q<XT and U≥1, this is bounded by N^ε U^4 X^2 T^δ, as displayed.

  Source: "\\left( {UQ\\over X}\\right)^{2}\n+\nT\n{UQ\\over X}"

- **unverified**: The final factorization is exact, but the claimed saving needs a relation such as X^2T≍N and a quantitative bound U^4 T^(1−δ)≤N^(−c) for some c>0, followed by ε<c. Merely knowing δ>1 would not establish an N-power saving without growth restrictions on T and U. These parameter statements are not supplied.

  Source: "T^{1-\\gd}\nU^{4}\nN^{\\vep}"

- **map_correction**: The source references eq:dim, not eq:gls. The supplied spectral theorem neither asserts δ>1 unconditionally nor supplies the required parameter scales. The eq:gls edge should therefore not be treated as a proof input here; the missing eq:dim statement and relevant scale definitions are the appropriate candidates. This is a mapping/context limitation, not itself a demonstrated proof defect.

  Source: "From \\eqref{eq:dim}, this is a power savings."

Missing context: Definition of I_Q^(=,=), including its collision restriction and its relation to the bound eq:cIQ3def.; Definition eq:tilQis and surrounding hypotheses for eq:modBndaNeqAp, establishing q0|q, (q/q0)^2≤u^4, and applicability when a=a'.; Bounds for the family F and its coefficients, including #F≪T^δ, nonzero a, and polynomial size control needed for divisor losses.; Parameter definitions relating N, X, T, U and the global M, including U≥1 and a sufficiently large frequency cutoff for eq:eqeq.; The statement eq:dim and quantitative parameter choices implying U^4 T^(1−δ)≤N^(−c) for some c>0.