Comment by causalmodels

The numerical results are trivial to check. I wrote the analytical results in Lean by hand before asking a former professor to confirm after asking him to keep this private.

They're valid.