set_theory_with_infinity_realizes_delta
plain-language theorem explainer
Full ZFC with infinity modelled realizes the δ-core: von Neumann ω contains ∅ and is closed under successor, and a PRC embedding into the parsed ZFC formal system exists. Foundation workers comparing the set-theoretic leg against type and category parses would cite this. The proof is a one-line pairing of the infinity-model theorem with the ZFC δ-embedding theorem, lifting the HF caveat that infinity was not modelled.
Claim. The empty set lies in the von Neumann ordinal $\omega$, and $\omega$ is closed under successor $n \mapsto n \cup \{n\}$; moreover there is a nonempty PRC embedding of the $\delta$-core into the formal system obtained by parsing full ZFC over Mathlib's $\mathrm{ZFSet}$.
background
Primitive Recognition Calculus (PRC) isolates a minimal δ-core: two distinguished endpoints and finite traces that extend. A formal system realizes that core when there is a PRCEmbeddingInto it: maps on endpoints and traces that preserve distinction and trace extension.
The full-ZFC parse builds a FormalSystem whose tokens inject into Mathlib's ZFSet (universe 0), whose discrimination relation is genuine ZF extensional difference, and whose endpoints are the real ∅ and {∅}. Upstream, infinity_modeled records that von Neumann ω contains ∅ and is closed under insert n n (the successor x ↦ x ∪ {x}); that is exactly the axiom of infinity HF set theory could not supply. Separately, zfSystem_embeds_delta asserts Nonempty (PRCEmbeddingInto zfSystem) once the system is shown expressive enough.
This module packages the three classical foundations (set theory, type theory, category theory) as parsed formal systems and records which of them realize δ.
proof idea
Term-mode pair constructor. The first conjunct is exactly FullZFCParse.infinity_modeled (itself ⟨ZFSet.omega_zero, fun _ h => ZFSet.omega_succ h⟩). The second conjunct is exactly FullZFCParse.zfSystem_embeds_delta, which applies the general embedding-target lemma to zfSystem once expressiveness is established. No further rewriting or case analysis.
why it matters
Closes the set-theory leg of the foundations parse at full strength. The HF parse could only realize δ with the caveat that infinity is not modelled; this declaration lifts that caveat by pairing the modelled axiom of infinity with a genuine PRC embedding into full ZFC. Sibling results in the same module (three_foundations_realize_delta, three_foundations_not_degenerate, three_foundations_own_distinction) compare the three classical foundations as δ-carriers; this theorem is the set-theoretic half of that comparison. In the broader Recognition stack it shows that ordinary ZFC, once infinity is present, already contains the primitive endpoint distinction the forcing chain later specializes (T5 J-uniqueness through T8 dimension). No downstream users are recorded yet; the immediate role is foundational bookkeeping rather than a physics constant derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.