Initial program 13.8
\[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Applied egg-rr0.5
\[\leadsto \sqrt{-\color{blue}{\left(\mathsf{log1p}\left(-u1 \cdot u1\right) - \mathsf{log1p}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Taylor expanded in u2 around inf 14.7
\[\leadsto \color{blue}{\sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 - {u1}^{2}\right)}}
\]
Simplified0.5
\[\leadsto \color{blue}{\sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \left(-u1\right)\right)}}
\]
Proof
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (log1p.f32 u1) (log1p.f32 (*.f32 u1 (neg.f32 u1)))))): 0 points increase in error, 0 points decrease in error
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (Rewrite<= log1p-def_binary32 (log.f32 (+.f32 1 u1))) (log1p.f32 (*.f32 u1 (neg.f32 u1)))))): 232 points increase in error, 3 points decrease in error
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (log.f32 (+.f32 1 u1)) (log1p.f32 (Rewrite<= distribute-rgt-neg-in_binary32 (neg.f32 (*.f32 u1 u1))))))): 0 points increase in error, 0 points decrease in error
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (log.f32 (+.f32 1 u1)) (log1p.f32 (neg.f32 (Rewrite<= unpow2_binary32 (pow.f32 u1 2))))))): 0 points increase in error, 0 points decrease in error
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (log.f32 (+.f32 1 u1)) (Rewrite<= log1p-def_binary32 (log.f32 (+.f32 1 (neg.f32 (pow.f32 u1 2)))))))): 149 points increase in error, 69 points decrease in error
(*.f32 (sin.f32 (*.f32 2 (*.f32 u2 (PI.f32)))) (sqrt.f32 (-.f32 (log.f32 (+.f32 1 u1)) (log.f32 (Rewrite<= sub-neg_binary32 (-.f32 1 (pow.f32 u1 2))))))): 0 points increase in error, 0 points decrease in error
Final simplification0.5
\[\leadsto \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \left(-u1\right)\right)} \cdot \sin \left(2 \cdot \left(u2 \cdot \pi\right)\right)
\]