Exact controls for the Kac–Grassmann candidate proof

Run with Python 3:

python3 verify_structural_controls.py

The script uses only the standard library and exact rational arithmetic. It checks three deliberately small controls:

1. the non-square-zero rank-one model $M_2(k)\widehat\otimes\Lambda(\theta)$, including the super-Leibniz rule, $Q^2=\operatorname{ad}E_{12}\ne0$, $Q^6=0$, and the module contraction identity;
2. the supercenter of $Q(1)\widehat\otimes\Lambda(\theta_1,\theta_2)$, including the queer case that is easiest to mishandle by signs; and
3. explicit separability idempotents for the smallest queer and matrix simple superalgebras.

These are sign and model checks. They do not prove the global theorem. The global argument is in FPRD-supertannakian-candidate-resolution-2026-09-06.md and depends on Kac’s differentiably-simple-superalgebra theorem and Coulembier–Sherman’s commutative absolute-flatness theorem.