Man this post took forever to get out the door but I think I have cornered the market on “formal modelling of pre-i386 memory addressing in Lean” blog posts https://ntaylor.ca/posts/lean-ltl-6/