# Reading roadmap: manuscript-expanded.tex

The manuscript encodes circle curvatures in an Apollonian-group orbit and constructs a weighted representation function from shifted binary quadratic forms. It reduces a power-saving exceptional-set bound to a major-arc lower bound and a minor-arc mean-square estimate. Uniform spectral gap and effective bisector counting supply the major-arc equidistribution; explicit exponential-sum estimates handle three denominator ranges on the minor arcs. A separate appendix derives the needed uniform spectral gap from arithmetic subgroups. The final comparison of represented mass and exceptional-set size gives density one among admissible integers.

Source SHA-256: `9939002e09d4f1726684edebc860d0b6f9dce839e4ea6761c41c4660ef932f64`. Indexed 154,622 characters.

Edges point from prerequisite to consumer. Solid proof edges are attributed inferences, not formal certificates; references remain candidates.

## Arithmetic encoding and congruences

Descartes quadruples, group parametrization and admissible residue classes.

Claims: lem:GGq

## Reduction to circle-method estimates

Representation counts, truncation and exceptional-set comparison.

Claims: thm:Main, thm:RNU, thm:CircMeth

## Major arcs

Uniform spectral counting, singular series and truncation transfer.

Claims: thm:cMNis, thm:cMNtoMNU

## Minor arcs

Control three denominator ranges and combine mean-square estimates.

Claims: thm:IQ0, thm:IQX, thm:IQM

## Spectral-gap appendix

A bounded-generation and subgroup-gap argument for the Apollonian congruence family.

Claims: th_sg

## Internal claim index

### Theorem [thm:Main] — `thm:Main`

Source lines 572–577.

Almost every admissible number is the curvature of a circle in $\sG$. Quantitatively, the number of exceptions up to $N$ is bounded by $O(N^{1-\eta})$, where $\eta>0$ is effectively computable.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: \ We first show that the difference between $\cR_{N}$ and $\cR_{N}^{U}$ is small in $\ell^{1}$. Using \eqref{eq:fFTbnd} we have \beann \sum_{n<N}|\cR_{N}(n)-\cR_{N}^{U}(n)| &=& \sum_{n<N} \left| \sum_{\ff\in\fF}\sum_{x,y\in\Z} \gU\left(\frac {2x}X\right) \gU\left(\frac yX\right) \bo_{\{n=\ff(2x,y)\}} \sum_{u\mid(2x,y)\atop u\ge U}\mu(u) \right| \\ &\ll& \sum_{\ff\in\fF} \sum_{u \ge U} \sum_{y\ll X\atop y\equiv0(\mod u)} \sum_{x\ll X\atop 2x\equiv0(\mod u)} 1 \\ &\ll & T^{\gd} {X^{2}\over U} , \eeann for any $\vep>0$. Recall from \eqref{eq:Uis} that $U$ is a fixed power of $N$, so the above saves a power from the total mass \eqref{eq:totMass}. Now let $Z$ be the ``exceptional'' set of admissi


Candidate references: `thm:RNU` (candidate_proof_dependency); `eq:fFTbnd` (candidate_proof_dependency); `eq:Uis` (candidate_proof_dependency); `eq:totMass` (candidate_proof_dependency); `eq:RNUbnd` (candidate_proof_dependency); `eq:TXNis` (candidate_proof_dependency).

### Lemma [eq:vgIs] — `eq:vgIs`

Source lines 1117–1171.

\cite{SarnakToLagarias}

Let $x,y\in\Z$ with $(2x,y)=1$, and take any element $\g\in\G$ with corresponding quadruple \be v_{\g}=(a_{\g},b_{\g},c_{\g},d_{\g})^{t}=\g\cdot v_{0}\in\sO. \ee Then the number \be \<e_{4},\xi_{x,y}\cdot \g\cdot v_{0}\> = \<w_{x,y},\g\cdot v_{0}\> = 4A_{\g}x^{2} +4B_{\g}xy +C_{\g}y^{2} -a _{\g} \ee is the curvature of some circle in $\sG$, where we have defined \bea A_{\g} &:=& a_{\g}+b_{\g}, \\ \nonumber B_{\g} &:=& {a _{\g} + b _{\g} - c _{\g} + d _{\g}\over 2}, \\ \nonumber C_{\g} &:=& a_{\g} + d_{\g} . \eea Note from \eqref{eq:Fv} that $B_

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `eq:Fv` (internal_reference); `external:SarnakToLagarias` (external_reference).

### Lemma [lem:line:1307] — `lem:line:1307`

Source lines 1307–1318.

\cite{GrahamLagariasMallowsWilksYanI, FuchsThesis}

The group $\tilde\G$ is generated by $$ \pm \mattwo1{4i}{}1,\quad \pm \mattwo{-2}ii{},\quad \pm \mattwo{2+2i}{4+3i}{-i}{-2i}. $$

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `external:GrahamLagariasMallowsWilksYanI` (external_reference); `external:FuchsThesis` (external_reference).

### Lemma [lem:GGq] — `lem:GGq`

Source lines 1324–1344.

\cite{FuchsThesis}

\ (1) The quotient groups $\G/\G(q)$ are multiplicative, that is, if $q$ factors as $$ q=p_{1}^{\ell_{1}}\cdots p_{r}^{\ell_{r}}, $$ then $$ \G/\G(q)\cong \G/\G(p_{1}^{\ell_{1}})\times\cdots\times \G/\G(p_{r}^{\ell_{r}}). $$ (2) If $(q,6)=1$ then \be \G/\G(q)\cong\SO_{F}(\Z/q\Z). \ee (3) If $q=2^{\ell}$, $\ell\ge3$, then $\G/\G(q)$ is the full preimage of $\G/\G(8)$ under the projection $\SO_{F}(\Z/q\Z)\to \SO_{F}(\Z/8\Z)$. That is, the powers of $2$ stabilize at $8$. Similarly, the powers of $3$ stabilize at $3$, meaning that for $q=3^{\ell}$,

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `external:FuchsThesis` (external_reference).

### Theorem [thm:RNU] — `thm:RNU`

Source lines 1483–1495.

There exists an $\eta>0$ and a function $\fS(n)$ with the following properties. For $\foh N<n<N$, the singular series $\fS(n)$ is nonnegative, vanishes only when $n\notin\sA$, and is otherwise $ \gg_{\vep}N^{-\vep} $ for any $\vep>0$. Moreover, for $\foh N<n<N$ and admissible, \be \cR_{N}^{U}(n)\gg \fS(n) T^{\gd-1}, \ee except for a set of cardinality $\ll N^{1-\eta}$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: \ We restrict our attention to the set of admissible $n<N$ so that \eqref{eq:cMNUbnd} holds (the remainder having sufficiently small cardinality). Let $Z$ denote the subset of these $n$ for which $\cR_{N}^{U}(n)<\foh \cM_{N}^{U}(n)$; hence for $n\in Z$, $$ 1\ll {|\cE_{N}^{U}(n)|\over N^{-\vep}T^{\gd-1}} . $$ Then by \eqref{eq:cEN2bnd}, \beann |Z| &\ll_{\vep}& \sum _{n<N} {|\cE_{N}^{U}(n)|^{2} \over N^{-\vep}T^{2(\gd-1)}} \ll N^{1-\eta+\vep} , \eeann whence the claim follows, since $\vep>0$ is arbitrary.


Candidate references: `thm:CircMeth` (candidate_proof_dependency); `eq:cMNUbnd` (candidate_proof_dependency); `eq:cEN2bnd` (candidate_proof_dependency).

### Theorem [thm:CircMeth] — `thm:CircMeth`

Source lines 1574–1591.

There exists an $\eta>0$ and a decomposition \be \cR_{N}^{U}(n)=\cM_{N}^{U}(n)+\cE_{N}^{U}(n) \ee with the following properties. For $\foh N<n<N$ and admissible, $n\in\sA$, we have \be \cM_{N}^{U}(n)\gg \fS(n) T^{\gd-1}, \ee except for a set of cardinality $\ll N^{1-\eta}$. The singular series $\fS(n)$ is the same as in Theorem \ref{thm:RNU}. Moreover, \be \sum_{n<N}|\cE_{N}^{U}(n)|^{2} \ll N\, T^{2(\gd-1)} N^{-\eta} . \ee

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `thm:RNU` (internal_reference).

### Theorem [eq:gls] — `eq:gls`

Source lines 1796–1809.

Patterson, Sullivan, Lax-Phillips

The spectrum above $1$ is purely continuous, and the spectrum below $1$ is purely discrete. The latter is empty unless $\gd>1$, in which case, ordering the eigenvalues by \be 0<\gl_{0}<\gl_{1} \le \cdots\le \gl_{max}<1, \ee the base eigenvalue $\gl_{0}$ is given by $$ \gl_{0}=\gd(2-\gd). $$

*Extractive statement; proof gist not independently reconstructed.*

### Theorem [thm:specGap] — `thm:specGap`

Source lines 1865–1872.

Given $\G$ as above, there exists some $\vep=\vep(\G)>0$ such that for all $q\ge1$, \be \gl_{1}(q)\ge \gl_{0}+\vep. \ee

*Extractive statement; proof gist not independently reconstructed.*

### Theorem [eq:decayMtrx] — `eq:decayMtrx`

Source lines 1906–1922.

{\cite[Prop. 5.3]{KontorovichOh2011}}

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$. Then for any smooth vectors $v,w\in V^{\infty}$, \be \left| \<\pi(g).v,w\> \right| \ll \|g\|^{-2(2-\gT)} \cdot \cS v\cdot \cS w . \ee Here $\|\cdot\|$ is the standard Frobenius matrix norm. \\

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `external:KontorovichOh2011` (external_reference).

### Theorem [thm:Vin] — `thm:Vin`

Source lines 1954–2005.

{\cite{Vinogradov2013}}

Let $\Phi,\Psi\subset S^{2}$ be spherical caps and let $\cI\subset\R/\Z$ be an interval. Then under the above hypotheses on $\G$ (in particular $\gd>1$), and using the decomposition \eqref{eq:gDecomp}, we have \be \sum_{\g\in\G} \bo { \left\{ {c} s_{1}(\g)\in\Phi \\ s_{2}(\g)\in \Psi \\ \|a(\g)\|^{2}<T \\ m(\g)\in\cI \right\} } = c_{\gd}\cdot \mu(\Phi) \mu(\Psi) \ell(\cI) T^{\gd} + O\big( T^{ \gT } \big) , \ee as $T\to\infty$. Here $c_{\gd}>0$, $\|\cdot\|$ is the Frobenius norm, $\ell$ is Lebesgue measure, $\mu$ is Patterson-Sullivan measure (c

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `eq:gDecomp` (internal_reference); `eq:muPS` (internal_reference); `external:Vinogradov2013` (external_reference).

### Lemma [lem:spec0] — `lem:spec0`

Source lines 2047–2082.

Fix $\g_{1}\in\G$, $q\ge1$, and any ``congruence'' group $\tilde\G(q)$ satisfying \be \G(q)<\tilde\G(q)<\G. \ee Then as $Y\to\infty$, \bea && \hskip-.5in \#\{ \g\in\tilde\G(q) : \|\g_{1}\g\|<Y \} \\ && = {1\over [\G:\tilde\G(q)]} \cdot \#\{ \g\in\G : \|\g\|<Y \} + O(Y^{\gT_{0}}) , \eea where $\gT_{0}<\gd$ depends only on the spectral gap for $\G$. The implied constant above does not depend on $q$ or $\g_{1}$. The same holds with $\g_{1}\g$ in \eqref{eq:lemLHS} replaced by $\g\g_{1}$.

*Extractive statement; proof gist not independently reconstructed.*


Candidate references: `eq:lemLHS` (internal_reference).

### Lemma [lem:spec3] — `lem:spec3`

Source lines 2228–2251.

Let $\gT_{0}$ be as in \eqref{eq:lemRHS}. Define $\cC$ in \eqref{eq:TT1T2} by \be \cC:={10^{30}\over \gd-\gT_{0}}, \ee hence determining $T_{1}$ and $T_{2}$. There exists some $\eta_{0}>0$ depending only on the spectral gap of $\G$ so that for any $1\le q<N$ and any $r(\mod q)$, \be \sum_ {\g\in\fF} \bo_{\{ \<e_{1},\g v_{0}\> \equiv r(\mod q)\}} \ll {1\over q^{\eta_{0}}} T^{\gd} . \ee The implied constant is independent of $r$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Dropping the condition $\<e_{1},\g_{1}\,\g_{2}v_{0}\>>T/100$ in \eqref{eq:fFdef}, bound the left hand side of \eqref{eq:spec3} by \be \sum_ {\g_{1}\in\G\atop\|\g_{1}\|\asymp T_{1}} \sum_ {\g_{2}\in\G\atop\|\g_{2}\|\asymp T_{2}} \bo_{\{ \<e_{1},\g_{1}\g_{2} v_{0}\> \equiv r(\mod q)\}} \ee We decompose the argument into two ranges of $q$. {\bf Case 1: $q$ small.} In this range, we fix $\g_{1}$, and follow a standard argument for $\g_{2}$. Let $\tilde\G(q)<\G$ denote the stabilizer of $v_{0} (\mod q)$, that is \be \tilde\G(q):=\{\g\in\G:\g v_{0}\equiv v_{0}(\mod q)\}. \ee Clearly \eqref{eq:G1G} is satisfied, and it is elementary that \be [\G:\tilde\G(q)]\asymp q^{2}, \ee cf. \eqref{eq:Fuc}. Dec

- `eq:wStar` (proof_dependency; curated_source_check): First we assume the Claim and complete the proof of \eqref{eq:spec3}.

Candidate references: `eq:lemRHS` (internal_reference); `eq:TT1T2` (internal_reference); `eq:fFdef` (candidate_proof_dependency); `eq:spec3` (candidate_proof_dependency); `eq:G1G` (candidate_proof_dependency); `eq:Fuc` (candidate_proof_dependency); `eq:lemRHS` (candidate_proof_dependency); `eq:1` (candidate_proof_dependency); `eq:cCis` (candidate_proof_dependency); `eq:TT1T2` (candidate_proof_dependency); `eq:wStar` (candidate_proof_dependency); `eq:2` (candidate_proof_dependency); `eq:3` (candidate_proof_dependency); `eq:fdIs` (candidate_proof_dependency); `eq:qToT1` (candidate_proof_dependency); `external:LaxPhillips1982` (external_reference); `external:BourgainGamburd2009` (external_reference); `external:Hermann1926` (external_reference); 2 more in the JSON/interactive graph.

### Lemma [lem:spec1] — `lem:spec1`

Source lines 2455–2498.

Let $1<K\le T_{2}^{1/10}$, fix $|\gb|<K/N$, and fix $x,y\asymp X$. Then for any $\g_{0}\in\G$, any $q\ge1$, and any group $\tilde\G(q)$ satisfying \eqref{eq:G1G}, we have \bea \nonumber \sum_ {\g\in\fF\cap\{ \g_{0}\tilde\G(q)\}} e \bigg( \gb\, \ff_{\g}(2x,y) \bigg) &=& {1\over [\G:\tilde\G(q)]} \sum_ {\g\in\fF} e \bigg( \gb\, \ff_{\g}(2x,y) \bigg) \\ && \hskip1in + O( T^{\gT} K) , \eea where $\gT<\gd$ depends only on the spectral gap for $\G$, and the implied constant does not depend on $q$, $\g_{0}$, $\gb$, $x$ or $y$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: The proof follows with minor changes that of Lemma \ref{lem:spec0}, so we give a sketch; see also \cite[\S4]{BourgainKontorovichSarnak2010}. According to the construction \eqref{eq:fFdef} of $\fF$, the $\g$'s in question satisfy $\g=\g_{1}\g_{2}\in\g_{0}\tilde\G(q)$, and hence we can write $$ \g_{2}=\g_{1}^{-1}\g_{0}\g_{2}', $$ with $\g_{2}'\in\tilde\G(q)$. Then $\g_{2}'=\g_{0}^{-1}\g_{1}\g_{2}$, and using \eqref{eq:ffToInProd}, we can write the left hand side of \eqref{eq:spec1} as $$ \sum_{\g_{1}\in\G\atop T_{1}<\|\g_{1}\|<2T_{1}} \sum_{\g_{2}'\in\tilde\G(q)\atop T_{2}<\|\g_{1}^{-1}\g_{0}\g_{2}'\|<2T_{2}} \bo_{\{\<e_{1},\g_{0}\g_{2}'\,v_{0}\>>T/100\}}\ e \bigg( \gb\, \<w_{x,y}, \g_{0}\g_{2


Candidate references: `eq:G1G` (internal_reference); `lem:spec0` (candidate_proof_dependency); `eq:fFdef` (candidate_proof_dependency); `eq:ffToInProd` (candidate_proof_dependency); `eq:spec1` (candidate_proof_dependency); `eq:fgIs` (candidate_proof_dependency); `eq:FqIs` (candidate_proof_dependency); `eq:reg1Lem` (candidate_proof_dependency); `eq:cNq` (candidate_proof_dependency); `eq:reg2Lem` (candidate_proof_dependency); `eq:reg3Lem` (candidate_proof_dependency); `eq:NqErr` (candidate_proof_dependency); `eq:TT1T2` (candidate_proof_dependency); `eq:cCis` (candidate_proof_dependency); `external:BourgainKontorovichSarnak2010` (external_reference).

### Lemma [lem:spec2] — `lem:spec2`

Source lines 2576–2607.

Fix $N/2<n<N$, $1<K\le T_{2}^{1/10}$, and $x,y\asymp X$. Then \be \sum_ {\g\in \fF } \bo_{ \big\{ | \ff_{\g}(2x,y)- n| < \frac N{K} \big\} } \gg {T^{\gd}\over K} + T^{\gT} , \ee where $\gT<\gd$ only depends on the spectral gap for $\G$. The implied constant is independent of $x,y,$ and $n$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: The proof is an explicit calculation nearly identical to the one given in \cite[\S5]{BourgainKontorovichSarnak2010}; we give only a sketch here. Write the left hand side of \eqref{eq:spec2} as $$ \sum_{\g_{1}\in\G\atop T_{1}<\|\g_{1}\|<2T_{1}} \sum_{\g_{2}\in\G\atop T_{2}<\|\g_{2}\|<2T_{2}} \bo_{\{ \<e_{1},\g_{1}\g_{2}v_{0}\> > T/100 \}} \bo_{\{ |\<w_{x,y},\g_{1}\g_{2}v_{0}\>-n|<N/K \}} . $$ Fix $\g_{1}$ and express the condition on $\g_{2}$ as $\g_{2}\in R\subset G$, where $R$ is the region $$ R= R_{\g_{1},x,y,n}:= \left\{ g\in G : {c} T_{2}<\|g\|<2T_{2} \\ \<\g_{1}^{t}e_{1},g\, v_{0}\>>T/100 \\ |\<\g_{1}^{t}w_{x,y}, g\, v_{0} \> -n| < \frac N{K} \right\} . $$ Lift $G=\SO_{F}(\R)$ to its sp


Candidate references: `eq:spec2` (candidate_proof_dependency); `eq:iota` (candidate_proof_dependency); `eq:gDecomp` (candidate_proof_dependency); `eq:Vin` (candidate_proof_dependency); `thm:Vin` (candidate_proof_dependency); `external:BourgainKontorovichSarnak2010` (external_reference).

### Lemma [eq:cSfbnd1] — `eq:cSfbnd1`

Source lines 2701–2711.

With the above conditions, \be | \cS_{f}(q_{0},r;n,m) | \le q_{0}^{-1/2} . \ee

*Extractive statement; proof gist not independently reconstructed.*

### Lemma [eq:modBndaNeqAp] — `eq:modBndaNeqAp`

Source lines 3048–3068.

With the above notation, we have the estimate \be |\cS| \ll \left({q/ q_{0}}\right)^{2} { \{(a^{2},q_{0}) \cdot ((a')^{2},q_{0})\} ^{1/2} \over q^{5/4} } (a-a',q)^{1/4} . \ee

*Extractive statement; proof gist not independently reconstructed.*

### Lemma [eq:modBndaEqAp] — `eq:modBndaEqAp`

Source lines 3217–3239.

Assuming $a=a'$ and $f(m,-n)\neq f'(m',-n')$, we have the estimate \be |\cS| \ll (q/q_{0})^{5}\ { (a^{2},q_{0}) \over q^{9/8} } \cdot |f(m,-n)-f'(m',-n')|^{1/2} . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Assume first that $q$ (and hence $q_{0}$) is a prime power, continuing to omit the prime $2$. Returning to the definition of $\cS$ in \eqref{eq:cSdef}, it is clear in the case $a=a'$ that $$ \sum_{r(q)}'=(q/q_{0})\sum_{r(q_{0})}'. $$ Hence we again apply Kloosterman's $3/4$th bound to \eqref{eq:cS1}, getting \bea |\cS | &\ll& \bo_{ nC\equiv 2mB(\tilde q_{0}) \atop n'C'\equiv 2m'B'(\tilde q'_{0}) } (q/q_{0})^{9/2} { (a^{2},q_{0}) \over q^{5/4} } \\ \nonumber && \times \prod_{p^{j}\| q_{0}} \Bigg( p^{j} , \bar 4 \left\{ \overline{C'} (m')^{2} -\overline{C} m^{2} + \overline{ a_{1}} (a^{2},p^{j}) ( \overline{C'} (L')^{2} - \overline{C} L^{2} ) \right\} \Bigg)^{1/4} , \eea which is valid now wit


Candidate references: `eq:cSdef` (candidate_proof_dependency); `eq:cS1` (candidate_proof_dependency); `eq:tildQdef` (candidate_proof_dependency); `eq:Ldef` (candidate_proof_dependency); `eq:modBndaEqAp1` (candidate_proof_dependency); `eq:pr2` (candidate_proof_dependency); `eq:15` (candidate_proof_dependency); `eq:fmnfp` (candidate_proof_dependency); `eq:cP1` (candidate_proof_dependency); `eq:cP2` (candidate_proof_dependency).

### Lemma [eq:fincK] — `eq:fincK`

Source lines 3450–3457.

Fix an equivalence class $\cK$ of primitive binary quadratic forms of discriminant $-4a^{2}$. We claim that the number of equivalent forms $f\in\cK$ with $\ff=f-a\in\fF$ is bounded, that is, \be \#\{\ff\in\fF:f\in\cK\}=O(1). \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: From \eqref{eq:ABCdef}, \eqref{eq:fFdef}, and \eqref{eq:disc}, we have that $f(m,n)=Am^{2}+2Bmn+Cn^{2}$ has coefficients of size $$ A,B,C\ll T, $$ and $AC-B^{2}=a^{2}$, with $ a\asymp T. $ It follows that $AC\asymp T^{2}$, and hence \be A,C\asymp T. \ee Now suppose we have $\ff=f-a$ and $\ff'=f'-a$ with $f$ as above and $f'$ having coefficients $A',B',C'$. If $f$ and $f'$ are equivalent then there is an element $\mattwo ghij\in\GL(2,\Z)$ so that \bea A' &=& g^{2} A + 2 gi B + i^{2} C,\\ \nonumber B' &=& gh A + (gj+hi) B + ij C ,\\ \nonumber C' &=& h^{2} A + 2 hj B + j^{2} C. \eea The first line can be rewritten as $$ A' = C ( i + g B /C )^{2} + g^{2} {4a^{2}\over C} , $$ so that $$ g^{2} \le


Candidate references: `eq:ABCdef` (candidate_proof_dependency); `eq:fFdef` (candidate_proof_dependency); `eq:disc` (candidate_proof_dependency).

### Lemma [eq:cKzBnd] — `eq:cKzBnd`

Source lines 3520–3533.

For a fixed large integer $z$, the number of inequivalent classes $\cK$ of primitive quadratic forms of determinant $-4a^{2} $ which represent $z$ is \be \ll_{\vep}\ z^{\vep}\cdot (z,4a^{2})^{1/2} , \qquad \text{for any $\vep>0$.} \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: If $f\in\cK$ represents $z$, say $f(m,n)=z$, then, setting $w=(m,n)$, $f$ represents $z_{1}:=z/w^{2}$ primitively. We see from \eqref{eq:ApBpCpABC} that $f$ is then in the same class as $f_{1}(m,n)=z_{1}m^{2}+2Bmn+Cn^{2}$, with $$ -4a^{2}=z_{1}C-B^{2} . $$ Moreover, by a unipotent change of variables preserving $z_{1}$, we can force $B$ into the range $[0,z_{1})$, that is, $B$ is determined mod $z_{1}$. So the number of inequivalent such $f_{1}$ is equal to \be \#\{B(\mod z_{1}):B^{2}\equiv-4a^{2}(z_{1})\} = \prod_{p^{e}\mid\mid z_{1}} \#\{B^{2}\equiv-p^{2f}(p^{e})\} , \ee where $p^{f}\mid\mid 2a$. If $2f\ge e$, then the number of local solutions is at most $p^{e/2}$. Otherwise, write $B=B_{


Candidate references: `eq:ApBpCpABC` (candidate_proof_dependency); `eq:BtoZ1` (candidate_proof_dependency).

### Lemma [lem:kEllD] — `lem:kEllD`

Source lines 3559–3566.

Fix $(A,B,C)=1$ and $d\mid AC-B^{2}$. Then there are integers $k,\ell $ with $(k,\ell,d)=1$ so that, whenever $Am^{2}+2Bmn+Cn^{2}\equiv0(d)$, we have \be (mk+n\ell)^{2}\equiv0(d). \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: We will work locally, then lift to a global solution. Let $p^{e}\mid\mid d$. Case 1: If $(p,A)=1$, then $Am^{2}+2Bmn+Cn^{2}\equiv0(p^{e})$ implies $$ (m+\bar A Bn)^{2}-\bar A ^{2}B^{2}n^{2}+\bar ACn^{2}\equiv (m+\bar A Bn)^{2}\equiv 0(p^{e}). $$ In this case, we set $k_{p}:=1$, and $\ell_{p}:={\bar A B}$. Case 2: If $(p,A)>1$, then by primitivity, $(p,C)=1$. As before, we have $ (n+\bar C Bm)^{2}\equiv 0(p^{e}), $ and we choose $k_{p}={\bar C B}$, $\ell_{p}:=1$. By the Chinese Remainder Theorem, there are integers $k$ and $\ell$ so that $k\equiv k_{p}(\mod p^{e})$, and similarly with $\ell$. By construction, we have $(k,\ell,d)=1$, as claimed.

### Lemma [eq:nmUpToM] — `eq:nmUpToM`

Source lines 3590–3602.

Given large $M$, $(A,B,C)=1$ and $d\mid AC-B^{2}$, \be \#\{m,n<M:Am^{2}+2Bmn+Cn^{2}\equiv0(d)\} \ee $$ \ll_{\vep} d^{\vep} \left({M^{2}\over d^{1/2}}+M\right) . $$

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: As in Lemma \ref{lem:kEllD}, $A,B,C$ and $d$ determine $k,\ell$ so that $$ \sum_{m,n<M}\bo_{\{Am^{2}+2Bmn+Cn^{2}\equiv0(d)\}} \le \sum_{m,n<M}\bo_{\{(mk+n\ell)^{2}\equiv0(d)\}} . $$ But then there is a $d_{1}\mid d$, with $d\mid d_{1}^{2}$ so that $mk+n\ell\equiv0(d_{1})$. Let $w=(\ell, d_{1})$; then $mk\equiv0(w)$ implies $m\equiv0(w)$ since $(k,\ell,d)=1$. There are at most $1+M/w$ such $m$ up to $M$. With $m$ fixed, $n$ is uniquely determined mod $d_{1}/w$. Hence we get the bound \beann \eqref{eq:nmUpToM} &\le& \sum_{d_{1}\mid d\atop d\mid d_{1}^{2}} \sum_{w\mid d_{1}} \sum_{m,n<M}\bo_{\{m\equiv0(\mod w)\}}\bo_{\{ n\equiv-\overline{\frac \ell w}\frac mw k(\mod \frac{d_{1}}w)\}} \\ &\ll& \


Candidate references: `lem:kEllD` (candidate_proof_dependency).

### Proposition [eq:eqeq] — `eq:eqeq`

Source lines 3644–3671.

For large $M$ and $\ff=f-a\in\fF$ fixed, \be \# \left\{ {c} \ff'\in\fF \\ m,n,m',n'<M \Bigg| {c} a'=a\\ \ff(m,-n)=\ff'(m',-n') \right\} \ll_{\vep} (TM)^{\vep} \left( M^{2} + TM \right) , \ee for any $\vep>0$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Once $f,m,n$, and $\ff'=f'-a\in\fF$ are determined, it is elementary that there are $\ll_{\vep} M^{\vep}$ values of $m',n'$ with $f(m,-n)=f'(m',-n')$. Decomposing $f'$ into classes and applying \eqref{eq:fincK}, \eqref{eq:cKzBnd}, and \eqref{eq:nmUpToM}, in succession, we have \beann && \hskip-1in \sum_{m,n<M} \sum_{\ff'\in\fF\atop a'=a} \sum_{m',n'<M} \bo_{\{f(m,-n)=f'(m',-n')\}} \\ &\ll_{\vep}& \sum_{m,n<M} \sum_{\ff'\in\fF\atop a'=a} \bo_{\{f'\text{ represents }f(m,-n)\}} M^{\vep} \\ &\ll& M^{\vep} \sum_{m,n<M} \sum_{\text{classes }\cK\atop\text{representing }f(m,-n)} \sum_{\ff'\in\fF\atop a'=a,f'\in\cK} 1 \\ &\ll_{\vep}& (TM)^{\vep} \sum_{m,n<M} (f(m,-n),4a^{2})^{1/2} \\ &\ll& (TM)^{\vep


Candidate references: `eq:fincK` (candidate_proof_dependency); `eq:cKzBnd` (candidate_proof_dependency); `eq:nmUpToM` (candidate_proof_dependency).

### Theorem [thm:cMNis] — `thm:cMNis`

Source lines 3862–3869.

For $\foh N<n<N$, there exists a function $\fS(n)$ as in Theorem \ref{thm:RNU} so that \be \cM_{N}(n)\gg\fS(n)T^{\gd-1} . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: First we discuss the modular component. Write $\fS_{Q_{0}}$ as $$ \fS_{Q_{0}}(n) = \sum_{q<Q_{0}} {1\over [\G:\tilde\G(q)] } \sum_{\g_{0}\in\G/\tilde\G(q)} c_{q}(\<w_{x,y},\g_{0} v_{0}\>-n) , $$ where $c_{q}$ is the Ramanujan sum, $c_{q}(m)=\sum_{r(q)}'e_{q}(rm)$. By \eqref{eq:Fuc}, the analysis now reduces to a classical estimate for the singular series. We may use the transitivity of the $\g_{0}$ sum to replace $\<w_{x,y},\g_{0} v_{0}\>$ by $\<e_{4},\g_{0} v_{0}\>$, extend the sum on $q$ to all natural numbers, and use multiplicativity to write the sum as an Euler product. Then the resulting singular series $$ \fS(n) := \prod_{p} \left[ 1+ \sum_{k\ge1} {1\over[\G:\G_{0}(p^{k})]} \sum_{\g_{


Candidate references: `thm:RNU` (internal_reference); `eq:Fuc` (candidate_proof_dependency); `eq:hatFunc` (candidate_proof_dependency); `lem:spec2` (candidate_proof_dependency); `eq:fMdecomp` (candidate_proof_dependency); `eq:cMNUn` (candidate_proof_dependency); `eq:cMNbnd` (candidate_proof_dependency); `eq:Q0is` (candidate_proof_dependency); `eq:TXNis` (candidate_proof_dependency); `external:BourgainKontorovich2010` (external_reference).

### Theorem [thm:cMNtoMNU] — `thm:cMNtoMNU`

Source lines 3945–3950.

There is an $\eta>0$ such that the bound \eqref{eq:cMNbnd} holds with $\cM_{N}$ replaced by $\cM_{N}^{U}$, except on a set of cardinality $\ll N^{1-\eta}$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Putting \eqref{eq:fMdecomp} into \eqref{eq:cMNUn} gives \beann && \hskip-.5in \sum_{n<N} |\cM_{N}(n)-\cM_{N}^{U}(n)| \ll \sum_{x,y\asymp X} \sum_{n<N}|\fM(n)| \sum_{u\mid(2x,y)\atop u\ge U} 1 \\ &\ll_{\vep}& \sum_{y<X} \sum_{u\mid y\atop u\ge U} \sum_{x<X\atop 2x\equiv0(\mod u)} \left\{ N^{\vep} \sum_{\ff\in\fF} {K_{0}\over N} \left[ \sum_{n<N} \hat\ft \left( (\ff(2x,y)-n) \frac {K_{0}}N \right) \right] + K_{0}^{2}Q_{0}^{4}T^{\gT_{1}} \right\} \\ &\ll& N^{\vep} X\frac XU T^{\gd} , \eeann using \eqref{eq:fSbnd} and \eqref{eq:Q0is}. The rest of the argument is identical to that leading to \eqref{eq:nZbnd}.


Candidate references: `eq:cMNbnd` (internal_reference); `eq:fMdecomp` (candidate_proof_dependency); `eq:cMNUn` (candidate_proof_dependency); `eq:fSbnd` (candidate_proof_dependency); `eq:Q0is` (candidate_proof_dependency); `eq:nZbnd` (candidate_proof_dependency).

### Lemma [eq:cRfuIs] — `eq:cRfuIs`

Source lines 4105–4138.

Recalling the notation \eqref{eq:cSfDef}, we have \be \hat\cR_{f,\d }\left(\frac rq+\gb\right) = {1\over \d ^{2}} \sum_{n,m\in\Z} \cJ_{f}\left(X,\gb;{n\over \d q_{0}},{m\over \d q_{0}}\right) \cS_{f}(q_{0},r\d _{0};n,m) , \ee where we have set \be \cJ_{f}\left(X,\gb;{n\over uq_{0}},{m\over uq_{0}}\right) := \iint\limits_{x,y\in\R} \gU\left({x\over X}\right) \gU\left({y\over X}\right) e \bigg( \gb f(x,y) -{n\over uq_{0}}x-{m\over uq_{0}}y \bigg) dx dy . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Returning to \eqref{eq:cRffuIs}, we have \beann \hat\cR_{f,\d}\left(\frac rq+\gb\right) &=& \sum_{x,y\in\Z} \gU\left({\d x\over X}\right) \gU\left({\d y\over X}\right) e_{q_{0}} \bigg( r \d_{0} f( x,y) \bigg) e \bigg( \gb \d^{2} f(x,y) \bigg) \\ &=& \sum_{k(q_{0})} \sum_{\ell( q_{0})} e_{q_{0}} \bigg( r \d_{0} f(k,\ell) \bigg) \\ && \times \left[ \sum_{x\in\Z\atop x\equiv k(q_{0})} \sum_{y\in\Z\atop y\equiv \ell(q_{0})} \gU\left({\d x\over X}\right) \gU\left({\d y\over X}\right) e \bigg( \gb \d^{2} f(x,y) \bigg) \right] . \eeann Apply Poisson summation to the bracketed term above: \beann \Bigg[ \cdot \Bigg] &=& \sum_{x,y\in\Z} \gU\left({\d (q_{0}x+k)\over X}\right) \gU\left({\d (q_{0}y+\ell)


Candidate references: `eq:cSfDef` (internal_reference); `eq:cRffuIs` (candidate_proof_dependency).

### Proposition [eq:hatRfuBnd] — `eq:hatRfuBnd`

Source lines 4245–4257.

With the above notation, \be \left| \hat\cR_{f,\d }\left(\frac rq+\gb\right) \right| \ll u (\sqrt{q}|\gb|T)^{-1} . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: By (non)stationary phase (see, e.g., \cite[\S8.3]{IwaniecKowalski}), the integral in \eqref{eq:cJfIs} has negligible contribution unless $$ {|n|\over \d q_{0}}, {|m|\over \d q_{0}} \ll |\gb|\cdot |\nabla f|\ll |\gb|\cdot TX, $$ so the $n,m$ sum can be restricted to \be |n|,|m|\ll |\gb|\cdot TX\cdot \d q_{0} \ll \d . \ee Here we used $|\gb|\ll (qM)^{-1}$ with $M$ given by \eqref{eq:Mis}. In this range, stationary phase gives \be \left| \cJ_{f}\left(X,\gb;{n\over \d q_{0}},{m\over \d q_{0}}\right)\right| \ll\min\left(X^{2},{1\over |\gb|\cdot|\operatorname{discr}(f)|^{1/2}}\right) \ll\min\left(X^{2},{1\over |\gb| T}\right) , \ee using \eqref{eq:disc} and \eqref{eq:fFTbnd} that $|\operatorname{d


Candidate references: `eq:cJfIs` (candidate_proof_dependency); `eq:Mis` (candidate_proof_dependency); `eq:disc` (candidate_proof_dependency); `eq:fFTbnd` (candidate_proof_dependency); `eq:nmRest` (candidate_proof_dependency); `eq:cJfbnd` (candidate_proof_dependency); `eq:cSfbnd1` (candidate_proof_dependency); `eq:cRfuIs` (candidate_proof_dependency); `eq:tilQis` (candidate_proof_dependency); `external:IwaniecKowalski` (external_reference).

### Theorem [thm:IQ0] — `thm:IQ0`

Source lines 4311–4320.

Recall the integrals $\cI_{Q_{0},K_{0}},\ \cI_{Q_{0}}$ from \eqref{eq:IQ0K0}, \eqref{eq:IQ0}. There is an $\eta>0$ so that $$ \cI_{Q_{0},K_{0}}, \ \cI_{Q_{0}}\ll N\, T^{2(\gd-1)}\, N^{-\eta} , $$ as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: We first handle $\cI_{Q_{0},K_{0}}$. Returning to \eqref{eq:RNRf} and applying \eqref{eq:hatRfuBnd} gives $$ \left| \widehat{\cR_{N}^{U}} \left(\frac rq+\gb\right) \right| \ll \sum_{\d< U} \sum_{\ff\in\fF} u (\sqrt{q}|\gb|T)^{-1} \ll U^{2} T^{\gd-1} (\sqrt{q}|\gb|)^{-1} . $$ Inserting this into \eqref{eq:IQ0K0} and using \eqref{eq:Q0is}, \eqref{eq:fuIs} gives \beann \cI_{Q_{0},K_{0}} &\ll& \sum_{q<Q_{0}} \sideset{}{'}\sum_{r(q)} \int_{|\gb|<K_{0}/N} \left| \gb \frac N{K_{0}} \right|^{2} U^{4} T^{2(\gd-1)} {1\over q|\gb|^{2}} d\gb \\ &\ll& Q_{0} \frac N{K_{0}} U^{4} T^{2(\gd-1)} \ll N T^{2(\gd-1)} N^{-\eta} . \eeann Next we handle \beann \cI_{Q_{0}} &\ll& \sum_{q<Q_{0}} \sideset{}{'} \sum_{r(


Candidate references: `eq:IQ0K0` (internal_reference); `eq:IQ0` (internal_reference); `eq:RNRf` (candidate_proof_dependency); `eq:hatRfuBnd` (candidate_proof_dependency); `eq:IQ0K0` (candidate_proof_dependency); `eq:Q0is` (candidate_proof_dependency); `eq:fuIs` (candidate_proof_dependency).

### Lemma [eq:cIQ1def] — `eq:cIQ1def`

Source lines 4517–4537.

Assume $Q<X$. For $\square\in\{=,\neq\}$, we have \be \cI_{Q}^{(\square)} \ll U^{6} {X^{2}\over T} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'\square a} \sum_{q\asymp Q} { \{(a^{2},q)\cdot((a')^{2},q)\}^{1/2}(a-a',q)^{1/4} \over q^{5/4} } . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Apply \eqref{eq:modBndaNeqAp} and \eqref{eq:nmRest}, \eqref{eq:cJfbnd} to \eqref{eq:IQbnd1}, giving \beann \cI_{Q}^{(\square)} &\ll& U \sum_{u<U} {1\over u^{4}} \sum_{|n|,|m|,|n'|,|m'|\ll u}\ \sum_{\ff,\ff'\in\fF\atop a'\square a}\ \sum_{q\asymp Q} \\ && \qquad \times {u^{4} \{(a^{2},q)\cdot((a')^{2},q)\}^{1/2}(a-a',q)^{1/4} \over q^{5/4} } \\ && \qquad \qquad \times \int_{|\gb|<1/(qM)} \min\left( X^{2}, {1\over |\gb|T} \right)^{2} d\gb , \eeann where we used \eqref{eq:tilQis}. The claim then follows immediately from \eqref{eq:Mis} and $Q<X$.


Candidate references: `eq:modBndaNeqAp` (candidate_proof_dependency); `eq:nmRest` (candidate_proof_dependency); `eq:cJfbnd` (candidate_proof_dependency); `eq:IQbnd1` (candidate_proof_dependency); `eq:tilQis` (candidate_proof_dependency); `eq:Mis` (candidate_proof_dependency).

### Proposition [eq:cIQ2bnd] — `eq:cIQ2bnd`

Source lines 4576–4583.

There is an $\eta>0$ such that \be \cI_{Q}^{(=)}\ll N \, T^{2(\gd-1)}N^{-\eta}, \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: From \eqref{eq:cIQ1def}, we have \beann \cI_{Q}^{(=)} &\ll& U^{6} {X^{2}\over T} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'=a} \sum_{q\asymp Q} {(a^{2},q)\over q} \\ &\ll& {U^{6} X^{2}\over QT} \sum_{\ff\in\fF} \sum_{\tilde q_{1}\mid a^{2}\atop\tilde q_{1}\ll Q} \tilde q_{1} \sum_{q\asymp Q\atop q\equiv0(\tilde q_{1})} \sum_{\ff'\in\fF\atop a'=a} 1 \\ &\ll_{\vep}& {U^{6} X^{2}\over T} \sum_{\ff\in\fF} T^{\vep} \sum_{\ff'\in\fF\atop a'=a} 1 . \eeann 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}: $$ \cI_{Q}^{(=)} \ll_{\vep} {U^{6} X^{2}\over T} T^{\gd} T^{\vep} {T^{\gd}\over Q_{0}^{\eta_{0}}} .


Candidate references: `eq:cIQ1def` (candidate_proof_dependency); `eq:spec3` (candidate_proof_dependency); `eq:fuIs` (candidate_proof_dependency); `eq:TXNis` (candidate_proof_dependency).

### Proposition [eq:cIQ11bnd] — `eq:cIQ11bnd`

Source lines 4645–4652.

There is an $\eta>0$ such that \be \cI_{Q}^{(\neq,>)}\ll N \, T^{2(\gd-1)}N^{-\eta}, \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Writing $(a,a')=h>H$, $\tilde q_{1}=(a^{2},q)$, $\tilde q_{1}'=((a')^{2},q)$, and using $(a-a',q)\le q$ in \eqref{eq:cIQ1def}, we have \beann \cI_{Q}^{(\neq,>)} &\ll& U^{6} {X^{2}\over T} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'\neq a,(a,a')>H} \sum_{q\asymp Q} { \{(a^{2},q)\cdot((a')^{2},q)\}^{1/2}(a-a',q)^{1/4} \over q^{5/4} } \\ &\ll& U^{6} {X^{2}\over T} \sum_{\ff\in\fF} \sum_{h\mid a\atop h>H} \sum_{\ff'\in\fF\atop a'\equiv 0(\mod h)} \sum_{\tilde q_{1}\mid a^{2}\atop \tilde q_{1}\ll Q} \sum_{\tilde q_{1}'\mid (a')^{2}\atop [\tilde q_{1},\tilde q_{1}']\ll Q} (\tilde q_{1} \tilde q_{1}')^{1/2} \sum_{q\asymp Q\atop q\equiv 0([\tilde q_{1},\tilde q_{1}'])} {1\over Q} \\ &\ll_{\vep}& U^{6}


Candidate references: `eq:cIQ1def` (candidate_proof_dependency); `eq:spec3` (candidate_proof_dependency); `eq:His` (candidate_proof_dependency); `eq:fuIs` (candidate_proof_dependency).

### Proposition [eq:cIQ12bnd] — `eq:cIQ12bnd`

Source lines 4712–4719.

There is an $\eta>0$ such that \be \cI_{Q}^{(\neq,\le)}\ll N \, T^{2(\gd-1)}N^{-\eta}, \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: First note that \beann \cI_{Q}^{(\neq,\le)} &=& U^{6} {X^{2}\over T} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'\neq a,(a,a')\le H} \sum_{q\asymp Q} { \{(a^{2},q)\cdot((a')^{2},q)\}^{1/2}(a-a',q)^{1/4} \over q^{5/4} } \\ &\ll& U^{6} {X^{2}\over T} {1\over Q^{5/4}} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'\neq a, (a,a')\le H} \sum_{q\asymp Q} (a,q) (a',q) (a-a',q)^{1/4} . \eeann Write $g=(a,q)$ and $g'=(a',q)$, and let $h=(g,g')$; observe then that $h\mid (a,a')$ and $h\ll Q$. Hence we can write $g=hg_{1}$ and $g'=hg_{1}'$ so that $(g_{1},g_{1}')=1$. Note also that $h\mid (a-a',q)$, so we can write $(a-a',q)=h\tilde g$; thus $g_{1},g_{1}',$ and $\tilde g$ are pairwise coprime, implying $$ [hg_{


Candidate references: `lem:spec3` (candidate_proof_dependency); `eq:His` (candidate_proof_dependency); `eq:fuIs` (candidate_proof_dependency).

### Theorem [thm:IQX] — `thm:IQX`

Source lines 4838–4845.

For $Q_{0}\le Q<X$, there is some $\eta>0$ such that $$ \cI_{Q}\ll N\, T^{2(\gd-1)}\, N^{-\eta}, $$ as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

### Lemma [eq:cIQ3def] — `eq:cIQ3def`

Source lines 4963–4985.

Assume $Q\ge X$. For $\square\in\{=,\neq\}$, we have \be \cI_{Q}^{(\square)} \ll {U X^{3} \over QT} \sum_{u<U} {1\over u^{4}} \sum_{q\asymp Q}\ \sum_{n,m,n',m'\ll {U Q\over X}} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'\square a} |\cS| . \ee

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Consider the sum $\gl_{f}$ in \eqref{eq:glfDef}. Since $x,y\asymp X/u$, $|\gb|<1/(qM)$, $X\le Q$, and using \eqref{eq:Mis}, we have that $$ |\gb u^{2} f(x,y)|\ll \frac1{QM} u^{2} T\left(\frac Xu\right)^{2}= \frac XQ\le 1. $$ Hence there is contribution only if $nx/q_{0}, my/q_{0} \ll 1$, that is, we may restrict to the range $$ n,m\ll u q_{0}/X . $$ In this range, we give $\gl_{f}$ the trivial bound of $X^{2}/u^{2}$. Putting this analysis into \eqref{eq:IQbnd2}, the claim follows.


Candidate references: `eq:glfDef` (candidate_proof_dependency); `eq:Mis` (candidate_proof_dependency); `eq:IQbnd2` (candidate_proof_dependency).

### Proposition [eq:cI3bnd] — `eq:cI3bnd`

Source lines 5004–5014.

Assuming $X\le Q<M$, there is some $\eta>0$ such that \be \cI_{Q}^{(\neq)} \ll N\, T^{2(\gd-1)}\, N^{-\eta} , \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Since \eqref{eq:modBndaNeqAp} is such a large savings in $q>X$, we can afford to lose in the much smaller variable $T$. Hence put \eqref{eq:modBndaNeqAp} into \eqref{eq:cIQ3def}, estimating $(a-a',q)\le |a-a'|$ (since $a\neq a'$): \beann \cI_{Q}^{(\neq)} &\ll& {U X^{3} \over QT} \sum_{u<U} {1\over u^{4}} \sum_{q\asymp Q}\ \sum_{n,m,n',m'\ll {UQ\over X}} \sum_{\ff,\ff'\in\fF} u^{4} { a \cdot a' \over q^{5/4} } |a-a'|^{1/4} \\ &\ll& {U^{6} X^{3} \over T} \left( {Q\over X}\right)^{4} T^{2\gd} { T^{2}\over Q^{5/4}} T^{1/4} \\ &\ll& U^{6} X^{7/4} T^{2\gd} T^{4} = X^{2}T\, T^{2(\gd-1)} \, \left( U^{6} X^{-1/4} T^{5} \right) , \eeann where we used \eqref{eq:tilQis}, $Q<M$, and \eqref{eq:Mis}. Using


Candidate references: `eq:modBndaNeqAp` (candidate_proof_dependency); `eq:cIQ3def` (candidate_proof_dependency); `eq:tilQis` (candidate_proof_dependency); `eq:Mis` (candidate_proof_dependency); `eq:TXNis` (candidate_proof_dependency); `eq:fuIs` (candidate_proof_dependency).

### Proposition [eq:cI42bnd] — `eq:cI42bnd`

Source lines 5095–5105.

Assuming $Q<XT$, there is some $\eta>0$ such that \be \cI_{Q}^{(=,\neq)} \ll N\, T^{2(\gd-1)}\, N^{-\eta} , \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Returning to \eqref{eq:cIQ3def}, apply \eqref{eq:modBndaEqAp}: \beann \cI_{Q}^{(=,\neq)} &\ll& {U X^{3} \over QT} \sum_{u<U} {1\over u^{4}} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'= a} \sum_{q\asymp Q}\ \sum_{n,m\ll {U Q\over X}} \sum_{n',m'\ll {U Q\over X}\atop \ff(m,-n)\neq\ff'(m',-n')} |\cS| \\ &\ll& {U X^{3} \over QT} \sum_{u<U} {1\over u^{4}} \sum_{\ff,\ff'\in\fF} \sum_{\tilde q_{1}\mid a^{2}\atop \tilde q_{1}\ll Q} \sum_{q\asymp Q\atop q\equiv0(\tilde q_{1})} \sum_{n,m,n',m'\ll {U Q\over X}} u^{10} { \tilde q_{1} \over Q^{9/8} } \left(T\left({UQ\over X}\right)^{2}\right)^{1/2} \\ &\ll_{\vep}& {U^{8} X^{3} \over T} T^{2\gd}\, T^{\vep} \left( {U Q\over X}\right)^{4} { 1\over Q^{9/8} } T


Candidate references: `eq:cIQ3def` (candidate_proof_dependency); `eq:modBndaEqAp` (candidate_proof_dependency); `eq:TXNis` (candidate_proof_dependency).

### Proposition [eq:cI41bnd] — `eq:cI41bnd`

Source lines 5193–5203.

Assuming $Q<XT$, there is some $\eta>0$ such that \be \cI_{Q}^{(=,=)} \ll N\, T^{2(\gd-1)}\, N^{-\eta} , \ee as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Returning to \eqref{eq:cIQ3def}, apply \eqref{eq:modBndaNeqAp}, and \eqref{eq:eqeq}: \beann \cI_{Q}^{(=,=)} &\ll& {U X^{3} \over QT} \sum_{u<U} {1\over u^{4}} \sum_{q\asymp Q}\ \sum_{n,m\ll {UQ\over X}} \sum_{\ff\in\fF} \sum_{\ff'\in\fF\atop a'= a} \sum_{n',m'\ll UQ/X\atop \ff(m,-n)=\ff'(m',-n')} \hskip-.3in u^{4} {(a^{2},q)\over q^{5/4}}q^{1/4} \\ &\ll& {U X^{3} \over Q^{2}T} \sum_{u<U} \sum_{\ff\in\fF} \sum_{\tilde q_{1}\mid a^{2}\atop\tilde q_{1}\ll Q} \tilde q_{1} \sum_{q\asymp Q\atop q\equiv0(\tilde q_{1})}\ \left[ \sum_{n,m\ll {UQ\over X}} \sum_{\ff'\in\fF\atop a'= a} \sum_{n',m'\ll UQ/X\atop \ff(m,-n)=\ff'(m',-n')} 1 \right] \\ &\ll_{\vep}& N^{\vep} {U X^{3} \over Q^{2}T} U T^{\gd} Q 


Candidate references: `eq:cIQ3def` (candidate_proof_dependency); `eq:modBndaNeqAp` (candidate_proof_dependency); `eq:eqeq` (candidate_proof_dependency); `eq:dim` (candidate_proof_dependency).

### Theorem [thm:IQM] — `thm:IQM`

Source lines 5273–5281.

If $X\le Q<M$, then there is some $\eta>0$ so that $$ \cI_{Q}\ll N\, T^{2(\gd-1)} \, N^{-\eta}, $$ as $N\to\infty$.

*Extractive statement; proof gist not independently reconstructed.*

### Theorem [th_sg] — `th_sg`

Source lines 5433–5438.

Let $\bar\Ga$ be the Apollonian group and $\gl'_1(q)$ be as above. There is an absolute constant $c>0$ such that $\gl_1'(q)<1-c$ for all $q$. I.e. the Apollonian group has combinatorial spectral gap.

*Extractive statement; proof gist not independently reconstructed.*

### Lemma [lm_transference] — `lm_transference`

Source lines 5483–5496.

Let $G$ be a finite group and $S\subset G$ a finite symmetric generating set. Let $G_1,G_2,\ldots,G_k$ be subgroups of $G$ such that for every $g\in G$ there are $g_1\in G_1,\ldots,g_k\in G_k$ such that $g=g_1\cdots g_k$. Then \[ 1-\gl_1'(G,S)\ge\min_{1\le i\le k} \left\{\frac{|S\cap G_{i}|}{|S|}\cdot \frac{1-\gl_1'(G_{i},S\cap G_{i})}{2k^2}\right\}. \]

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Denote by $\pi$ the regular representation of $G$, i.e. we write \[ \pi(g_0)f(g)=f(g_0^{-1}g) \] for $f\in L^2(G)$ and $g,g_0\in G$. Let $T_{G,S}$ be the Markov operator defined above. Let $f_0\in L^2(G)$ be an eigenfunction with $\|f_0\|_2=1$ corresponding to $\gl_1'(G,S)$. It is orthogonal to the constant and \[ \langle T_{G,S}f_0,f_0\rangle=\gl_1'(G,S). \] Since $f_0$ is orthogonal to the constant, we have \[ \sum_{g\in G}\langle \pi(g)f_0,f_0 \rangle=|\langle f_0,1\rangle|^2=0. \] Thus there is $g_0\in G$ such that $\langle \pi(g_0)f_0,f_0 \rangle\le0$ and hence $\|\pi(g_0)f_0-f_0\|_2\ge\sqrt2$. By the hypothesis of the lemma, there are $g_i\in G_i$ for $1\le i\le k$ such that $g_0=g_1\c


Candidate references: `eq_TSG1` (candidate_proof_dependency); `eq_TSG2` (candidate_proof_dependency).

### Lemma [lm_generation] — `lm_generation`

Source lines 5511–5518.

Let $q\ge2$ be an integer. Then for every $g\in \bar\Ga/\bar\Ga(q)$, there are $g_1,\ldots, g_{10^{13}}\in\Ga_1/\Ga_1(q)$ and $h_1,\ldots, h_{10^{13}}\in\Ga_2/\Ga_2(q)$ such that $g=g_1h_1\cdots g_{10^{13}}h_{10^{13}}$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: Let $q$ be an integer and $q=p_1^{m_1}\cdots p_n^{m_n}$ where $p_i$ are primes. We prove that \[ A_{10^{13}}(q)=A_{10^{13}}(p_1^{m_1})\times\ldots\times A_{10^{13}}(p_n^{m_n}). \] Let $x\in A_{10^{13}}(p_1^{m_1})\times\ldots\times A_{10^{13}}(p_n^{m_n})$ be arbitrary. By definition, for each $k$, we can find elements $g_1^{(k)},\ldots g_{10^{13}}^{(k)}\in \Ga_1/\Ga_1(q)$ and $h_1^{(k)},\ldots h_{10^{13}}^{(k)}\in \Ga_2/\Ga_2(q)$ such that \[ x\equiv g_1^{(k)}h_1^{(k)}\cdots g_{10^{13}}^{(k)}h_{10^{13}}^{(k)}\;{\rm mod}\; p_k^{m_k}. \] Since $\Ga_1/\Ga_1(p^m)$ and $\Ga_2/\Ga_2(p^m)$ are the direct product of local factors, we can find elements $g_1,\ldots, g_{10^{13}}\in\Ga_1/\Ga_1(p^m)$ and 


Candidate references: `lm_local` (candidate_proof_dependency).

### Lemma [lm_local] — `lm_local`

Source lines 5623–5627.

Let $p$ be a prime and $m$ a positive integer. Then $A_{10^{13}}(p^m)=\bar\Ga/\bar\Ga(p^m)$.

*Extractive statement; proof gist not independently reconstructed.*

Proof opening: We give the proof for $p=2$ and then explain the differences for $p=3$. We prove by induction the following statement. For every $m\ge7$ and $g\in\bar\Ga(2^7)/\bar\Ga(2^m)$, there are $g_1,g_2,g_3\in \Ga_1(2^{2})/\Ga_1(2^m)$ such that \[ g=g_1\g_3g_2\g_3^{-1}\g_3^2 g_3\g_3^{-2}. \] For $m=7$ this is clear since we can take $g_1=g_2=g_3=1$. Now assume that $m>7$ and the statement holds for $m-1$. In this proof, we denote by $1$ the multiplicative unit (identity matrix) and by $0$ the matrix with all entries 0. Let $g\in\bar\Ga(2^7)/\bar\Ga(2^m)$ be arbitrary. By the induction hypothesis, there is $h_1,h_2,h_3\in \Ga_1(2^{2})/\Ga_1(2^m)$ such that \[ g-h_1\g_3h_2\g_3^{-1}\g_3^2 h_3\g_3^{-2}=2^


Candidate references: `eq:unip` (candidate_proof_dependency); `eq_Gamma1` (candidate_proof_dependency).

## External inputs and references

### [Ber12] Bernays1912 — `external:Bernays1912`

Source lines 5944–5952.

P.~Bernays. \newblock {\em \"{U}ber die {D}arstellung von positiven, ganzen {Z}ahlen durch die primitiven, bin\"{a}ren quadratischen {F}ormen einer nicht quadratischen {D}iskriminante}. \newblock PhD thesis, Georg-August-Universit\"{a}t, G\"{o}ttingen, Germany, 1912.


Candidate references: `sec:prelim` (external_reference).

### [BF10] BourgainFuchs2010 — `external:BourgainFuchs2010`

Source lines 5952–5958.

J.~Bourgain and E.~Fuchs. \newblock A proof of the positive density conjecture for integer {A}pollonian circle packings, 2010. \newblock Preprint, {\tt arXiv:1001.3894}.

- `section:1` (background; source_audit_annotation): Finally Bourgain and Fuchs \cite{BourgainFuchs2010} settled the so-called ``Positive Density Conjecture,'' that
$$
\#(\sB\cap[1,N])\gg N.
$$

Candidate references: `section:1` (external_reference).

### [BG08a] BourgainGamburd2008a — `external:BourgainGamburd2008a`

Source lines 5958–5963.

Jean Bourgain and Alex Gamburd. \newblock Expansion and random walks in {${\rm SL}_d(\Bbb Z/p^n\Bbb Z)$}. {I}. \newblock {\em J. Eur. Math. Soc. (JEMS)}, 10(4):987--1011, 2008.


Candidate references: `section:10` (external_reference).

### [BG08b] BourgainGamburd2008 — `external:BourgainGamburd2008`

Source lines 5963–5969.

Jean Bourgain and Alex Gamburd. \newblock Uniform expansion bounds for {C}ayley graphs of {${\rm SL}_2(\Bbb F_p)$}. \newblock {\em Ann. of Math. (2)}, 167(2):625--642, 2008.


Candidate references: `section:10` (external_reference).

### [BG09] BourgainGamburd2009 — `external:BourgainGamburd2009`

Source lines 5969–5975.

Jean Bourgain and Alex Gamburd. \newblock Expansion and random walks in {${\rm SL}_d(\Bbb Z/p^n\Bbb Z)$}. {II}. \newblock {\em J. Eur. Math. Soc. (JEMS)}, 11(5):1057--1103, 2009. \newblock With an appendix by Bourgain.


Candidate references: `lem:spec3` (external_reference); `section:10` (external_reference).

### [BGS10] BourgainGamburdSarnak2010 — `external:BourgainGamburdSarnak2010`

Source lines 5975–5980.

Jean Bourgain, Alex Gamburd, and Peter Sarnak. \newblock Affine linear sieve, expanders, and sum-product. \newblock {\em Invent. Math.}, 179(3):559--644, 2010.


Candidate references: `section:10` (external_reference).

### [BGS11] BourgainGamburdSarnak2011 — `external:BourgainGamburdSarnak2011`

Source lines 5980–5985.

J.~Bourgain, A.~Gamburd, and P.~Sarnak. \newblock Generalization of {S}elberg's 3/16th theorem and affine sieve. \newblock {\em Acta Math}, 207:255--290, 2011.


Candidate references: `section:10` (external_reference).

### [BGT11] BreuillardGreenTao2011 — `external:BreuillardGreenTao2011`

Source lines 5985–5990.

Emmanuel Breuillard, Ben Green, and Terence Tao. \newblock Approximate subgroups of linear groups. \newblock {\em Geom. Funct. Anal.}, 21(4):774--819, 2011.


Candidate references: `section:10` (external_reference).

### [BK10] BourgainKontorovich2010 — `external:BourgainKontorovich2010`

Source lines 5990–5996.

J.~Bourgain and A.~Kontorovich. \newblock On representations of integers in thin subgroups of {SL}$(2,{{\bf {Z}}})$. \newblock {\em GAFA}, 20(5):1144--1174, 2010.


Candidate references: `sec:outline` (external_reference); `thm:cMNis` (external_reference).

### [BK11] BourgainKontorovich2011a — `external:BourgainKontorovich2011a`

Source lines 5996–6001.

J.~Bourgain and A.~Kontorovich. \newblock On {Z}aremba's conjecture, 2011. \newblock Preprint, {\tt arXiv:1107.3776}.


Candidate references: `sec:outline` (external_reference).

### [BKS10] BourgainKontorovichSarnak2010 — `external:BourgainKontorovichSarnak2010`

Source lines 6001–6006.

J.~Bourgain, A.~Kontorovich, and P.~Sarnak. \newblock Sector estimates for hyperbolic isometries. \newblock {\em GAFA}, 20(5):1175--1200, 2010.


Candidate references: `sec:preII` (external_reference); `sec:lems` (external_reference); `lem:spec1` (external_reference); `lem:spec2` (external_reference).

### [Bou12] Bourgain2012 — `external:Bourgain2012`

Source lines 6006–6011.

J.~Bourgain. \newblock Integral {A}pollonian circle packings and prime curvatures. \newblock {\em J. Anal. Math.}, 118(1):221--249, 2012.


Candidate references: `section:1` (external_reference).

### [Bro86] Brooks1986 — `external:Brooks1986`

Source lines 6011–6016.

R.~Brooks. \newblock The spectral geometry of a tower of coverings. \newblock {\em J. Differential Geom.}, 23(1):97--107, 1986.


Candidate references: `section:10` (external_reference).

### [Bro07] Brooks2007 — `external:Brooks2007`

Source lines 6016–6022.

R.~Brooks. \newblock The spectral geometry of {R}iemannian surfaces. \newblock In {\em Topology in molecular biology, ed. M. I. Monastyrsky}. Springer, 2007.


Candidate references: `section:10` (external_reference).

### [Bur86a] Burger1986 — `external:Burger1986`

Source lines 6022–6028.

Marc Burger. \newblock Grandes valeurs propres du laplacien et graphes. \newblock In {\em S\'eminaire de {T}h\'eorie {S}pectrale et {G}\'eom\'etrie, {N}o.\ 4, {A}nn\'ee 1985--1986}, pages 95--100. Univ. Grenoble I, 1986.


Candidate references: `section:10` (external_reference).

### [Bur86b] BurgerThesis — `external:BurgerThesis`

Source lines 6028–6033.

Marc Burger. \newblock {\em Petites valeurs propres du laplacien et topologie de {F}ell}. \newblock PhD thesis, EPFL, 1986.


Candidate references: `section:10` (external_reference).

### [Bur88] Burger1988 — `external:Burger1988`

Source lines 6033–6038.

Marc Burger. \newblock Spectre du laplacien, graphes et topologie de {F}ell. \newblock {\em Comment. Math. Helv.}, 63(2):226--252, 1988.


Candidate references: `section:10` (external_reference).

### [BV11] BourgainVarju2011 — `external:BourgainVarju2011`

Source lines 6038–6043.

J.~Bourgain and P.~Varj{\'u}. \newblock Expansion in ${SL}\sb n(\bold {Z}/q \bold {Z})$, $q$ arbitrary, 2011. \newblock To appear, {\it Invent. Math.} {\tt arXiv:1006.3365v1}.


Candidate references: `section:10` (external_reference).

### [BY91] BerensteinYger1991 — `external:BerensteinYger1991`

Source lines 6043–6048.

Carlos~A. Berenstein and Alain Yger. \newblock Effective {B}ezout identities in {${\bf Q}[z_1,\cdots,z_n]$}. \newblock {\em Acta Math.}, 166(1-2):69--120, 1991.


Candidate references: `lem:spec3` (external_reference).

### [CHH88] CowlingHaagerupHowe1988 — `external:CowlingHaagerupHowe1988`

Source lines 6048–6053.

M.~Cowling, U.~Haagerup, and R.~Howe. \newblock Almost {$L\sp 2$} matrix coefficients. \newblock {\em J. Reine Angew. Math.}, 387:97--110, 1988.


Candidate references: `sec:preII` (external_reference).

### [DSC93] DiaconisSaloffCoste1993 — `external:DiaconisSaloffCoste1993`

Source lines 6053–6058.

P.~Diaconis and L.~Saloff-Coste. \newblock Comparison techniques for random walk on finite groups. \newblock {\em Ann. Probab.}, 21(4):2131--2156, 1993.


Candidate references: `section:10` (external_reference).

### [FS11] FuchsSanden2011 — `external:FuchsSanden2011`

Source lines 6058–6063.

Elena Fuchs and Katherine Sanden. \newblock Some experiments with integral {A}pollonian circle packings. \newblock {\em Exp. Math.}, 20(4):380--399, 2011.


Candidate references: `section:1` (external_reference).

### [Fuc10] FuchsThesis — `external:FuchsThesis`

Source lines 6063–6068.

E.~Fuchs. \newblock Arithmetic properties of {A}pollonian circle packings, 2010. \newblock Princeton University Thesis.


Candidate references: `section:1` (external_reference); `sec:prelim` (external_reference); `lem:line:1307` (external_reference); `lem:GGq` (external_reference).

### [GGPS66] GelfandGraevPS1966 — `external:GelfandGraevPS1966`

Source lines 6068–6073.

I.~M. Gelfand, M.~I. Graev, and I.~I. Pjateckii-Shapiro. \newblock {\em Teoriya predstavlenii i avtomorfnye funktsii}. \newblock Generalized functions, No. 6. Izdat. ``Nauka'', Moscow, 1966.


Candidate references: `sec:preII` (external_reference).

### [GLM{\etalchar{+}}03] GrahamLagarias2003 — `external:GrahamLagarias2003`

Source lines 6073–6079.

Ronald~L. Graham, Jeffrey~C. Lagarias, Colin~L. Mallows, Allan~R. Wilks, and Catherine~H. Yan. \newblock Apollonian circle packings: number theory. \newblock {\em J. Number Theory}, 100(1):1--45, 2003.


Candidate references: `section:1` (external_reference); `sec:prelim` (external_reference).

### [GLM{\etalchar{+}}05] GrahamLagariasMallowsWilksYanI — `external:GrahamLagariasMallowsWilksYanI`

Source lines 6079–6086.

Ronald~L. Graham, Jeffrey~C. Lagarias, Colin~L. Mallows, Allan~R. Wilks, and Catherine~H. Yan. \newblock Apollonian circle packings: geometry and group theory. {I}. {T}he {A}pollonian group. \newblock {\em Discrete Comput. Geom.}, 34(4):547--585, 2005.


Candidate references: `lem:line:1307` (external_reference).

### [Goo83] GoodBook — `external:GoodBook`

Source lines 6086–6092.

Anton Good. \newblock {\em Local analysis of {S}elberg's trace formula}, volume 1040 of {\em Lecture Notes in Mathematics}. \newblock Springer-Verlag, Berlin, 1983.


Candidate references: `sec:preII` (external_reference).

### [Hel08] Helfgott2008 — `external:Helfgott2008`

Source lines 6092–6097.

H.~A. Helfgott. \newblock Growth and generation in {${\rm SL}_2(\Bbb Z/p\Bbb Z)$}. \newblock {\em Ann. of Math. (2)}, 167(2):601--623, 2008.


Candidate references: `section:10` (external_reference).

### [Her26] Hermann1926 — `external:Hermann1926`

Source lines 6097–6103.

Grete Hermann. \newblock Die {F}rage der endlich vielen {S}chritte in der {T}heorie der {P}olynomideale. \newblock {\em Math. Ann.}, 95(1):736--788, 1926.


Candidate references: `lem:spec3` (external_reference).

### [IK04] IwaniecKowalski — `external:IwaniecKowalski`

Source lines 6103–6109.

Henryk Iwaniec and Emmanuel Kowalski. \newblock {\em Analytic number theory}, volume~53 of {\em American Mathematical Society Colloquium Publications}. \newblock American Mathematical Society, Providence, RI, 2004.


Candidate references: `sec:lems` (external_reference); `rmk:line:2712` (external_reference); `eq:hatRfuBnd` (external_reference).

### [KLN06] KLN2006 — `external:KLN2006`

Source lines 6109–6114.

Martin Kassabov, Alexander Lubotzky, and Nikolay Nikolov. \newblock Finite simple groups as expanders. \newblock {\em Proc. Natl. Acad. Sci. USA}, 103(16):6116--6119, 2006.


Candidate references: `section:10` (external_reference).

### [Klo27] Kloosterman1927 — `external:Kloosterman1927`

Source lines 6114–6119.

H.~D. Kloosterman. \newblock On the representation of numbers in the form {$ax^2+by^2+cz^2+dt^2$}. \newblock {\em Acta Math.}, 49(3-4):407--464, 1927.


Candidate references: `rmk:line:3068` (external_reference).

### [KO11] KontorovichOh2011 — `external:KontorovichOh2011`

Source lines 6119–6126.

A.~Kontorovich and H.~Oh. \newblock Apollonian circle packings and closed horospheres on hyperbolic 3-manifolds. \newblock {\em Journal of the American Mathematical Society}, 24(3):603--648, 2011.


Candidate references: `section:1` (external_reference); `eq:decayMtrx` (external_reference).

### [LMW02] LagariasMallowsWilks2002 — `external:LagariasMallowsWilks2002`

Source lines 6126–6131.

Jeffrey~C. Lagarias, Colin~L. Mallows, and Allan~R. Wilks. \newblock Beyond the {D}escartes circle theorem. \newblock {\em Amer. Math. Monthly}, 109(4):338--361, 2002.


Candidate references: `section:1` (external_reference).

### [LP82] LaxPhillips1982 — `external:LaxPhillips1982`

Source lines 6131–6137.

P.D. Lax and R.S. Phillips. \newblock The asymptotic distribution of lattice points in {E}uclidean and non-{E}uclidean space. \newblock {\em Journal of Functional Analysis}, 46:280--350, 1982.


Candidate references: `sec:outline` (external_reference); `sec:preII` (external_reference); `sec:lems` (external_reference); `lem:spec3` (external_reference).

### [MVW84] MatthewsVasersteinWeisfeiler1984 — `external:MatthewsVasersteinWeisfeiler1984`

Source lines 6137–6142.

C.~Matthews, L.~Vaserstein, and B.~Weisfeiler. \newblock Congruence properties of {Z}ariski-dense subgroups. \newblock {\em Proc. London Math. Soc}, 48:514--532, 1984.


Candidate references: `sec:prelim` (external_reference).

### [MW83] MasserWustholz1983 — `external:MasserWustholz1983`

Source lines 6142–6148.

D.~W. Masser and G.~W{\"u}stholz. \newblock Fields of large transcendence degree generated by values of elliptic functions. \newblock {\em Invent. Math.}, 72(3):407--464, 1983.


Candidate references: `lem:spec3` (external_reference).

### [Pat76] Patterson1976 — `external:Patterson1976`

Source lines 6148–6153.

S.J. Patterson. \newblock The limit set of a {F}uchsian group. \newblock {\em Acta Mathematica}, 136:241--273, 1976.


Candidate references: `sec:preII` (external_reference).

### [PS10] PyberSzabo2010 — `external:PyberSzabo2010`

Source lines 6153–6158.

L.~Pyber and E.~Szabo. \newblock Growth in finite simple groups of lie type of bounded rank, 2010. \newblock Preprint {\tt arXiv:1005.1858}.


Candidate references: `section:10` (external_reference).

### [Sar90] Sarnak1990 — `external:Sarnak1990`

Source lines 6158–6164.

Peter Sarnak. \newblock {\em Some applications of modular forms}, volume~99 of {\em Cambridge Tracts in Mathematics}. \newblock Cambridge University Press, Cambridge, 1990.


Candidate references: `section:10` (external_reference).

### [Sar07] SarnakToLagarias — `external:SarnakToLagarias`

Source lines 6164–6169.

P.~Sarnak. \newblock Letter to {J}. {L}agarias, 2007. \newblock \url{http://web.math.princeton.edu/sarnak/AppolonianPackings.pdf}.


Candidate references: `section:1` (external_reference); `sec:prelim` (external_reference); `eq:vgIs` (external_reference); `section:10` (external_reference).

### [Sar11] Sarnak2011 — `external:Sarnak2011`

Source lines 6169–6174.

Peter Sarnak. \newblock Integral {A}pollonian packings. \newblock {\em Amer. Math. Monthly}, 118(4):291--306, 2011.


Candidate references: `section:1` (external_reference).

### [Sel65] Selberg1965 — `external:Selberg1965`

Source lines 6174–6179.

A.~Selberg. \newblock On the estimation of {F}ourier coefficients of modular forms. \newblock {\em Proc. of Symposia in Pure Math.}, VII:1--15, 1965.


Candidate references: `section:10` (external_reference).

### [SGV11] SalehiVarju2011 — `external:SalehiVarju2011`

Source lines 6179–6184.

A.~Salehi~Golsefidy and P.~Varj{\'u}. \newblock Expansion in perfect groups, 2011. \newblock Preprint.


Candidate references: `section:10` (external_reference).

### [Sha99] Shalom1999 — `external:Shalom1999`

Source lines 6184–6189.

Yehuda Shalom. \newblock Bounded generation and {K}azhdan's property ({T}). \newblock {\em Inst. Hautes \'Etudes Sci. Publ. Math.}, 90:145--168, 1999.


Candidate references: `section:10` (external_reference).

### [Sod37] Soddy1937 — `external:Soddy1937`

Source lines 6189–6194.

F.~Soddy. \newblock The bowl of integers and the hexlet. \newblock {\em Nature}, 139:77--79, 1937.


Candidate references: `section:1` (external_reference).

### [Sul84] Sullivan1984 — `external:Sullivan1984`

Source lines 6194–6200.

D.~Sullivan. \newblock Entropy, {H}ausdorff measures old and new, and limit sets of geometrically finite {K}leinian groups. \newblock {\em Acta Math.}, 153(3-4):259--277, 1984.


Candidate references: `sec:preII` (external_reference).

### [Var12] Varju2012 — `external:Varju2012`

Source lines 6200–6205.

P{\'e}ter~P. Varj{\'u}. \newblock Expansion in {$SL_d(O_K/I)$}, {$I$} square-free. \newblock {\em J. Eur. Math. Soc. (JEMS)}, 14(1):273--305, 2012.


Candidate references: `section:10` (external_reference).

### [Vin13] Vinogradov2013 — `external:Vinogradov2013`

Source lines 6205–6212.

I.~Vinogradov. \newblock Effective bisector estimate with application to {A}pollonian circle packings. \newblock {\em IMRN}, 2013. \newblock Princeton University Thesis 2012, {\tt arxiv:1204.5498v1}.


Candidate references: `section:1` (external_reference); `sec:preII` (external_reference); `thm:Vin` (external_reference).

## Coverage and limits

{"mode": "native_latex_index", "claims": 46, "sections": 10, "external_references": 49, "source_bibliography_entries": 49, "unresolved_bibliography": 0, "unresolved": 0, "numbering": "Native labels, not reconstructed printed numbers."}

- Reference edges are not certified proof dependencies. Edge direction is prerequisite → consumer.
- Numbers reflect simple source counters; labels and line anchors are authoritative.
- Extractive statements and proof openings are marked; they are not reconstructed proof gists.
- Macros, included files and custom counters require an expanded source or annotated fallback.
- 20 October 2026: one source-supported prerequisite-to-consumer edge identifies the internal lifting Claim used by lem:spec3. This is an incomplete argument map; adjudications and later repair details are restricted to the panel view.