Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)