three_foundations_own_distinction
plain-language theorem explainer
Each of the three classical foundations carries a native binary-distinction law: set-theoretic extensionality on HF codes, type-theoretic canonicity of the two-element type, and categorical classification of the terminal subobject. Anyone comparing how set theory, type theory, and category theory encode the δ distinction would cite this packaging. The proof is a one-line product of the three already-proved lemmas.
Claim. Natural-number HF codes satisfy $m = n$ if and only if they have the same members; every closed term $b$ of the two-element type is either $\mathsf{false}$ or $\mathsf{true}$; and the subobject classifier sends the constantly-true predicate on the terminal object to $\mathsf{True}$.
background
The Primitive Recognition Calculus (PRC) parses three classical foundations so each can host the same δ distinction core. On the set-theory leg, hereditarily finite sets are coded by natural numbers via the Ackermann interpretation; membership is bit-testing, and equality is bit-extensionality. On the type-theory leg, the two-element type is Lean's Bool, with constructors false and true. On the category-theory leg, subobjects of the terminal object Unit are predicates Unit → Prop, and the classifier Ω records their characteristic truth value.
Upstream, ext_iff states that two HF codes are equal iff they have the same members ("exactly ℕ bit extensionality"). canonicity states that every closed term of the two-element type is one of the two constructors. classifies_top is the trivial evaluation that the constantly-true predicate classifies as True. This theorem simply conjoins those three native distinction laws.
proof idea
Term-mode one-liner. The goal is a three-way conjunction, so the proof is the triple of upstream lemmas: set-theoretic extensionality (ext_iff), type-theoretic canonicity of the two-element type (canonicity), and categorical classification of the top subobject (classifies_top). No further rewriting or case analysis is performed here.
why it matters
In the PRC foundations program, δ is the minimal distinction that any foundation must own. The doc-comment frames this result as proving that "each is the foundation's own way of telling its two primitives apart, and each yields the δ distinction." Sibling results package related claims: that the three foundations realize δ, that they are non-degenerate, and that full ZFC with infinity also realizes δ.
No downstream consumers are recorded yet; the declaration is a citation anchor for the three-foundation comparison rather than a stepping stone in a longer chain. It sits at the foundation layer of Recognition Science, before the forcing chain (T0–T8) and the Recognition Composition Law, by fixing how classical foundations already encode binary distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.