RealizesDelta
plain-language theorem explainer
A formal system realizes the δ core precisely when a Primitive Recognition Calculus embedding into its own interface exists (nonempty embedding type). Anyone citing the distinction dichotomy or the δ4 headline that distinction is not optional uses this predicate as the positive horn. The body is a one-line definitional unfolding of embedding nonemptiness.
Claim. A formal system $F$ realizes the $\delta$ core when there exists a PRC embedding into $F$: maps of primitive endpoints and finite traces into $F$'s tokens and expressions that preserve the left/right endpoint distinction and trace extension.
background
The Primitive Recognition Calculus (PRC) treats recognition as a minimal formal interface. A FormalSystem supplies verifier-side carriers Token and Expr, a binary distinction relation on tokens, an expression-extension order, and a map from abstract endpoints into tokens. That interface is exactly what the inevitability theorems quantify over.
A PRC embedding into such a system is a structure that sends the two primitive endpoints to tokens and finite traces to expressions while preserving the left/right distinction and finite trace extension. The present definition packages existence of that structure as a single proposition: the foundation "realizes δ" on its own interface.
Locally this sits in the distinction-dichotomy module, which separates foundations that can tell two objects apart from those that cannot (the degenerate case).
proof idea
Pure definition: the predicate is definitionally Nonempty (PRCEmbeddingInto F). No tactics, no lemmas. Downstream proofs obtain a witness by obtain ⟨emb⟩ := h and then read off emb.preserves_distinction (or build an embedding by hand from a distinguished pair when the system is discriminating and expression order is reflexive).
why it matters
This is the positive side of the δ dichotomy. It is the right disjunct in distinction_dichotomy (any foundation with reflexive expression order is either degenerate or realizes δ) and the left-hand side of the biconditional in distinction_not_optional (δ4 headline: distinction is not optional except for the fully degenerate foundation). It also feeds not_degenerate_of_realizesDelta, the constructive bridge realizesDelta_of_discriminating, and the shrunk δ-certificate bundle.
In the broader Recognition Science forcing picture, realizing δ is the formal-system face of the claim that a non-trivial foundation must already carry the primitive left/right distinction that the eight-tick / Cl₈ story later geometrizes. Without this predicate the inevitability theorems have nothing to assert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.