Technical evidence and reproducible checks

This source-adjudicated account was first published 19 October 2026 and updated 20 October 2026. Native labels and expanded-source line ranges refer to the frozen arXiv v2 text. All three scripts use exact arithmetic. Finite checks establish their reported finite statements; uniform asymptotic claims require a separate argument.

20 October update: the coordinate-height issue and its repair

Kontorovich–Zhang's 2022 paper explicitly documents the matching issue in its §3.2, pp.14–15. Our original literature search missed that discussion. The reconciliation links the published version, checks the bounded-shear mechanism, and supplies a direct four-coordinate determinant proof of BK's lifting Claim for every sufficiently large modulus, including composites and prime powers. The remaining vector-orbit counts, spectral-error balances and analytic premises are not certified by that local repair.

Vector stabilizers and spectral balances

lem:spec3, expanded lines 2265–2307, defines a subgroup fixing $v_0$ modulo $q$, then writes $[\Gamma:\widetilde\Gamma(q)]\asymp q^2$ and an $O(q)$ fixed-coordinate fiber bound. At split primes, the Descartes form is equivalent to a determinant form. Nonzero null vectors correspond to rank-one matrices, numbering $(p-1)(p+1)^2$. The appendix generators give the requisite elementary matrices over $\mathbb F_p[i]$; the accepted Astra arbitration explains the generation and transitivity argument without importing Fuchs' theorem.

An orbit of order $p^3$ has a coordinate fiber of at least order $p^2$. Granting the analytic coset-counting input, the corrected small-modulus error has size $T_1^\delta p^2T_2^{\Theta_0}$, so one needs $p^3\lesssim T_2^{\delta-\Theta_0}$, rather than the printed quadratic cutoff. At the chosen large-modulus auxiliary prime $q_0\asymp T_1^{(\delta-\Theta_0)/2}$, the corresponding error reaches order $T_1^\delta$ and loses the claimed saving. These are defects in the supplied proof; modifying the cutoffs is not yet a verified repair.

The coordinate change sending a primitive vector to one with first coordinate 1 also changes the equation's row to $e_1^t\gamma U^{-1}$. The claimed coefficient heights require control of $U^{-1}$, which is not supplied. This diagnoses the original inference. The new local completion bypasses that coordinate change and proves the lifting Claim by a bounded-minor argument. Astra rejects a different prime-avoidance objection: an existing integral solution can be divided by its common gcd. It also confirms that the full source supplies the scale relation and other context missing from some packets.

Full Astra arbitration · Finite orbit checks · Orbit/group script.

Full special-orthogonal group

lem:GGq (2), lines 1324–1344, identifies the congruence image with full $\mathrm{SO}_F(\mathbb Z/q\mathbb Z)$ for $(q,6)=1$. Complete closure of the stated even-word generators modulo 7 has 58,800 elements and excludes $-I$. But $-I$ preserves the Descartes form and has determinant +1. Adjoining it gives 117,600 distinct determinant-one isometries, already enough to contradict equality with full SO. No classification formula for the full orthogonal group is required. A spin-image or bounded-index formulation is a repair lead whose uses remain to be checked.

This is an exact coordinating check. The assigned Gemini arbitration was rejected by the assessment validator and supplies no accepted decision on this target.

Pointwise smoothing cancellation

lem:spec0, lines 2138–2191, claims that small $g,h$ leave both indicators equal to one when $\|\gamma_1\gamma\|<Y(1-10\eta)$. The problem is conjugation by the unrestricted representative $\gamma_1$.

Set $U=S_1S_2$, $V=S_2S_3$, $A=U-I$, and

The script checks $A^3=0$, $g^tFg=F$, $\det g=1$, and $\|g-I\|^2<\eta^2$ for $\eta=1/100$. Take $Y=100$, $\gamma_1=V^{700}$, $\gamma=\gamma_1^{-1}$ and $h=I$. The lattice matrices are integral and $\gamma_1\equiv I\pmod7$. Although $\gamma_1\gamma=I$ has squared Frobenius norm 4, the perturbed product has squared norm

Thus the printed pointwise cancellation fails. This does not refute the counting lemma's conclusion. Both assigned follow-up arbiters on this target produced invalid assessments; this witness is separately attributed to the coordinating exact source check.

Exact smoothing script · Exact rational output.

The paper's cited Bourgain–Kontorovich–Sarnak template, arXiv:1001.4541v1, puts the small perturbation outside the representative. That is a plausible repair lead, not a checked transfer from $\mathrm{SL}_2(\mathbb R)$ to $\mathrm{SL}_2(\mathbb C)$ with all subgroup, Sobolev and weighted-boundary estimates intact.

Weighted spectral estimate

lem:spec1, lines 2499–2571, reparametrizes $\gamma_2=\gamma_1^{-1}\gamma_0\gamma_2'$. For its new function, the inner sum is $\sum f(\gamma_0\gamma_2')$. The unchanged kernel $F_q(a,e)=\sum f(a^{-1}\gamma)$ therefore needs $a=\gamma_0^{-1}$; the printed expression uses $\gamma_1\gamma_0^{-1}$. The later region tests also use inconsistent products.

This coordinating source check identifies an ordering mismatch. Uniform weighted errors, the linear-functional boundary strip and smoothing losses remain unverified. There is no usable independent arbitration of this target.

Quadratic-form counting: checked local completion

eq:cKzBnd, lines 3520–3556, writes $z_1C-B^2=-4a^2$ even though the source's form is $Ax^2+2Bxy+Cy^2$, with $AC-B^2=a^2$ and discriminant $-4a^2$. The form $5x^2+4xy+y^2$ gives the exact witness $A=5,B=2,C=1,a=1$: $B^2\equiv-a^2\pmod5$, whereas $B^2\not\equiv-4a^2\pmod5$.

For a primitive representation of $z_1$, change coordinates to put $A=z_1$. Then $B^2\equiv-a^2\pmod{z_1}$ and $C$ is determined. The number of equivalence classes is at most the number of residue solutions; equality is unnecessary. For $p^e\mid\mid z_1$ and $\alpha=v_p(a)$, if $2\alpha\ge e$ there are $p^{\lfloor e/2\rfloor}$ roots. Otherwise, divide out $p^\alpha$ and count roots of the unit congruence, with at most two at odd primes and at most four at 2. The bound is $C_p\sqrt{\gcd(p^e,a^2)}$. Multiplication and a sum over the square divisors from imprimitive representations absorb the divisor factors into $z^\epsilon$, giving the intended upper bound. Gemini's independent full-source arbitration supplies this local completion under the original form/class assumptions.

Full Gemini arbitration · 100 exact prime-power checks · Root-count script. The elementary argument establishes the bound; finite tests alone would not establish it.

Routine reductions and rejected objections

The accepted initial main-theorem arbitration supplies a dyadic completion conditional on the upstream estimates. Its stronger effectivity objection is not adopted as a proof of ineffectivity: that question remains open here. The accepted minor-arc arbitration supplies an exponent restriction below 1/4 and retains the prose coprimality condition. This remains conditional on lem:spec3 and other prerequisites.

Model reports include both accepted and unsupported objections; consult the current synthesis before interpreting a model's original severity labels. No downstream false statement is inferred solely from a defective prerequisite proof.

Reproduction and source record

Download and extract the curated review package. With Python 3 and SymPy (the frozen environment used SymPy 1.14.0), run:

python3 exact_orbits.py > reproduced-orbits.json
python3 exact_smoothing.py > reproduced-smoothing.json
python3 exact_local_roots.py > reproduced-local-roots.json

Compare the parsed JSON with the supplied exact-orbits.json, exact-smoothing.json and exact-local-roots.json. All generator sets and finite orbits are complete for the stated moduli. The scripts make no network calls and use no floating point. The source PDF and native-file hashes are in the separate reading packet. The original evidence manifest also records hashes of privately cached external snapshots; those bibliography entries are not assertions that their proofs were audited or that their full texts are included here.

The historical source-check note was written before follow-up collection finished. Its pending status and reservations are historical, not the final coverage or expenditure. Use the current coverage record.