Mem
plain-language theorem explainer
Ackermann membership on natural numbers: code i belongs to code n exactly when bit i of n is set. This is the standard ∈ relation for hereditarily finite sets under the Ackermann coding. Anyone building or citing the HF parse of set theory inside Primitive Recognition Calculus uses it as the atomic membership atom. The body is a one-line alias of binary bit testing.
Claim. For $i,n\in\mathbb{N}$, write $\mathrm{Mem}(i,n)$ for the proposition that the $i$-th binary digit of $n$ equals $1$. Under the Ackermann coding of hereditarily finite sets this is the membership relation $i\in n$.
background
The module parses classical set-theoretic structure into the Primitive Recognition Calculus. Hereditarily finite (HF) sets are coded by natural numbers via the Ackermann encoding: the set with elements coded by $i_1,\ldots,i_k$ is the number whose set bits are exactly those indices. Membership then becomes a pure bit test.
Mem is that bit test, packaged as a Prop. Upstream, the two-element type (Lean Bool) supplies the true/false values that Nat.testBit returns; a small bit map sends those booleans to $0$ and $1$ when numeric coefficients are needed. The surrounding siblings (ext_iff, not_mem_empty, mem_one_iff) treat this predicate as the ∈ of an HF set universe.
Local setting: PRCSetTheoryParse is building an expressive, non-degenerate HF system that realizes a delta-style distinction structure, so a concrete, extensional membership atom is required before any axiom-level lemmas.
proof idea
Pure definition, not a proof. The body equates Mem i n with Nat.testBit n i = true. No lemmas are applied; the mathematical content is exactly the standard library bit predicate, re-named so later HF and extensionality statements can speak in set-theoretic language.
why it matters
Without a coded ∈ there is no HF set theory inside PRC. This definition is the membership atom for the Ackermann interpretation: siblings use it for extensionality (two HF codes are equal iff they have the same members, i.e. ℕ bit-extensionality), emptiness, singleton membership, and the package hfSystem that claims the coded universe is expressive, embeds delta, is expression-reflexive, and is non-degenerate. Downstream the module aims at hf_set_theory_realizes_delta, tying HF set structure to the distinction dichotomy of Primitive Recognition Calculus. In the broader RS foundation this is scaffolding for reading classical finite-set reasoning in the same language as the forcing chain and recognition composition, not a physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.