peanoSystem_embeds_delta
plain-language theorem explainer
Peano arithmetic carries a structure-preserving embedding of the primitive recognition δ-core: the two endpoints and finite traces map into tokens and expressions while keeping the left/right distinction. Anyone arguing that the primitive distinction is foundation-independent cites this instance. The proof is a one-line specialization of the generic two-distinct-primitives lemma to the pair 0 ≠ 1.
Claim. There exists a PRC embedding into the Peano formal system: a map of endpoints to tokens and traces to expressions that preserves the primitive left/right distinction and finite trace extension. The Peano system is the formal system generated by the two distinct naturals $0$ and $1$.
background
The Primitive Recognition Calculus (PRC) isolates a minimal δ-core: two distinguished endpoints and finite traces that extend while keeping that distinction. A formal system is a token/expression carrier equipped with a distinguishability relation. A PRC embedding into such a system is a pair of maps (endpoints to tokens, traces to expressions) that preserve distinction and trace extension.
The Peano instance is built as the two-distinct formal system on the naturals with witness $0 \neq 1$, the first arithmetic separation. Upstream, the generic lemma states that any foundation exposing two distinguishable primitives realizes the δ-core: nonempty PRC embedding into the two-distinct system they generate. That lemma is the sole substantive input here; the Peano system is just that construction at $(0,1)$.
proof idea
One-line term proof. Apply the generic theorem that any two distinguishable primitives yield a nonempty PRC embedding into their two-distinct formal system, specializing the carrier to $\mathbb{N}$ with witnesses $0$ and $1$, and discharging $0 \neq 1$ by decide. No further case analysis or construction is needed; the embedding witness is inherited from the generic argument via the expressive two-distinct system.
why it matters
This is the arithmetic leg of Item 4 in the inevitability instances: the primitive distinction is not an artifact of one notation. Downstream, named_foundations_embed_delta conjoins this with the Boolean, set-theoretic, and type-theoretic legs to assert that four structurally different foundations each realize δ. The dichotomy theorem then uses the same fact to place Peano on the non-degenerate side: realizing δ implies not degenerate.
In the broader Recognition forcing picture, this supports the claim that the ledger-level distinction (the δ that later feeds the J-cost and the T0–T8 chain) appears wherever a foundation can tell two primitives apart, including ordinary Peano arithmetic. It does not itself force $\phi$, the eight-tick, or $D=3$; it only anchors the arithmetic instance of the δ-core those later steps presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.