Simplified0.4
\[\leadsto \color{blue}{\frac{{\left(2 \cdot \left(\pi \cdot n\right)\right)}^{\left(\mathsf{fma}\left(k, -0.5, 0.5\right)\right)}}{\sqrt{k}}}
\]
Proof
(/.f64 (pow.f64 (*.f64 2 (*.f64 (PI.f64) n)) (fma.f64 k -1/2 1/2)) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (PI.f64)) n)) (fma.f64 k -1/2 1/2)) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (fma.f64 k (Rewrite<= metadata-eval (neg.f64 1/2)) 1/2)) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (fma.f64 k (neg.f64 (Rewrite<= metadata-eval (/.f64 1 2))) 1/2)) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (fma.f64 k (neg.f64 (/.f64 1 2)) (Rewrite<= metadata-eval (/.f64 1 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 k (neg.f64 (/.f64 1 2))) (/.f64 1 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (/.f64 1 2)) k)) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (*.f64 (neg.f64 (Rewrite=> metadata-eval 1/2)) k) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (*.f64 (Rewrite=> metadata-eval -1/2) k) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) k) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 2 k))) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 k) 2)) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 k)) 2) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 k 2))) (/.f64 1 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 1 2) (neg.f64 (/.f64 k 2))))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 1 2) (/.f64 k 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 1 k) 2))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))) (sqrt.f64 k)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 2 (PI.f64)) n) (/.f64 (-.f64 1 k) 2)))): 30 points increase in error, 18 points decrease in error