Source check of the supplied Astra counterexample

21 October 2026. Coordinator mathematical adjudication and exact symbolic checks, separate from the native panel. The user identified the supplied analysis as Astra's; the precise model ID and effort are unauthenticated. This note checks that supplied claim rather than claiming discovery priority.

The counterexample refutes Theorems 1.2 and 1.3 as stated in arXiv 2208.02525v6. The official journal PDF was subsequently supplied and compared: the counterexample applies to its Theorems 1.2–1.3, p. 192; see the journal comparison. Full line-by-line equivalence is not claimed. The author currently links arXiv from the publication entry. Annals 202 (2025), 189–264, has 76 article pages, whereas v6 has 63 PDF pages. Publisher milestones give received date 26 September 2022, revised 29 July 2024, accepted 6 September 2024.

Statement and quantifiers

The native labels are thm:effective-U-orbit (Theorem 1.2), thm:main-thm (Theorem 1.3), and eq:def-compact-set (the vector-and-bivector thick part). The source gives the exceptional condition in Theorem 1.3 as

a_0 (\ell )x_0 \not\in X_{e^{-|\ell|/3}}

for some 0.99t≤|ℓ|≤1.01t. Both signs must therefore be checked to exclude this alternative. The theorem explicitly quantifies over every sufficiently large t and every starting lattice, with a fixed Sobolev norm and an absolute implied constant. The counterexample below keeps the starting lattice and test function fixed for Theorem 1.3; no issue about uniformity in a moving test function arises.

Exact lattice and exterior-square calculation

Let

Its determinant is one. Direct inversion gives

The exact checker verifies this and the exterior-square identity J(∧²g)=g⁻ᵀJ for the signed Hodge map J sending (e₁∧e₂,e₁∧e₃,e₂∧e₃) to (e₃,−e₂,e₁). Thus the bivector test really is the dual-lattice test for the usual induced Euclidean norm; it is not omitted or replaced by a one-sided vector calculation.

Put q=exp(L/6). For L≥10 we have q>4: already 1+5/3+(5/3)²/2=73/18>4 is a strict Taylor lower bound for exp(5/3). Thus a₀(L)=diag(q²,q⁻¹,q⁻¹). The four shortest lengths are

Here are exhaustive branch arguments over all integers, not a finite numerical search:

• A vector of a₀(L)Λ has coordinates (2q²(m+n/3), n/q, p/(2q)). A nonzero transverse coordinate is at least 1/(2q); with both transverse coordinates zero the first coordinate is at least 2q².
• A vector of a₀(−L)Λ* has coordinates (Q/(2q²), q(K−Q/3), 2qJ). A nonzero transverse coordinate is at least q/3, which exceeds 3/(2q²) for q≥4. If both vanish, J=0 and Q must be divisible by three. The first coordinate is then at least 3/(2q²).
• A vector of a₀(−L)Λ has coordinates (2(m+n/3)/q², qn, qp/2). Nonzero transverse coordinates are at least q/2>2/q²; otherwise the minimum is 2/q² on the first axis.
• A vector of a₀(L)Λ* has coordinates (q²Q/2, (K−Q/3)/q, 2J/q). For Q≠0 the first coordinate is at least q²/2>1/q; for Q=0 the minimum is 1/q.

The bounds are attained on coordinate axes, so these minima hold for the coordinate sup norm too. Their ratios to the theorem threshold q⁻² are q/2, 3/2, 2 and q. Consequently both signs lie in X_((3/2)exp(−L/3)) for every L≥10. The entire theorem window satisfies the hypothesis for all sufficiently large t. The symbolic script also checks complete integer boxes at rational q=4,8 as independent sanity checks; the branch arguments, not those boxes, establish the all-integer statement.

Fixed-vector obstruction and the two theorem formulations

Both a(t) and u(r) fix e₁, while g e₁=2e₁. Thus all a(t)u(r)Λ contain 2e₁. The locus Y={Λ′:2e₁∈Λ′} is closed: in a local basis chart the integer vector g′⁻¹(2e₁) must remain integral under a convergent sequence. It is proper: diag(3,1,1/3)Z³ does not contain 2e₁. Choose a nonzero nonnegative smooth compactly supported bump in X∖Y. Its orbit integral is zero for every t and its Haar integral is strictly positive. Its Sobolev norm is fixed and finite, so an exponentially decaying discrepancy bound is impossible.

This directly refutes Theorem 1.3. For Theorem 1.2 use x_t=a(t)gΓ. The exact matrix identities give u(reᵗ)x_t=a(t)u(r)gΓ and a(−t)a₀(ℓ)x_t=a₀(ℓ)gΓ. The theorem permits x_t to depend on t. This proves the refutation of its uniform formulation as well.

Definition 6.1 and equation (6.7)

The native label def:initial-construction removes a point if some allowed diagonal translate fails the β^(1/4) thick-part test. The subsequent eq:decomposition-measure asserts exponentially small removal. Every y in E=a(s)u([1])x₀ still contains 2e₁. Choosing ℓ=0, ℓ′=−2δ₁t gives the vector 2exp(−2δ₁t/3)e₁.

The recorded constants are δ₁=δ₂=10⁻⁵ and β=exp(−ε³t). The source definitions imply N₁>1 and ε=exp(−10⁵N₁)<10⁻³. Therefore

For all sufficiently large t the vector is shorter than β^(1/4). Hence F is empty, with discarded proportion one, contradicting the bound O(s²β^α₂)→0. This does not depend on accepting the nondivergence proposition.

For the proposed nondivergence application, S=s−ℓ and the shifted base point is a₀(ℓ′)x₀. Its endpoint requirement would involve the stronger thickness exp(−S/3). The original hypothesis at an endpoint of size |ℓ′±S| gives only exp(−|ℓ′±S|/3). At ℓ=0, ℓ′=−2δ₁t, one endpoint has size (1+δ₁)t while S=(1−δ₁)t. The lost ratio is exp(−2δ₁t/3), despite both times lying in the prescribed window.

A separate literal issue in Proposition 4.1

The native source at prop:quantitative-nondivergence actually prints

a_0(-s)x , a_0(s)x \not\in X_{e^{- s/3 }}

as its hypothesis. The proof's intended contrapositive calls for membership, so this deserves a separate typo/statement check. It does not cure the main counterexample: even reading this as membership leaves the shifted-endpoint exponent loss just demonstrated. Neither the literal typo nor an attempted correction is used as an unverified premise of our fixed-vector refutation.

Constant changes and the curve calculation

For the supplied family g_(c,Q), direct inversion gives a first-axis lattice minimum c and dual first-axis minimum Q/c. Coordinate branches show these are the critical coefficients for the two signs after sufficiently large diagonal translations. Choosing c>C and integer Q>Cc defeats any proposed fixed constant C multiplying exp(−|ℓ|/3). Thus changing strictness or a universal norm normalization does not solve this obstruction. A stronger exponent 1/3−κ would exclude these fixed-vector examples, but no amended theorem or complete repair is verified here.

The curve calculation also has a checked matrix-scale issue: a quadratic Taylor term at r=exp(−t/2)/2 is multiplied by exp(t), giving exactly 1/4. This refutes that claimed exponentially small rescaled matrix remainder. It is not by itself a counterexample to Corollary 1.6, nor a complete argument about quotient distance near the cusp. Shorter intervals require the rest of the proof and parameters to be checked afresh.

Evidence and next checks

exact-check.py and exact-results.json bind the exact algebra to the frozen expanded-source hash. All mathematics above is a coordinator check of Astra's supplied analysis, not a formal certificate or a native-panel result. The independent panel receives the manuscript without this note or the Astra synopsis. Targeted journal comparison is complete. No exhaustive correction search or priority claim is implied.