mem_one_iff
plain-language theorem explainer
Under Ackermann coding of hereditarily finite sets, code 1 is the singleton {∅}, and its only member is code 0. Anyone wiring HF set theory into the PRC FormalSystem interface cites this to pin the right endpoint. The proof is a two-case bit test on the natural index: bit 0 of 1 is set, and every successor bit is unset.
Claim. For every natural number $i$, Ackermann membership holds between $i$ and $1$ if and only if $i = 0$. Equivalently, under the standard coding of hereditarily finite sets, the only element of the singleton $\{\emptyset\}$ (code $1$) is $\emptyset$ (code $0$).
background
This module parses hereditarily finite (HF) set theory into the Primitive Recognition Calculus FormalSystem interface. Tokens are HF set codes (naturals); discrimination is extensional set inequality; the endpoints are genuine $\emptyset$ (code 0) and ${\emptyset}$ (code 1).
Membership is Ackermann coding: $i \in n$ means bit $i$ of $n$ is set (Nat.testBit n i = true). Extensionality is then ordinary bit-extensionality of $\mathbb{N}$. Code 0 has no bits set (empty set); code 1 has only bit 0 set, so it is the von Neumann singleton ${\emptyset}$.
Upstream Peano facts (succ_ne_zero) supply that every successor differs from zero, which closes the negative half of the biconditional when the index is a successor.
proof idea
Case-split on the index $i$.
If $i = 0$, both sides hold: Nat.testBit 1 0 is true by decision procedure, and $0 = 0$ is reflexivity, so the biconditional is iff_of_true.
If $i = \mathrm{succ}, j$, the right-hand side $i = 0$ is false by Nat.succ_ne_zero. The left-hand side is false because Mem unfolds to testBit, testBit_succ reduces bit $\mathrm{succ}, j$ of 1 to bit $j$ of $1/2$, and $1/2 = 0$ (decided), so the bit is unset. Package with iff_of_false.
why it matters
This is clause (iii) of the packaged faithfulness theorem hf_set_theory_realizes_delta: HF set theory under Ackermann coding has ${\emptyset} = $ code 1 with exactly the member $\emptyset$. That theorem also records extensionality, emptiness of code 0, discrimination by genuine set difference, and a nonempty PRC embedding of the $\delta$ core into hfSystem.
In the PRC story, the two endpoints of a formal system must be the genuine empty set and its singleton so that $\delta$ (the minimal distinction) is realized by von Neumann 0 and 1 as sets, not by ad-hoc tokens. Without this membership characterization, the parse would not certify that code 1 is ${\emptyset}$.
The result sits in Foundation, feeding the set-theoretic realization of the FormalSystem interface rather than the T0–T8 forcing chain directly; it is infrastructure for showing that ordinary HF set theory already carries the $\delta$ structure PRC demands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.