Axiom audit for the direct parallel repetition theorems

The theorems proved through the vendored developments must not depend on anything beyond the three standard axioms; this file fails to build otherwise. (The entangled theorem MIPRE.Repetition.quantumValue_repeat_le joins this file once quantumValue_eq_entangledValue is proved.)