For every \(x : \mathrm{VRObj}\): (i) \(x \in t(x)\) (A3_mem_self), proved as Or.inl rfl; (ii) \(x \subseteq t(x)\) (A3_subset_succ), proved as Or.inr.

A4_induction: any property holding at base and preserved by succ holds for all VRObj; proved by the induction tactic from the recursor of VRObj. A4_exhaustion: every VRObj is either base or of the form succ \(y\); proved by cases. See Remark 1.

If \(x = y\) (Lean equality), then \(\texttt{vrEq}\, x\, y\). Proved by subst followed by Iff.rfl.

\(O(1) = \texttt{succ}\, \texttt{base}\), \(O(2) = \texttt{succ}(\texttt{succ}\, \texttt{base})\), \(O(3) = \texttt{succ}(\texttt{succ}(\texttt{succ}\, \texttt{base}))\); all by rfl.

For every \(k {\lt} n\), \(O(k) \in O(n)\). Proved by induction on the proof of \(k {\lt} n\) using the constructors of Nat.le: the base case is A3_mem_self, and the step embeds via Or.inr.

\(\texttt{vadd}\, a\, b = \texttt{vadd}\, b\, a\) for all \(a, b : \mathrm{VRObj}\). By induction on \(b\): the base case uses vadd_zero_left; the step uses vadd_succ_left and the inductive hypothesis.

\((\texttt{vadd}\, a\, b)\, c = \texttt{vadd}\, a\, (\texttt{vadd}\, b\, c)\) for all \(a, b, c\). By direct induction on \(c\); no auxiliary lemmas needed beyond the definition of vadd.

\(\texttt{vmul}\, a\, (\texttt{vadd}\, b\, c) = \texttt{vadd}\, (\texttt{vmul}\, a\, b)\, (\texttt{vmul}\, a\, c)\) for all \(a, b, c\). By induction on \(c\); associativity of addition (T2) is the key step to redistribute the \(a\)-summand at the inductive step.

\(\texttt{vadd}(O(1),\, O(1)) = O(2)\); proved by rfl via two definitional reductions of vadd.

\(\texttt{O\_ zero}: O(0) = \texttt{base}\) and \(\texttt{O\_ succ}: O(n+1) = \texttt{succ}(O(n))\); both by rfl. These name the two defining equations of \(O\) explicitly to record the Peano correspondence \(0 \mapsto O_0\), \(\mathrm{Nat.succ} \mapsto \texttt{VRObj.succ}\).

\(\texttt{succ}\, x \ne \texttt{base}\) for every \(x : \mathrm{VRObj}\). Proved via VRObj.noConfusion: base and succ are distinct constructors.

P4_succ_inj_leibniz: if \(\texttt{vrEq}(\texttt{succ}\, x, \texttt{succ}\, y)\) then \(\texttt{vrEq}(x, y)\); proved via the predicate \(q\, z := \) if \(z = \texttt{base}\) then \(\top \) else \(p(\text{predecessor of }z)\). P4_succ_inj: if \(\texttt{succ}\, x = \texttt{succ}\, y\) (Lean equality) then \(x = y\); proved by projecting the constructor argument.

The Peano induction axiom P5 coincides with A4 (A4_induction). P5_induction is a named alias, establishing the explicit correspondence without new proof.

No object contains itself: \(\lnot (x \in x)\) for all \(x : \mathrm{VRObj}\). Derived from the private antisymmetry lemma mem_asymm (proved by induction on \(y\) using the private mem_succ_left); the irreflexivity follows immediately.

\(\texttt{vrNe}(\texttt{succ}\, x,\, x)\) for every \(x\). If \(\texttt{vrEq}(\texttt{succ}\, x,\, x)\) held, applying it to the predicate \(p := \texttt{mem}\, x\) would give \(x \in \texttt{succ}\, x \leftrightarrow x \in x\). The left side is true by A3; the right side is false by not_mem_self. See Remark 6.

Left inverse: \(O^{-1}(O(n)) = n\) for all \(n : \mathbb {N}\) (induction on \(n\)). Right inverse: \(O(O^{-1}(x)) = x\) for all \(x : \mathrm{VRObj}\) (induction on \(x\)). Together these establish that \(O\) is a bijection.

\(O(m + n) = \texttt{vadd}(O(m), O(n))\); \(O(m \cdot n) = \texttt{vmul}(O(m), O(n))\); \(O(m^n) = \texttt{vpow}(O(m), O(n))\); all proved by structural induction on the second argument. Note: T1–T4 are not invoked (see Remark 4).

The term Theorem_11_VR_PA : VR_PA_iso is constructed with forward := O, backward := O_inv, and the nine fields filled by the previously proved theorems. The preprint’s metatheoretic equivalence of theorem sets follows: any statement provable on \(\mathbb {N}\) transfers to \(\mathrm{VRObj}\) and vice versa via forward/backward. This is the central result of the chapter.