1 Introduction

This blueprint pins every mathematical definition and headline theorem in zetesis-puremath ¹ to its Lean 4 declaration. The companion source is a personal pure-math reservoir: content needed by the author’s formalization projects (formal-learning-theory-kernel, SMFE, and others) that is either absent from Mathlib or specialized in a way Mathlib’s current formulation does not support directly.