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 about Peano arithmetic are used in the proofs; only Lean Core's Init.Data.Nat is invoked, and exclusively at the definitional level. lake build passes without warnings; #print axioms is empty for every theorem. The formalisation does not introduce new mathematical content; it provides machine verification of the preprint and records six methodological observations made visible by the formalisation process: (1) A4 becomes a theorem rather than an axiom via the inductive type's recursor; (2) Peano axioms P1 and P2 are absorbed by typing; (3) Theorem 11 admits a constructively stronger form as an explicit isomorphism rather than a metatheoretic correspondence of theorem sets; (4) T1–T4 are not required for the equivalence with PA, which closes through the recursive symmetry alone; (5) the symbol ↔ in the preprint carries two distinct meanings (the operator viff on VRBool versus metatheoretic equivalence Iff); (6) the acyclicity of ∈ is structurally provable without an external measure. Developed using Lean 4 (toolchain version pinned in the repository) with assistance from Anthropic's Claude (Opus and Sonnet) under the methodology described in the repository README. A companion update to VR. A Formal System (version 1.0.1) records these observations in its closing Part IV.