zfWitness
plain-language theorem explainer
Maps the two Type-0 tokens false and true into the genuine ZF universe as the empty set and its singleton. Anyone building a FormalSystem parse of full ZFC cites this as the carrier injection. The definition is a two-clause pattern match; injectivity is proved separately from ∅ ≠ {∅}.
Claim. Define a map $w:\{\mathsf{false},\mathsf{true}\}\to V$ (the ZF universe at the lowest universe level) by $w(\mathsf{false})=\emptyset$ and $w(\mathsf{true})=\{\emptyset\}$.
background
The module parses full ZFC (Mathlib's ZFSet) into the Primitive Recognition Calculus FormalSystem interface. That interface demands a Type-0 token carrier, while ZF sets live one universe higher, so any parse must inject a small token set into the real ZF universe rather than identify tokens with sets outright.
Here the ZF universe is pinned as ZF := ZFSet.{0}. The two tokens are the booleans; their images are the von Neumann 0 and 1. Upstream, the module already records that $\emptyset\neq{\emptyset}$ because $\emptyset\in{\emptyset}$ while $\emptyset\notin\emptyset$.
Discrimination in the eventual formal system is not token inequality by fiat: it is genuine extensional difference of the represented sets (existence of a member that belongs to one image and not the other).
proof idea
Pure definition by cases on Bool: false maps to the empty set, true to the singleton of the empty set. No lemmas are applied; the body is the two-clause match itself. Noncomputability is inherited from the ZF set API. Injectivity is not part of this declaration; it is the separate theorem that cases on both booleans and appeals to $\emptyset\neq{\emptyset}$.
why it matters
This injection is the backbone of the full-ZFC parse. The formal system zfSystem takes tokens as Bool, sets discrimination to extensional difference of the images under this map, and uses the real $\emptyset$ and ${\emptyset}$ as endpoints. Downstream, zfWitness_injective records that distinct tokens name distinct sets; distinguishes_iff_ne equates the discrimination relation with inequality of those sets; and full_zfc_realizes_delta packages the whole story: extensionality, $\emptyset\neq{\emptyset}$, discrimination by real set difference, infinity ($\omega$), and a nonempty PRC embedding into the system.
In Recognition Science terms this is the foundation-side witness that a genuine set-theoretic universe can realize the $\delta$ core of the Primitive Recognition Calculus, rather than a toy two-point model with ad-hoc distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.