Additional source adjudication
21 October 2026. These are coordinator checks of native Sol/Gemini findings, not accepted model arbitration or formal verification. Exact native quotes and locations are in source-evidence.json. Original native outputs are unchanged.
Scope and editions
The native source is arXiv 2208.02525v6. The user-supplied official journal PDF has SHA-256 fe44b57f5aa5f50884b4a126da589fe38029f1a3035f9c57bd1e325c031d9e4f. Journal locations below were compared directly with extracted PDF text. This is targeted edition comparison, not a claim that every line is identical. The original strict-margin counterexample and journal comparison remain the decisive main-theorem evidence.
Successful local check: Lemma 2.1
All bracket containments and identities in Lemma 2.1, journal p. 197, hold. They are bilinear, so checking every pair in the displayed bases proves the stated universal containments. The exact checker performs 34 matrix checks, including the brackets between the two transverse subspaces and the three standard sl2 identities. This supports only this local lemma, not the later Baker–Campbell–Hausdorff constants or global argument.
Nondivergence: a literal statement counterexample
Proposition 4.1, journal p. 201, assumes both endpoints lie outside the thick part. Fix s=1 and let x_delta=diag(delta,delta^(-1),1) Gamma. If c=||e1|| and c delta<exp(-2/3), the vector delta e1 witnesses both exclusions. The same vector survives every a(1)u(r) translate. With beta=2c delta the bad set is therefore the whole centered unit interval, of measure one. The proposed uniform upper bound C beta^alpha tends to zero as delta tends to zero, a contradiction for any fixed alpha>0 and C. This uses no external nondivergence theorem and works for any fixed vector norm.
Replacing nonmembership by membership is a candidate statement correction. It does not address the shifted endpoint threshold loss or the empty retained-set example.
The separation lemma: a bounded-time counterexample
Lemma 4.2 quantifies over every ell at least 1 (journal pp. 201–202). With the standard coordinate or Frobenius Lie-algebra norm, choose
The interval notation [beta] means [-beta/2,beta/2], so the coefficients are permitted. Both exponentials in the hypothesis are literally equal as group elements. The coefficient triple has norm beta/4, while ||v||=e beta/4<beta because e<3. The a(-1) lattice has shortest vector e^(-1/2), as does its dual; this exceeds beta^(1/4)=1/16. Thus its vector and bivector conditions hold. All opposite coefficients u*,v2,w2 vanish, contradicting the claimed conclusion.
This refutes the full printed parameter range under these conventional norms. The proof explicitly assumes ell sufficiently large when it says the integral return is nontrivial. Restricting to sufficiently large ell would exclude this particular example; applications later in the paper use ell growing with t. This local counterexample therefore does not independently refute those large-time applications.
Initial dimension: two false auxiliary assertions
In the proof of Proposition 6.2, journal p. 205, the assertion that an SL(3,Z) element with nontrivial unipotent part must itself be unipotent is false. For example,
The two factors commute; the first is semisimple, and the second is a nonidentity unipotent. The integral matrix has determinant one and eigenvalues 1,-1,-1. Its square is unipotent, but a power-taking replacement needs to be incorporated into the bounds and subsequent argument. This example disproves the blanket auxiliary assertion; it is not a counterexample to Proposition 6.2 with all its dynamical hypotheses.
The stabilizer assertion on the same page also omits a component. Put D=diag(-1,-1,1). Conjugation by D sends (a,u,u*) to (a,-u,-u*), so it fixes their exterior product v_H. But every element of A0 H has positive first diagonal entry, whereas D has first entry -1. Hence Stab(v_H)=A0 H is false literally. Its identity-component version is a possible correction; a finite-component issue alone does not establish failure of the quantitative argument.
On p. 204, the coefficient in (6.8) is a0, while the later appeal to that equation claims a lower bound for a2. This reference does not justify the bound as printed. The separation exponents also change between 5 d0 ell and 10 d0 ell. These are checked source inconsistencies. We have not reconstructed the return selection or proved that every possible corrected version fails.
Subgroup nonconcentration: reversed conjugation
Proposition 6.3's proof, journal p. 206, uses the identity
It is false. The source's own diagonal weights give Ad(a0(ell)) equal to exp(-ell/2) on r1 and exp(ell/2) on r2. The input widths beta exp(-ell) in r1 and beta in r2 therefore become beta exp(-3ell/2) and beta exp(ell/2). They do not both become beta exp(-ell/2).
Negative conjugation balances these two scales. That supplies a local algebraic correction, but the translated point, allowed parameter ranges, thick-part conditions and repeated closing argument must then be checked. We do not adopt a repaired Proposition 6.3 on the strength of changing the sign.
Basic reduction: an impossible cover
Proposition 7.2's proof (journal p. 208) asserts that a finite collection of translates Pi(x) covers all X=SL(3,R)/SL(3,Z). For fixed finite parameters, Pi is relatively compact: it is a finite product of bounded exponential neighborhoods and conjugates of such neighborhoods. Each Pi(x) is therefore relatively compact; finitely many cannot cover the noncompact space X.
For a direct proof of noncompactness, the lattices diag(e^(-T),e^T,1)Z^3 have shortest vector tending to zero, whereas the shortest-vector function is positive and bounded below on every compact subset. Thus this is a false auxiliary assertion in the proof.
The measure under discussion is supported on an appropriate thick subset. A finite cover of that subset is a possible replacement, but its size and compatibility with the required neighborhood estimates have to be supplied. We do not infer that the reduction proposition itself is false.
Conditional measures: a missing denominator
Lemma 8.6 (journal p. 212) bounds a conditional probability by the unconditioned probability. For the full playground P, the definition gives
Conditioning alone does not imply the displayed inequality with denominator one. For instance, if mu(P)=1/4 and A is a subset of P with mu(A)=1/8, then the conditional probability is 1/2, greater than 1/8. Fullness only gives mu(P) at least beta^15, so the direct available upper bound carries beta^(-15).
This is a counterexample to the invoked inference from the definition, not to the dynamical lemma's final bound. A separate stronger dynamical estimate could in principle establish that bound. The needed bound, and its propagation into later packet estimates, remain unresolved.
Hyperbola lemma: a uniform parameter counterexample
Part (1) of Lemma 11.4 (journal p. 240) claims that closeness at scale A exp(-3s') forces |w-w'| at most A exp(-s'+2ell). This necessity fails, by an unbounded factor in beta.
Write q=exp(s'), take A=1, ell=0, and set
Suppose
These ensure both w and w' lie in the lemma's permitted range. Let C and C' be the two graphs X=-Y/(1+wY) and X=-Y/(1+w'Y), each clipped to the exact square in the statement, whose half-width is R=3 beta/(5q).
For |Y| at most R, both denominators exceed 1/2 because
For every point of C', the same-Y point of C is still in the square. If Y is nonnegative then |X_C| is at most Y, which is at most R. If Y is negative, its denominator for C is larger than that for C', so |X_C| is smaller than |X_C'|. Thus clipping does not invalidate the comparison.
The exact graph difference gives
Same-Y pairing bounds Euclidean distance as well. Therefore every point of C' lies within the required q^(-3) neighborhood of C. But
contradicting the claimed parameter conclusion. The ratio is beta^(-1), so no fixed multiplicative constant restores that conclusion uniformly as beta tends to zero.
These sufficient conditions are compatible with the paper's linked scales, not merely with unrelated free parameters. Choose s'=c t with c=delta1/4=1/400000. If b=epsilon^3, then beta=exp(-bt). The source constants give epsilon2=10^(-26) theta, N1=10^31/theta, and
Also c>b. All four displayed sufficient conditions therefore hold for sufficiently large t. Since C1 epsilon1 is much smaller than 2, A=1 is permitted. The k range and ell=0 are permitted exactly. This establishes a counterexample to the printed lemma within the source's asymptotic parameter regime.
This strengthens Sol's proposed two-times-bound example. It does not establish an appropriate corrected estimate or repair the later curve-counting arguments.
A dropped factor and a changed exponent
In the proof of Lemma 11.6, journal p. 246, the cited Lemma 11.4(2) supplies neighborhood size beta^(-100) A exp(-3s'). Substituting A=exp(2s'-2ell-m) gives beta^(-100) exp(-s'-2ell-m). The proof claims the stronger bound exp(-s'-2ell-m), dropping beta^(-100). The cited bound does not supply that conclusion, even provisionally accepting the already defective lemma. This diagnoses an inference; it does not disprove Lemma 11.6 independently.
In Proposition 9.10's proof, journal p. 231, the constructed orbit-visit lower bound beta^30 exp(2s') is later replaced by beta^22 exp(2s') as though it were the same property. For 0<beta<1 this is a stronger bound. The following page returns to beta^30, so the beta^22 occurrence can plausibly be a local transcription error. We do not count it as an additional false theorem or infer that it alone breaks the final estimate.
Exact versus approximate decomposition
Proposition 12.1 asserts an exact positive-measure decomposition (journal p. 258). The final comparison on p. 260 establishes only proximity against smooth test functions. Such proximity cannot by itself yield an exact decomposition with a small positive exceptional weight.
For example, delta_h and delta_0 differ by at most h on every 1-Lipschitz test function. But if delta_h=(1-e)delta_0+e nu for a probability measure nu and h nonzero, evaluating the singleton {0} forces e=1. Thus arbitrarily small weak distance need not permit any small positive error component.
There is also an overlap problem: for the declared cover Upsilon_k, each mass times its normalized restriction equals the original measure restricted to Upsilon_k. Their sum has multiplicity equal to the number of covering sets. A cover without disjointization does not supply the stated measure identity.
These are verified defects in the supplied derivation. They do not by themselves rule out another construction satisfying Proposition 12.1. Replacing it with a weak approximation theorem requires proof of disintegration, transported dimensional bounds, normalization and accumulation of errors.
Chronology and claims not adopted
The cited Lindenstrauss–Mohammadi Proposition 4.2 is present on p. 16 of arXiv:2112.14562v1, submitted 29 December 2021, before the 26 September 2022 cutoff. Its PDF and abstract history are frozen with hashes. The native panel's unresolved availability question is therefore resolved for this specific proposition. Its original groups are SL(2,C) and SL(2,R) times SL(2,R), and its transverse measure is one-dimensional. Yang's SL3 proposition uses a two-dimensional transverse measure and different scales. The applicability/adaptation remains an obligation; this check does not certify it.
The native local packets sometimes lack definitions present in the complete source. In particular, [1]=[-1/2,1/2], the basis and diagonal matrices are explicitly defined. Missing packet context is not a paper error. Bounds calculated by assuming [1]=[0,1] are not adopted.
Broader objections about encounter geometry, inverse-function charts, closing estimates, overlaps, complete orbit pieces, Diophantine transference and norm constants remain separately listed in allegation-inventory.json. We do not elevate every listed concern to a confirmed defect. No defect is inferred in the qualitative Ratner theorem quoted for context.
Current primary pages (Annals, arXiv history, and the author's publication list) were fetched again. No correction was found in those inspected records or targeted correction searches; that is not an exhaustive search or a novelty claim. No author's agreement with these findings is recorded.
Additional supporting archive items are identified in the original report. View the manuscript hashes and repository snapshot.