named_foundations_embed_delta
plain-language theorem explainer
Four standard foundations each admit a Primitive Recognition Calculus embedding: two-valued logic, Peano arithmetic via 0≠1, set theory via ∅≠{∅}, and type theory via the two-point type. Anyone arguing that the δ-core is foundation-independent would cite this. The proof is a four-way packing of the individual embedding theorems already proved for each carrier.
Claim. There exist PRC embeddings into each of four formal systems: the two-valued Boolean carrier, Peano arithmetic on $\mathbb{N}$ with $0 \neq 1$, a set-theoretic carrier with $\emptyset \neq \{\ast\}$, and a type-theoretic carrier based on the two-point type. Equivalently, each of these foundations realizes the primitive endpoint distinction $\delta$.
background
Primitive Recognition Calculus (PRC) isolates a minimal distinction: two endpoints (left and right) that a formal system can tell apart, together with finite traces that extend that distinction. A PRC embedding into a formal system $F$ is a pair of maps (endpoints to tokens, traces to expressions) that preserve the endpoint distinction and finite trace extension.
The local module builds concrete FormalSystem witnesses from any two distinct values via a two-point construction. Boolean logic uses false and true; Peano uses $0,1\in\mathbb{N}$; set theory uses $\emptyset$ versus the universe on a one-point domain (the von Neumann $0$ vs $1$ seed); type theory uses the two-point type. Each individual system already has a proved Nonempty embedding theorem.
Upstream, the structure PRCEmbeddingInto records exactly the preservation obligations. The sibling theorems boolLogicSystem_embeds_delta, peanoSystem_embeds_delta, setFoundationSystem_embeds_delta, and typeTheorySystem_embeds_delta discharge those obligations one foundation at a time.
proof idea
Term-mode packing, not a new argument. The proof is the four-tuple of existing Nonempty witnesses:
boolLogicSystem_embeds_delta (via the expressive Boolean carrier), peanoSystem_embeds_delta (via two_distinct_realizes_delta on $0\neq 1$), setFoundationSystem_embeds_delta (via $\emptyset\neq\mathrm{univ}$ on Unit), typeTheorySystem_embeds_delta (the type-theoretic two-point case).
No further tactics: inhabit the four-fold conjunction by citing those four theorems.
why it matters
Doc-comment labels this Item 4, widened: the primitive distinction is not an artifact of one foundation's notation. It appears wherever two primitives can be told apart. That is the inevitability claim for the δ-core across logic, arithmetic, sets, and types.
In the Recognition Science foundation layer this supports the claim that the forcing chain's starting distinction is portable: any setting rich enough to separate two tokens already hosts a PRC embedding. Downstream use is not yet wired in this module (used_by is empty), so the result presently stands as a consolidated citation point for the four concrete embeddings rather than a lemma inside a larger proof.
It does not touch T5–T8 (J-uniqueness, φ, eight-tick, D=3) directly; it sits earlier, at the formal-system substrate on which those forcing steps are later stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.