three_foundations_not_degenerate
plain-language theorem explainer
HF set theory, type theory, and the topos of sets are each non-degenerate as formal systems: each can distinguish at least one pair of tokens. Anyone citing the three-foundation parse of the distinction dichotomy needs this conjunction. The proof is a three-component term packaging the individual non-degeneracy lemmas.
Claim. Neither hereditarily finite set theory, nor type theory, nor the topos-of-sets foundation is degenerate: for each parsed system $F$, it is not the case that $\forall a,b\colon F.\mathrm{Token},\; \neg F.\mathrm{distinguishes}(a,b)$. Equivalently, each foundation can tell at least one pair of tokens apart.
background
The Primitive Recognition Calculus parses classical foundations into a common FormalSystem interface: tokens, a discrimination relation, endpoints, and an expression-order. Degeneracy means the discrimination relation is empty: the foundation cannot tell any two tokens apart.
HF set theory is parsed with natural-number codes as tokens and extensional inequality as discrimination, endpoints $\emptyset$ and ${\emptyset}$. The topos parse takes global points of the subobject classifier $\Omega$ as tokens, with inequality of truth values as discrimination and endpoints $\top$ and $\bot$. Type theory is parsed analogously (canonicity supplies the distinction).
The distinction dichotomy splits foundations into those that realize a genuine $\delta$-distinction and those that are degenerate. Upstream lemmas already show each of the three parses is non-degenerate, typically by realizing $\delta$ and invoking the general fact that realizing $\delta$ precludes degeneracy.
proof idea
One-line term proof: the conjunction is assembled as the triple of the three existing non-degeneracy theorems
hfSystem_not_degenerate,
ttSystem_not_degenerate, and
toposSystem_not_degenerate.
No new reasoning; each conjunct is discharged by its dedicated upstream lemma (the topos case via not_degenerate_of_realizesDelta applied to the $\delta$-embedding).
why it matters
Packages the non-degeneracy half of the three-foundation story: set theory (extensionality), type theory (canonicity), and category theory (subobject classification) each land on the $\delta$ side of the distinction dichotomy rather than collapsing. Sibling results cover realizing $\delta$ and owning the distinction mechanism; together they underwrite the claim that the substantive distinction mechanism of each foundation is proved.
In the Recognition Science foundation layer this is bookkeeping for the claim that standard foundations are not vacuous under the PRC parse. It does not itself force $J$, $\varphi$, the eight-tick octave, or $D=3$; those sit later in the forcing chain (T5–T8). No downstream consumers are recorded yet; the lemma is a conjunction point for the three parses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.