zfSystem_not_degenerate
plain-language theorem explainer
Full ZFC, parsed as a formal system with genuine extensional discrimination, is non-degenerate: it distinguishes at least one pair of tokens. Anyone placing ZFC on the δ side of the distinction dichotomy cites this. The proof is a one-line application of the general fact that realizing δ precludes degeneracy, using the already-proved δ-embedding for the ZFC system.
Claim. The formal system obtained by parsing full ZFC (Mathlib $\mathrm{ZFSet}$ at universe $0$) is not degenerate: its discrimination relation is nonempty, so there exist tokens it can tell apart.
background
In the Primitive Recognition Calculus, a formal system is degenerate when its discrimination relation is empty: it cannot tell any two tokens apart. The distinction dichotomy splits foundations into that empty case and those that realize δ, a minimal two-endpoint distinction core.
The ZFC system packages full ZFC into the formal-system interface: tokens are a small carrier injected into the ZF universe, discrimination is genuine ZF extensional difference of the represented sets, and the endpoints are the real empty set and its singleton. Upstream, realizing δ is incompatible with degeneracy: if a system embeds the δ core, the embedding's preserved distinction witnesses a nonempty discrimination relation ("Realizing δ entails discrimination: the two cases are mutually exclusive").
proof idea
One-line term proof. Apply the general lemma that any formal system realizing δ is non-degenerate, supplying the already-established fact that the ZFC system embeds (hence realizes) δ. That general lemma unpacks the embedding witness and feeds its preserved distinction into the universal quantifier in the degeneracy predicate, yielding an immediate contradiction.
why it matters
This pins full ZFC on the non-degenerate, δ-realizing side of the distinction dichotomy in the Primitive Recognition Calculus. The companion packaging note records that the same parse satisfies extensionality, has $\emptyset \neq {\emptyset}$, discriminates by genuine extensional difference, models the axiom of infinity ($\omega$ with empty set and successor closure), and realizes the δ core. With no downstream dependents yet recorded, the result is a leaf certification that classical set theory is not a degenerate foundation under the PRC parse, and that standard mathematical foundations fall on the expressive side of the dichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.