zfWitness_injective
plain-language theorem explainer
The map sending Boolean tokens to ZF sets (false to empty, true to singleton empty) is injective. Anyone assembling the ZFC parse of the FormalSystem interface needs this to guarantee distinct tokens name extensionally distinct sets. The proof is exhaustive case analysis on the two Booleans, discharging mismatches via emptiness of the empty set.
Claim. The witness map $w:\{\mathsf{false},\mathsf{true}\}\to\mathrm{ZF}$ defined by $w(\mathsf{false})=\emptyset$ and $w(\mathsf{true})=\{\emptyset\}$ is injective: if $w(a)=w(b)$ then $a=b$.
background
This module parses full ZFC into the minimal FormalSystem interface used by the Primitive Recognition Calculus (PRC) inevitability theorem. That interface needs a token carrier, an expression carrier, a discrimination relation, an expression-extension order, and endpoint tokens. Here tokens are Booleans, and discrimination is genuine ZF extensional inequality of the represented sets.
The witness map embeds those tokens into the ZF universe at universe level 0: false names $\emptyset$, true names ${\emptyset}$ (von Neumann 0 and 1). The companion lemma that $\emptyset\neq{\emptyset}$ is proved from membership: $\emptyset\in{\emptyset}$ but $\emptyset\notin\emptyset$. Injectivity of the witness is the remaining algebraic fact that makes the embedding faithful before the full system record is assembled.
proof idea
Introduce $a,b:\mathrm{Bool}$ with $w(a)=w(b)$. Case-split on both Booleans. After unfolding the witness definition, the equal-token diagonals close by reflexivity. The two off-diagonal cases reduce to $\emptyset={\emptyset}$ or its symmetric form; each is absurd by the prior lemma that empty differs from singleton-empty. No induction or external injectivity lemmas are required.
why it matters
Faithfulness of the token embedding is a prerequisite for treating ZFC as a concrete FormalSystem instance inside PRC: discrimination must track real set inequality, and endpoints must be the genuine empty set and its singleton. Sibling constructions in the same module (the ZFC system record, expressiveness, and the embedding of the distinction relation $\delta$) sit on top of this injectivity. In the broader Recognition stack, PRC is the foundation layer that forces recognition structure before the T0–T8 chain; a verified ZFC parse shows that classical set theory can host the distinction calculus without collapsing tokens. No downstream consumers are wired yet in the graph, so this is currently a local building block rather than a cited lemma higher up.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.