{
  "case_id": "case-7bcd03f1ff7867735a8684d3",
  "target_id": "lem:spec3",
  "original_proof_status": "defective",
  "statement_status": "unresolved",
  "statement_argument": "The displayed proof of Lemma lem:spec3 fails because it misidentifies the index of the vector stabilizer modulo q as order q^2 instead of q^3 and undercounts the congruence fiber in both Case 1 and Case 2, causing the spectral error term to be too large in the stated parameter ranges. In addition, the unimodular coordinate change in Case 2 lacks height control and the reuse of Case 1 for the lifted vector v_* lacks a uniform orbit/fiber bound for general nonzero vectors modulo q_0. Because fixing these issues would require altering the Case 1/Case 2 cutoff exponent, adjusting the constant C in the lemma statement or choosing smaller q_0, supplying height-controlled coordinates, and verifying uninspected external inputs, the status of the lemma statement as formulated remains unresolved within the supplied packet.",
  "summary": "The proof of Lemma lem:spec3 is defective. First, conditional on the congruence quotient description eq:Fuc (Lemma lem:GGq), the orbit of a primitive null vector v_0 modulo a prime p>=5 under SO_F(F_p) lies on the 3-dimensional affine null cone and has cardinality of order p^3, whereas eq:G0qBnd asserts [Gamma : tilde{Gamma}(q)] asymp q^2 (confusing the affine vector orbit with the 2-dimensional projective quadric). Second, restricting one coordinate <e_1, gamma_1 gamma_2' v_0> equiv r (mod q) leaves a fiber of order q^2 cosets in Gamma/tilde{Gamma}(q) rather than O(q), so the spectral error term in Case 1 is O(T_1^delta q^2 T_2^{Theta_0}) instead of O(T_1^delta q T_2^{Theta_0}); this fails to save a power of q across the stated Case 1 range q < T_2^{(delta - Theta_0)/2}. Third, Case 2 reuses the same defective bound at a prime q_0 asymp T_1^{(delta - Theta_0)/2} for an arbitrary nonzero integer vector v_* (not necessarily on the null cone), where the error term again fails to save a power of q_0. Fourth, the linear change of variables used to assume (v_1, q) = 1 for composite q is not height-controlled, leaving the height bound <= log T_1 for the polynomials P_gamma unjustified.",
  "chronology_note": "The recorded review cutoff is the journal received date 2012-05-24 (Invent. Math., doi:10.1007/s00222-013-0475-y). All cited external references in Lemma lem:spec3 (Hermann 1926, Lax-Phillips 1982, Masser-Wustholz 1983, Berenstein-Yger 1991, Bourgain-Gamburd 2009, and Fuchs 2010) predate this cutoff. Our arbitration of the findings relies only on elementary finite-field and modular algebra together with the internal text of the manuscript; no post-cutoff results are used, though model weights cannot be stripped of later knowledge.",
  "external_results": [
    {
      "role": "proof_input",
      "imported_result": "Orbital counting bound #{gamma in Gamma : ||gamma|| < Y} << Y^delta for geometrically finite Kleinian groups with critical exponent delta > 1.",
      "available_from": "1982",
      "date_evidence": "Bibliography entry [LP82]: P. D. Lax and R. S. Phillips, Journal of Functional Analysis, 46:280-350, 1982.",
      "date_basis": "journal_publication",
      "version": "J. Funct. Anal. 46 (1982), 280-350",
      "finding_ids": [
        "finding-e20889d0f893f373cb31"
      ]
    },
    {
      "role": "proof_input",
      "imported_result": "Description of congruence quotients Gamma/Gamma(q) for the Apollonian group, specifically Gamma/Gamma(q) iso SO_F(Z/qZ) for (q,6)=1 (cited via Lemma lem:GGq / eq:Fuc).",
      "available_from": "2010",
      "date_evidence": "Bibliography entry [Fuc10]: E. Fuchs, Arithmetic properties of Apollonian circle packings, Princeton University Thesis, 2010.",
      "date_basis": "thesis_publication",
      "version": "Princeton University PhD Thesis, 2010",
      "finding_ids": [
        "finding-1e6b6475f3e54a2cc69d",
        "finding-e20889d0f893f373cb31",
        "finding-fbc15a63a1f198d2135d"
      ]
    },
    {
      "role": "proof_input",
      "imported_result": "Effective Nullstellensatz / Bezout height bound (Theorem IV of Masser-Wustholz 1983, based on Hermann 1926) bounding the denominator d and cofactor heights for a system of polynomials without common complex zeros.",
      "available_from": "1983",
      "date_evidence": "Bibliography entries [Her26] Math. Ann. 95(1):736-788, 1926 and [MW83] Invent. Math. 72(3):407-464, 1983.",
      "date_basis": "journal_publication",
      "version": "Invent. Math. 72(3) (1983), 407-464, Theorem IV",
      "finding_ids": [
        "finding-b50410999141a2199ffd",
        "finding-fd0b1e0a60459ec7f586"
      ]
    },
    {
      "role": "background",
      "imported_result": "Related Nullstellensatz lifting argument in Prop. 4.1 of Bourgain-Gamburd 2009.",
      "available_from": "2009",
      "date_evidence": "Bibliography entry [BG09]: J. Eur. Math. Soc. (JEMS), 11(5):1057-1103, 2009.",
      "date_basis": "journal_publication",
      "version": "JEMS 11(5) (2009), 1057-1103",
      "finding_ids": [
        "finding-fd0b1e0a60459ec7f586"
      ]
    },
    {
      "role": "background",
      "imported_result": "Improved effective Bezout bounds (Theorem 5.1 of Berenstein-Yger 1991), cited only as a parenthetical remark.",
      "available_from": "1991",
      "date_evidence": "Bibliography entry [BY91]: Acta Math., 166(1-2):69-120, 1991.",
      "date_basis": "journal_publication",
      "version": "Acta Math. 166(1-2) (1991), 69-120",
      "finding_ids": [
        "finding-fd0b1e0a60459ec7f586"
      ]
    }
  ],
  "decisions": [
    {
      "finding_id": "finding-1e6b6475f3e54a2cc69d",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "[\\G:\\tilde\\G(q)]\\asymp q^{2}",
      "reasoning": "In eq:G0q, tilde{Gamma}(q) is defined as the stabilizer in Gamma of the vector v_0 (mod q), not of the projective line [v_0] (mod q). For a prime p >= 5 where v_0 notequiv 0 (mod p), the projective quadric {F(v) = 0} in P^3(F_p) has (p+1)^2 or p^2+1 points (order p^2), so the affine cone of nonzero null vectors in F_p^4 has (p-1)(p+1)^2 or (p-1)(p^2+1) points, which is of order p^3. Under the spin double cover iota: SL_2(Z[i]/(p)) -> SO_F(F_p) (Section 2.3 and Lemma lem:GGq), the group acts transitively on these nonzero null vectors (for instance, the stabilizer in SL_2(Z[i]/(p)) of a null vector has order p-1 or p+1 while |SL_2(Z[i]/(p))| = (p^2-1)^2 p^2 or (p^4-1)p^2, giving an orbit of size (p-1)(p+1)^2 or (p-1)(p^2+1) asymp p^3). Thus [Gamma : tilde{Gamma}(q)] is of order q^3 at prime moduli (and q^3 up to divisor factors in general), not q^2.",
      "hypothesis_check": "The root quadruple v_0 of a primitive integral Apollonian gasket is a primitive integer vector satisfying F(v_0) = 0, and Lemma lem:GGq (eq:Fuc) gives Gamma/Gamma(q) iso SO_F(Z/qZ) for (q,6)=1. Under these hypotheses, the stabilizer index of the vector v_0 (mod q) is not asymp q^2.",
      "affected_claims": [
        "lem:spec3"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied for comparison."
    },
    {
      "finding_id": "finding-e20889d0f893f373cb31",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "T_{1}^{\\gd}\\\nq\\\n\\left(\n\\frac1{q^{2}}\\\nT_{2}^{\\gd}\n+\nT_{2}^{\\gT_{0}}\n\\right)",
      "reasoning": "Because the vector orbit Gamma/tilde{Gamma}(q) v_0 (mod q) has size of order q^3 (at prime q=p) rather than q^2, imposing the single linear congruence <e_1, gamma_1 gamma_2' v_0> equiv r (mod q) restricts gamma_2' in Gamma/tilde{Gamma}(q) to a fiber of size order q^2 rather than O(q). Substituting the actual fiber size ~ q^2 and stabilizer index ~ q^3 into the Lemma lem:spec0 bound yields T_1^delta q^2 (q^{-3} T_2^delta + T_2^{Theta_0}) = q^{-1} T^delta + q^2 T_1^delta T_2^{Theta_0}. While the main term q^{-1} T^delta is unchanged because q^2/q^3 = 1/q, the spectral error term is q^2 T_1^delta T_2^{Theta_0} rather than q T_1^delta T_2^{Theta_0}. For q near the top of the advertised Case 1 range q < T_2^{(delta - Theta_0)/2}, we have q^2 T_2^{Theta_0} asymp T_2^delta, which fails to give any power saving in q (saving a full power 1/q requires q < T_2^{(delta - Theta_0)/3}). The exact same defect occurs in Case 2 when applying Case 1 to a prime q_0 asymp T_1^{(delta - Theta_0)/2}.",
      "hypothesis_check": "Checked against the hypotheses of Lemma lem:spec3, eq:lemRHS (Lemma lem:spec0), and the stated range eq:q1range (q < T_2^{(delta - Theta_0)/2}).",
      "affected_claims": [
        "lem:spec3"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied for comparison."
    },
    {
      "finding_id": "finding-b50410999141a2199ffd",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "Since $v$ is a primitive vector, after a linear change of variables we may assume that $(v_{1},q)=1$.",
      "reasoning": "For composite q, a primitive vector v = gamma_2 v_0 in Z^4 need not have any coordinate coprime to q (e.g., (2,3,0,0) mod 6), so a coordinate permutation does not suffice. While there exists a unimodular matrix U in SL_4(Z) such that (U v)_1 is coprime to q, replacing v by U v replaces gamma_1 by gamma_1 U^{-1}, which alters the coefficients of the linear polynomials P_gamma. The proof subsequently asserts without justification that the polynomials P_gamma have height <= log T_1 and uses this in eq:fdIs to deduce d << T_1^{10^{28}} < q. If U had entries of size comparable to q, the height of P_gamma would be at least log q and the Nullstellensatz bound d < q would fail; thus an explicit height bound on U (e.g., entries bounded by a small power of log q <= log N) is required for the proof step to hold.",
      "hypothesis_check": "The modulus q in Lemma lem:spec3 is an arbitrary integer 1 <= q < N, not restricted to primes, and v = gamma_2 v_0 is primitive since v_0 is primitive and gamma_2 in SL_4(Z).",
      "affected_claims": [
        "lem:spec3"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied for comparison."
    },
    {
      "finding_id": "finding-fbc15a63a1f198d2135d",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "such that $v_{*}\\not\\equiv0(\\mod q_{0})$",
      "reasoning": "Two prerequisites are omitted when reducing Case 2 to Case 1 modulo a prime q_0 asymp T_1^{(delta - Theta_0)/2}. First, the proof obtains v_*, z_* by clearing denominators from a rational solution v^* = (1, V_2^*, V_3^*, V_4^*), z^* = Z^* without specifying that the least common denominator is used (or that gcd(v_*) is divided out so that v_* is primitive and hence nonzero modulo every prime q_0). Second, and more substantively, v_* is an arbitrary nonzero integer vector solving the linear system <e_1, gamma v_*> = z_* for gamma in S and need not equal v_0 or even satisfy F(v_*) = 0. Applying the Case 1 argument to v_* modulo q_0 requires bounding the stabilizer index and hyperplane fiber size for an arbitrary nonzero vector v_* in F_{q_0}^4 (whether isotropic or non-isotropic for F), where the orbit under SO_F(F_{q_0}) again has order q_0^3 and the fiber has order q_0^2, invalidating the displayed bound q_0(q_0^{-2} T_1^delta + T_1^{Theta_0}) << q_0^{-1} T_1^delta at q_0 asymp T_1^{(delta - Theta_0)/2}.",
      "hypothesis_check": "The Claim in Case 2 guarantees only a nonzero integer vector v_* and integer z_* satisfying <e_1, gamma v_*> = z_* for gamma in S; it does not constrain F(v_*).",
      "affected_claims": [
        "lem:spec3"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied for comparison."
    },
    {
      "finding_id": "finding-fd0b1e0a60459ec7f586",
      "outcome": "packet_context",
      "severity": "none",
      "source_quote": "which is incompatible with \\eqref{eq:fdIs} and \\eqref{eq:qToT1}",
      "reasoning": "This finding records valid intermediate steps and context: conditional on the height bound for P_gamma and the effective Nullstellensatz estimate eq:fdIs, the arithmetic check 8^{4*2^{4-1}-1} = 8^{31} < 10^{28} holds, and the divisibility q | d with d >= 1 implies d >= q, which contradicts d << T_1^{10^{28}} and q >= T_1^{10^{29}} for large T_1. It also notes that converting a power saving in T_1 into a power saving in q < N relies on T = N^{1/100} from eq:TXNis.",
      "hypothesis_check": "Consistent with eq:TXNis, eq:TT1T2, eq:cCis, eq:qToT1, and eq:fdIs.",
      "affected_claims": [
        "lem:spec3"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied for comparison."
    }
  ]
}