not_mem_empty
plain-language theorem explainer
Under Ackermann coding of hereditarily finite sets, no natural number i is a member of code 0. Anyone citing the HF parse of the δ-core needs this as the empty-set clause. The proof is a one-line simplification of the bit-test definition of membership.
Claim. For every $i \in \mathbb{N}$, $\neg\, i \in_{\mathrm{Ack}} 0$, where $i \in_{\mathrm{Ack}} n$ means that bit $i$ of $n$ is set. Equivalently, the empty set (coded by $0$) has no members.
background
This module parses hereditarily finite (HF) set theory into the Primitive Recognition Calculus via the standard Ackermann coding of HF sets by natural numbers. Membership is the bit-test relation: code $i$ belongs to code $n$ precisely when bit $i$ of $n$ is set (Mem).
Under that coding, $0$ is the empty set: every bit of $0$ is unset. The companion fact that code $1$ is the singleton ${\emptyset}$ (only member $0$) sits immediately downstream. Extensionality of HF codes is just bit-extensionality of $\mathbb{N}$.
The local goal is to show that this coded HF universe realizes the $\delta$ core of PRC: it is extensional, non-degenerate, and distinguishes by genuine set difference, with endpoints $\emptyset$ and ${\emptyset}$ as von Neumann $0$ and $1$.
proof idea
One-line term/tactic proof: unfold Mem (which is Nat.testBit n i = true) and simplify. For $n = 0$, every bit test is false, so $\neg,\mathrm{Mem}, i, 0$ holds for all $i$.
why it matters
Feeds the packaged faithful-parse theorem hf_set_theory_realizes_delta, whose second conjunct is exactly $\forall i,,\neg,\mathrm{Mem}, i, 0$. That theorem asserts HF set theory under Ackermann coding satisfies extensionality, has $\emptyset = 0$ with no members, has ${\emptyset} = 1$ with sole member $\emptyset$, discriminates by set difference, and realizes the $\delta$ core via a PRC embedding.
In the Recognition foundation stack this is the set-theoretic reading of the primitive distinction: the two endpoints of the first distinction are literally the von Neumann numerals $0$ and $1$, distinguished as sets rather than as bare codes. It is a small but load-bearing clause in showing that the PRC $\delta$ structure is not an ad-hoc formal gadget but the HF universe itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.