# Verification and limits

The written proof is self-contained in main.tex. The detailed originating
researcher's audit is supplied in reproducibility/proof_audit.md.
This is an unrefereed self-audit, not independent expert review and not
formal proof-assistant verification.

The Python checker requires Python 3 and NumPy. Run from its directory:

    python3 check_ut4.py

Its preserved output primary_checks.json records 35 full-enumeration
word-field cases with 6,071,366 matrix input tuples, plus 34,500 exact
pointwise expansion checks. Four additional cases enumerate first
superdiagonal inputs with analytic conditional counting; they are marked
as reduced cases, not full group enumeration. F4 and F8 use genuine
finite-field arithmetic. Probability comparisons use rational numbers.

The secondary checker requires Node.js and no third-party dependencies:

    node check_secondary.mjs

Its preserved output secondary_checks.json records 13,081 tuples in
five cases, using separately implemented dense 4 by 4 matrices. It
also exhibits the class-two shortcut failure and the nonsplit C4/C2
identity-lifting obstruction. Re-running the scripts refreshes their
output timestamps, so preserve the archived outputs if exact provenance
is needed.

Both recorded runs returned PASS. They are finite regression checks,
not a substitute for the arbitrary-word, arbitrary-field proof. The
source conjecture for arbitrary finite p-groups remains unresolved here.