# Verification of the normal intersection counterexample

Author: Alper Ferudun, Mercury Software GmbH. Date: 4 October 2026.

The written proof gives a complete counterexample to AMR-011-0009, Abért's
Question 9. It uses Kassabov's established uniform expansion theorem for
alternating groups. The originating researcher has checked each step; no
outside review or proof-assistant verification occurred.

The quotients are images of one fixed free group F_r. Every input kernel
is normal and finite index, and every individual quotient has lazy spectral
gap at least κ²/(4r), independent of N. The joint image is proved to be
Alt(N)×Alt(N) using the diagonal subgroup and normal generation by a 3-cycle.
The centered diagonal indicator in the transitive N²-point action has norm
squared N−1 and displacement squared 6. The resulting upper gap bound
3/[2r(N−1)] transfers to the regular quotient and then to prefix intersections.

Exact finite checks passed in two separate implementations:

- Python exhaustively generated A_5×A_5 (3,600 elements) and A_6×A_6
  (129,600 elements), verified the full joint images and equal-size orbit
  fibers, and checked the lifted cuts. It also checked 5,910 permutation
  instances in degrees 3 through 7.
- C++ enumerated all even degree-five permutations lexicographically and
  checked the 3,600 pairs directly. All 25 orbit fibers have size 144;
  the lifted diagonal has 720 elements and 864 outgoing labelled edges.
  Integer-scaled norm and displacement identities passed for N=5,...,128.

These computations do not establish uniform expansion and do not replace
the general proof. The small generating sets used in the tests are not
claimed to be Kassabov's uniformly expanding sets.

The source statement, the relevant published theorems, and the scope of the
fixed-subgroup result were checked. Priority remains undetermined after a
bounded search. This is an AI-assisted unrefereed preprint, not a peer-reviewed
or formally verified result. Third-party PDF sources are not redistributed.

Reproduce the checks from the source archive with:

```
python3 reproducibility/check_finite.py
c++ -std=c++17 -O2 reproducibility/check_cut.cpp -o /tmp/tau-cut-check
/tmp/tau-cut-check
```