Computations and visualizations to augment the paper "Decidability bounds for Presburger arithmetic extended by sine" by Eion Blanchard and Philipp Hieronymi. See preprint on arXiv.
Visualization of approximating differences under sine to help encode the undecidable weak monadic second-order theory of the grid in sin-PA.
Visualization of feasible-boundary level sets for a conjunction of linear-sine inequalities to reduce variables for simplifying the existential sin-PA decision procedure.
