Requesting help with formalization in Lean!

Here’s what I have so far:

https://zenodo.org/records/15744937