ext_iff
plain-language theorem explainer
Two Ackermann codes of hereditarily finite sets are equal exactly when they share the same members under bit-membership. Anyone working the set-theoretic parse of the Primitive Recognition Calculus cites this as the extensionality axiom on ℕ. The proof is a short bidirectional argument: rewrite one way, and Nat bit-equality plus case analysis on test bits the other.
Claim. For all $m,n\in\mathbb{N}$, $m=n$ if and only if $\forall i\in\mathbb{N}$, (bit $i$ of $m$ is set $\leftrightarrow$ bit $i$ of $n$ is set). Equivalently, under Ackermann membership $i\in m:\Leftrightarrow$ the $i$-th bit of $m$ is $1$, two HF codes are equal exactly when they have the same members.
background
The module parses set theory inside the Primitive Recognition Calculus by coding hereditarily finite (HF) sets as natural numbers via the Ackermann encoding. Membership is bit testing: Mem i n means bit $i$ of $n$ is set, so $i\in n$ in the HF universe.
Extensionality is the claim that sets are determined by their members. On this coding it becomes ordinary bit-extensionality of $\mathbb{N}$: equal codes iff identical membership predicates. The empty set is coded by $0$ (no bits set); the rest of the HF hierarchy is built by setting bits that name already-coded sets.
Locally this sits beside the HF system package (hfSystem, distinction-vs-extensionality, embedding of $\delta$) that shows set theory supplies a genuine distinction mechanism for the recognition calculus.
proof idea
Bidirectional term proof via refine.
Left-to-right: if $m=n$, rewrite the membership biconditional at each $i$.
Right-to-left: apply Nat.eq_of_testBit_eq, reducing equality of codes to equality of all test bits. For each bit index $i$, instantiate the membership hypothesis, case-split on Nat.testBit m i and Nat.testBit n i, and finish with simp_all [Mem], which unfolds membership to the corresponding bit equalities and closes the four Boolean cases.
why it matters
This is the set-theoretic half of the three-foundations distinction package. Downstream, three_foundations_own_distinction quotes it verbatim as set theory's own way of telling primitives apart (paired with type-theoretic canonicity and categorical subobject classification), each yielding the $\delta$ distinction.
It also feeds distinguishes_iff_extensional, the full ZFC parse (distinguishes_iff_ne, full_zfc_realizes_delta), and the HF-system expressivity lemmas in the same module. In the Recognition framework this closes the claim that the Ackermann interpretation satisfies extensionality, so the set-theoretic parse is not a token accident: discrimination is real set difference on HF codes.
No forcing-chain landmark (T5–T8) is at stake here; the result is foundational plumbing for the PRC parse layer rather than a physics constant or dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.