Axiom audit for the low individual degree test

The soundness theorem, proved through the vendored MIPStarRE development, must not depend on anything beyond the three standard axioms; this file fails to build otherwise.