# Verification report

## Result

The manuscript proves the full Haar-measure-class interpretation of
Abért's Question 4. The exceptional set is a countable union of proper
algebraic subsets of `SL_2(Q_p)`.

## Critical repair to the imported candidate

The frozen upstream proof record ends after exactly 2,000 characters, before
the proof of its decisive algebraic claim. That claim was also stated too
strongly: for a nontrivial unipotent `u`, the map `x -> x u x^-1` has trace
identically 2 but is not constant.

The paper replaces it with the correct lemma retaining the parabolic-free
coefficient subgroup. The highest two coefficients of
`tr(w(I+tN))` force:

- `a_k a_0 = +/- I`;
- `e_k = -e_1`.

The word is then a fixed conjugate of a variable conjugate of a shorter word.
Induction ends at a constant in the coefficient subgroup, where the
parabolic-free hypothesis forces `+/- I`.

## Exact executable checks

Run:

`python3 reproducibility/check.py`

Current output:

`PASS: nilpotent powers, top coefficients, next coefficient, conjugation reduction, and overstrong-lemma counterexample`

All checks use exact rational arithmetic.

## Literature status

The original author-hosted PDF and current close literature were inspected
through 2026-09-02. Gordeev–Kunyavskii–Plotkin prove a general dichotomy for
central functions of word maps with constants, but do not state this exact
parabolic-free constant-trace induction. Aoun's random-freeness theorem does
not exclude unipotents. No direct later solution or status update was found.

Novelty confidence is low: Abért phrased the item as “Show that,” and the
proof is elementary enough to have been known informally. No priority claim
is made.

## Build and PDF QA

`PASS`: Tectonic 0.17.0 and BibTeX produced a four-page letter-size PDF with
zero LaTeX errors, undefined references/citations, overfull boxes, or
underfull boxes. All four pages were rendered at 144 DPI and directly
inspected; no clipping, margin, formula, bibliography, or legibility defect
was found. The exact checker passes from the source archive. The author approved public Zenodo/EulerSolve release on 2026-09-02 under CC BY 4.0; arXiv status is separate.

## Public release and license

The author approved public release on 2026-09-02. This paper, its source files, and this verification report are licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/