VR. A Formal System: Lean 4 Formalisation of Part I

Machine-verified Lean 4 formalisation of Part I of VR. A Formal System (Reznik, 2026; Zenodo DOI 10.5281/zenodo.20212092), the first work of the VR cycle. The formalisation covers the three primitives {∅, →, t}, the four axioms (A1–A4), Definitions 1–9, the §5 lemma t(x) ≠ x, the construction of von Neumann ordinals, the arithmetic operations and theorems T1–T4, the five Peano axioms in VR (Theorems P1–P5), and the §11 equivalence theorem realised as an explicit structural isomorphism VR_PA_iso : Nat ≃ VRObj preserving zero, successor, addition, multiplication, and exponentiation. All 51 theorems are axiom-free in the sense of Lean: none depends on propext, Classical.choice, or Quot.sound. No mathlib lemmas…