Can't you just formalize both definitions and pick the one to work with based on what you want to do? Surely the only obstacle here is the time and effort it takes to write the formalization?

Or, alternatively, just because you've formalized the advanced calculus version doesn't mean you need to use the formalization when teaching basic calculus. The way we've proven something and the way we teach that something don't have to be the same.

I imagine you could change the p-value test to randomly sample assignments generated via the exact same process that was used to generate the assignment used by the experiment, and as you run more and more iterations of this the calculated p-value should converge to the correct value, but then the question becomes is the p-value calculated this way the same as the p-value you'd get if you actually went ahead and used equiprobable assignment to begin with?

Ultimately, this all comes down to the fact that it's not hard to use true randomness for the whole thing, and true randomness produces statistically valid results, if you use true randomness for assignment then you can't screw up the p-value test, and so there's no reason at all to even consider how to safely use a PRNG here, all that does is open the door to messing up.

FWIW you can fix the shell issue by wrapping your shell in a shim that essentially runs wait4path on the nix store before exec'ing your real shell. I set up my environment to install that shim binary directly onto the data volume at a known path so it can be used as my login shell.

If you look at the preprint paper, the knot it starts with has 14 crossings, but they actually move the strings around to end up with 20 crossings prior to performing the first 2 crossing changes in the unknotting sequence. So the potential space for moves here is actually rather large.