hf_set_theory_realizes_delta
plain-language theorem explainer
Hereditarily finite set theory under Ackermann coding is a faithful parse of the primitive recognition calculus: it is extensional, carries genuine empty-set and singleton endpoints, discriminates by set difference, and embeds the δ core. Anyone citing the set-theoretic realization of PRC would quote this packaging result. The proof is a one-line product of five already-proved component lemmas.
Claim. Under Ackermann coding of the hereditarily finite sets, the following hold simultaneously: (i) $m=n$ if and only if $\forall i\,(\mathrm{Mem}(i,m)\leftrightarrow\mathrm{Mem}(i,n))$; (ii) nothing is a member of code $0$; (iii) $\mathrm{Mem}(i,1)$ if and only if $i=0$; (iv) two codes are distinguished exactly when they differ on some membership bit; and (v) there exists a PRC embedding into this formal system (preserving endpoint distinction and finite trace extension).
background
Ackermann membership reads bit $i$ of natural $n$: $\mathrm{Mem}(i,n)$ means that bit is set. Under this coding the naturals are exactly the hereditarily finite sets, with $\in$ recovered as bit tests. Extensionality is then ordinary bit-extensionality of $\mathbb{N}$: two codes are equal iff they have the same members.
The module builds a FormalSystem whose tokens are HF codes, whose discrimination relation is plain inequality of codes, and whose endpoints are the genuine von Neumann $0=\emptyset$ (code 0) and $1={\emptyset}$ (code 1). A PRC embedding into a formal system is a structure that maps the two primitive endpoints and finite traces so that endpoint distinction and trace extension are preserved.
Upstream, discrimination is already identified with genuine set difference ("two codes are distinguished exactly when they differ in some member"), and non-emptiness of a PRC embedding into this system is already recorded as "HF set theory contains the δ core."
proof idea
Term-mode packaging: the five conjuncts are supplied directly by the five prior results ext_iff, not_mem_empty, mem_one_iff, distinguishes_iff_extensional, and hfSystem_embeds_delta. No further rewriting or case analysis occurs; the theorem is the conjunction of those lemmas.
why it matters
This is the packaged "faithful parse" of HF set theory into the Primitive Recognition Calculus interface. It records, in one place, that Ackermann-coded HF sets satisfy extensionality, carry the von Neumann endpoints $\emptyset$ and ${\emptyset}$ as genuine sets, discriminate by real membership difference rather than coding accident, and realize the δ core via a PRC embedding. In the foundation layer this certifies that ordinary finite set theory is a concrete model of the distinction-and-trace structure PRC demands, before any physics (J-cost, forcing chain T0–T8, or the eight-tick octave) is imposed. No downstream consumers are wired yet; the declaration closes the SetTheoryParse development as a self-contained realization certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.