I figured it out! Thanks for being patient with me.
Great stuff, and you are welcome.
Even though this doesn’t fully represent a ceaser cipher, it still accurately preserves the semantics.
To be picky, semantics is in the opposite direction than formalization. I’d say at this point you have implemented the modular arithmetic that I said I would start by abstracting away.
Indeed, so many more things could be said and done: it’s a pretty nice case study.