{"dependency_proposals": [{"explanation": "Theorem thm:RNU is the main circle-method input explicitly assumed in the proof of Theorem thm:Main.", "label": "thm:RNU", "role": "proof_input", "source_quote": "\\begin{proof}[Proof of Theorem \\ref{thm:Main} assuming Theorem \\ref{thm:RNU}:]"}, {"explanation": "Equations eq:cRNis and eq:cRNhatUis define the representation functions \\cR_N(n) and \\cR_N^U(n) compared in the proof of Theorem thm:Main.", "label": "eq:cRNis", "role": "proof_input", "source_quote": "Our main object of study is then the representation number\n\\be\\label{eq:cRNis}\n\\cR_{N}(n):=\\sum_{\\ff\\in\\fF_{T}}\\sum_{(2x,y)=1}\n\\gU\\left(\\frac {2x}X\\right)\n\\gU\\left(\\frac yX\\right)\n\\bo_{\\{n=\\ff(2x,y)\\}}\n,\\ee"}, {"explanation": "Section references in the 'Plan for the Paper' subsection and forward references in the informal outline of Section 3 are narrative signposts rather than premises used in the local deduction of Theorem thm:Main from Theorem thm:RNU.", "label": "narrative:47002", "role": "background", "source_quote": "A more detailed outline of the proof, as well as the setup of some relevant exponential sums, is given in \\S\\ref{sec:outline}. Before we can do this, we need to recall the Apollonian group"}], "findings": [{"explanation": "Theorem thm:RNU states the lower bound \\fS(n) \\gg_\\vep N^{-\\vep} and the exceptional-set estimate eq:RNUbnd for the dyadic range \\frac{1}{2}N < n < N, whereas the proof of Theorem thm:Main defines Z and W for all admissible n < N. This is harmless because restricting Z and W to (\\frac{1}{2}N, N) bounds the number of exceptions in (\\frac{1}{2}N, N) by O(N^{1-\\eta'}), and summing over dyadic intervals yields the bound for all n < N.", "kind": "context", "source_quote": "Now let $Z$ be the ``exceptional'' set of admissible $n<N$ for which $\\cR_{N}(n)=0$. Futhermore, let $W$ be the set of admissible $n<N$ for which \\eqref{eq:RNUbnd} is satisfied."}, {"explanation": "Theorem thm:Main asserts that \\eta > 0 is effectively computable. In the local reduction, the resulting exponent is \\min(\\eta, \\fu - \\vep), where \\eta comes from Theorem thm:RNU and \\fu comes from eq:Uis (defined via eq:fuIs in terms of the spectral gap parameters \\gd - \\gT_1 and \\eta_0). Thus, the effective computability of \\eta in Theorem thm:Main is conditional on the effective computability of the constants in Theorem thm:RNU and Lemma lem:spec3.", "kind": "unverified", "source_quote": "Quantitatively, the number of exceptions up to $N$ is bounded by\n $O(N^{1-\\eta})$, where $\\eta>0$ is effectively computable."}, {"explanation": "Because the indexed source_slice spans from the statement of Theorem thm:Main in Section 1 through its proof at the end of Section 3, many attached dependency edges come from historical survey prose (e.g., eq:GLbnd, eq:SarBnd, fig1, fig2), the 'Plan for the Paper' overview (narrative:47002, narrative:55546, narrative:93454, narrative:99181, narrative:115416), or forward pointers to where parameters are later used (eq:gS2p, eq:gS12p, eq:cJfbnd, eq:ACisT, lem:spec3, eq:cCis). The actual local proof of Theorem thm:Main in Section 3.2 only uses Theorem thm:RNU (with eq:RNUbnd) and the Section 3.1 setup (eq:TXNis, eq:TT1T2, eq:fFdef, eq:fFTbnd, eq:ffToInProd, eq:binQuad, eq:Uis).", "kind": "map_correction", "source_quote": "A more detailed outline of the proof, as well as the setup of some relevant exponential sums, is given in \\S\\ref{sec:outline}. Before we can do this, we need to recall the Apollonian group"}], "missing_context": ["Introductory definitions (lines 502-572, omitted_context) defining the integral Apollonian gasket \\sG, its curvature set \\sB, and the admissible set \\sA prior to the statement of Theorem thm:Main.", "Proofs and effectivity of the constants in the premises Theorem thm:RNU and eq:Uis / eq:fuIs (which depend on the spectral gap inputs in later sections)."], "proof_status": "locally_supported", "summary": "Conditional on Theorem thm:RNU and the setup bounds in Section 3.1 (specifically eq:TXNis, eq:fFTbnd, eq:Uis, and the curvature parameterization via eq:binQuad and eq:ffToInProd), the local deduction of Theorem thm:Main at the end of Section 3.2 is sound. Using #\\fF_T \\ll T^\\gd (eq:fFTbnd) and switching the order of summation in the tail u \\ge U of the M\u00f6bius inversion formula, the proof establishes the \\ell^1 bound \\sum_{n<N} |\\cR_N(n) - \\cR_N^U(n)| \\ll T^\\gd X^2 / U. Combining this with the lower bound \\cR_N^U(n) \\gg_\\vep T^{\\gd-1} N^{-\\vep} on the non-exceptional admissible set W from Theorem thm:RNU and the relation TX^2 = N (eq:TXNis) bounds the number of admissible exceptions in (\\frac{1}{2}N, N) by O_\\vep(N^{1-\\eta} + N^{1+\\vep}/U), which gives a power savings since U = N^\\fu with \\fu > 0 (eq:Uis). A standard dyadic summation over intervals (\\frac{1}{2}N, N) completes the bound up to N; the claim that \\eta > 0 is effectively computable remains conditional on the effectivity of the spectral-gap constants underlying Theorem thm:RNU and eq:Uis.", "target_id": "thm:Main", "used_dependencies": ["eq:RNUbnd", "eq:TT1T2", "eq:TXNis", "eq:Uis", "eq:binQuad", "eq:fFTbnd", "eq:fFdef", "eq:ffToInProd", "eq:totMass", "lem:GGq", "thm:RNU"]}