{
  "case_id": "case-1626c7160100050229a7351c",
  "target_id": "lem:spec0",
  "original_proof_status": "defective",
  "statement_status": "unresolved",
  "statement_argument": "",
  "summary": "The frozen sketch does not establish uniformity in gamma_1: its smoothing comparison inserts an uncontrolled conjugation, and its stated Sobolev estimate does not control the translated vector uniformly. These are defects in the displayed argument, not counterexamples to the lemma. The full source supplies context supporting the finite-cover normalization; the final optimization is correct conditionally. The precise effective counting input remains unverified. No conclusion is propagated to downstream claims or the whole paper.",
  "chronology_note": "The recorded received-date evidence fixes the cutoff at 2012-05-24. The full bibliography supplies pre-cutoff publication years for Lax–Phillips, Bourgain–Kontorovich–Sarnak, and Kontorovich–Oh; in particular, Kontorovich–Oh is not identified merely by a citation key. Bibliographic availability does not verify an external theorem's text or applicability. The local error checks below require no later result. Model weights may contain later knowledge, but no such knowledge is used as historical evidence. No author response or separately labelled later edition was supplied.",
  "external_results": [
    {
      "role": "proof_input",
      "imported_result": "The Lax–Phillips input needed at eq:reg3Lem is an effective count for the specified SO_F norm balls, sufficient to yield O(eta Y^delta + Y^(delta-epsilon)) for their relative-width eta shells. The exact external theorem and its norm hypotheses are absent; this input remains unverified.",
      "available_from": "1982, according to the supplied journal citation",
      "date_evidence": "The bibliography identifies Lax–Phillips, Journal of Functional Analysis 46:280–350, 1982.",
      "date_basis": "Publication year in the supplied bibliography",
      "version": "Cited 1982 journal article; relevant theorem text not supplied",
      "finding_ids": [
        "finding-780309607bd9c1a5da36"
      ]
    },
    {
      "role": "proof_input",
      "imported_result": "Kontorovich–Oh Proposition 5.3, as restated in the manuscript: for G=SL_2(C), Theta>1, a unitary representation weakly containing no complementary series with parameter s>Theta, and smooth v,w, the coefficient is bounded by ||g||_F^(-2(2-Theta)) S(v)S(w), with the displayed second-order K-Sobolev norm. The originating proposition is uninspected; the local assessment checks the manuscript's application of its stated formula.",
      "available_from": "2011, according to the supplied journal citation",
      "date_evidence": "The bibliography identifies Kontorovich–Oh, Journal of the American Mathematical Society 24(3):603–648, 2011.",
      "date_basis": "Publication year in the supplied bibliography",
      "version": "Cited 2011 journal article, Proposition 5.3; manuscript restatement supplied",
      "finding_ids": [
        "finding-63f9c28e0b369f4d3b2f",
        "finding-780309607bd9c1a5da36"
      ]
    },
    {
      "role": "background",
      "imported_result": "Bourgain–Kontorovich–Sarnak Lemma 3.7 and Proposition 4.18 are cited for unfolding and level-one comparison. Their texts and hypotheses are not supplied, and no conclusion from them is imported to certify uniformity here.",
      "available_from": "2010, according to the supplied journal citation",
      "date_evidence": "The bibliography identifies Sector estimates for hyperbolic isometries, GAFA 20(5):1175–1200, 2010.",
      "date_basis": "Publication year in the supplied bibliography",
      "version": "Cited 2010 journal article; external lemma and proposition uninspected",
      "finding_ids": [
        "finding-be148e2c35505436dde0",
        "finding-6f2f20dcc9484a453169"
      ]
    }
  ],
  "decisions": [
    {
      "finding_id": "finding-be148e2c35505436dde0",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "In the range\n\\be\\label{eq:reg2Lem}\n\\|\\g_{1}\\g\\|<Y(1-10\\eta),\n\\ee\nboth $f(\\g_{1}g^{-1}\\g h)$ and $f(\\g_{1}\\g)$ are $1$, so their difference vanishes.",
      "reasoning": "Writing k=gamma_1 gamma gives gamma_1 g^{-1} gamma h=(gamma_1 g^{-1} gamma_1^{-1})kh. Smallness of g does not uniformly control this conjugated factor. This fails within the supplied group: take gamma_1=C_1^n, gamma=C_1^{-n}, h=e, and g a small opposite unipotent in the displayed J rho(SL_2) subgroup. Conjugation is unbounded as n grows; in the two-dimensional model an off-diagonal entry has magnitude 4n^2|t| for a fixed small unipotent parameter t. Thus the unperturbed product is e while the perturbed norm can exceed Y. The asserted inner-range vanishing, and hence the reduction of smoothing error to the stated shell, is false uniformly.",
      "hypothesis_check": "There is no bound on gamma_1. The displayed formula for C_1^n shows that taking n divisible by q puts gamma_1 and its inverse in Gamma(q), so the example can also lie in the original subgroup sum. Reindexing the enlarged Gamma sum does not remove conjugation.",
      "affected_claims": [
        "lem:spec0"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied."
    },
    {
      "finding_id": "finding-63f9c28e0b369f4d3b2f",
      "outcome": "confirmed_error",
      "severity": "substantive",
      "source_quote": "The functions $\\psi$ are bump functions in six real dimensions, so can be chosen to have second-order Sobolev norms bounded by $\\ll \\eta^{-5}$.",
      "reasoning": "The quoted scaling is correct for an unshifted unit-mass six-dimensional bump. It does not supply the bound required for the actual second vector Psi_{q,gamma_1}=R(gamma_1)Psi_q. For the manuscript's right regular action, dπ(X)R(a)=R(a)dπ(Ad(a^{-1})X). Therefore derivatives of the translated vector acquire adjoint coefficients depending on gamma_1. Unitarity controls its L2 norm, not these derivative norms. Consequently the offered Sobolev argument does not establish the uniform eta^{-10} remainder. This does not rule out obtaining that remainder by a different argument.",
      "hypothesis_check": "Contrary to the review's missing-context list, the full source explicitly defines the Sobolev norm using first and second derivatives in Lie(K). This norm is not invariant under arbitrary right translation by Gamma, and gamma_1 is not restricted to K or an adjoint-bounded set.",
      "affected_claims": [
        "lem:spec0"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied."
    },
    {
      "finding_id": "finding-6f2f20dcc9484a453169",
      "outcome": "packet_context",
      "severity": "none",
      "source_quote": "Of course the projection onto the base representation is just $[\\G:\\tilde\\G(q)]^{-1}$ times the same projection at level one, cf. \\eqref{eq:gl0Qgl0}.",
      "reasoning": "Equality of lowest eigenvalues alone would not suffice, but it is not the full supplied premise. Equations eq:gls and eq:glQs distinguish the base eigenvalue strictly from the next one, and eq:RepDecomp supplies a single base irreducible, with an analogous decomposition at principal levels. For H=tildeGamma(q), lifting into the principal cover leaves room for only that base representation, while the level-one lift already supplies it. If d=[Gamma:H], normalized pullback is d^{-1/2} times pullback. Unfolding the bump pairing gives a factor d^{-1/2} for each vector, hence d^{-1} for the base matrix coefficient, including the translated vector. This checks the implication from the source's stated spectral premises, not those premises independently.",
      "hypothesis_check": "H has finite index and lies between Gamma(q) and Gamma. Covering-space inclusion also passes the stated spectral exclusion to H; normality is unnecessary. The comparison retains the same translation at level one, whose unsmoothed count equals N_1 because gamma_1 belongs to Gamma.",
      "affected_claims": [
        "lem:spec0"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied."
    },
    {
      "finding_id": "finding-780309607bd9c1a5da36",
      "outcome": "unresolved",
      "severity": "substantive",
      "source_quote": "apply \\cite{LaxPhillips1982}, bounding the count by\n\\be\\label{eq:reg3Lem}\n\\ll Y^{\\gd}\\eta + Y^{\\gd-\\vep},\n\\ee\nwhere $\\vep>0$ depends on the spectral gap for $\\G$.",
      "reasoning": "The exact external result yielding this effective shell estimate is not supplied, so its applicability cannot be certified. However, the objection overstates the missing context: the same frozen source gives the spin map and explicitly records the quadratic norm comparison in eq:gToIg. Its Cartan coordinates and Frobenius convention are also present. Norm comparability supports the exponent conversion but does not, by itself, prove a relative-width eta shell estimate. The necessary effective counting theorem and integrated mixing estimate remain substantive verification dependencies, not demonstrated false statements.",
      "hypothesis_check": "The source states geometric finiteness, infinite covolume, and delta>1 for the Apollonian group. What remains unverified is the quantitative theorem for the actual norm balls and the asserted integrated bound—not the absence of these geometric hypotheses. No alternative proof or repair search is undertaken.",
      "affected_claims": [
        "lem:spec0"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied."
    },
    {
      "finding_id": "finding-bff5861e48ae6665a78d",
      "outcome": "packet_context",
      "severity": "none",
      "source_quote": "Optimizing $\\eta$ and renaming $\\gT_{0}<\\gd$ in terms of the spectral gap $\\vep$ gives the claim.",
      "reasoning": "This is a correct conditional observation, not an additional defect. Taking eta=Y^{-epsilon/11} makes eta Y^delta and Y^(delta-epsilon) eta^{-10} both equal Y^(delta-epsilon/11); the remaining Y^(delta-epsilon) term is smaller. Thus Theta_0=delta-epsilon/11 works if eq:NqErr has the asserted uniform constants. This calculation cannot supply the missing uniformity in the preceding steps.",
      "hypothesis_check": "Epsilon is positive and fixed by the spectral input. The chosen eta tends to zero, as required for smoothing. Uniformity must already hold before this optimization.",
      "affected_claims": [
        "lem:spec0"
      ],
      "revised_status": "not_checked",
      "revised_quote": "",
      "revised_reasoning": "No later edition was supplied."
    }
  ]
}