A Computer-Assisted Proof of Alexa's Primality Criterion

For every integer n>=8, put K=floor(n^(1/3)/2) and take r_i to be the least nonnegative residue of (2i+1)^(n-1) modulo n. We prove Alexa's corrected criterion: n is prime if and only if the ordinary integer sum of r_i for i=1,...,K equals K. Residue counting excludes cancellation by zero terms. A classical odd quadratic nonresidue bound excludes even inputs, and prime-product counting treats large prime squares. An integer-parameter version of the Forbes-Kayal-Mittal-Saha polynomial construction bounds an initial odd run in a proper finite-field subgroup of order g by 7sqrt(g)+50, forcing both factors of a remaining semiprime below 150000. Exact computations exclude all remaining cases: 1683064 odd primes in the square domain and 4571 base-3-liar semiprime pairs. C++ and Python implementations and witness certificates are supplied. This is a computer-assisted, AI-assisted, self-audited and unrefereed proof; no independent review, formal verification, practical primality-testing speedup or absolute priority certificate is claimed.