two_distinct_realizes_delta
plain-language theorem explainer
Any type with two unequal elements yields a formal system that admits a Primitive Recognition Calculus embedding of the δ core. Foundations researchers cite it to discharge Item 4 of the PRC inevitability list for arbitrary two-valued carriers. The proof is a one-line application of the general expressive-to-embedding theorem to the two-distinct instance.
Claim. For any type $\alpha$ and any $a_0, a_1 \in \alpha$ with $a_0 \neq a_1$, the formal system whose tokens are elements of $\alpha$, whose expressions are natural numbers ordered by length, and whose endpoints map to $a_0$ and $a_1$, admits a nonempty PRC embedding: there exist maps of endpoints and finite traces that preserve endpoint distinction and trace extension.
background
Primitive Recognition Calculus (PRC) isolates a minimal δ core: two distinguished endpoints (left/right) and finite traces that extend by length. A formal system is a carrier of tokens and expressions equipped with a distinction predicate and an expression-extension relation. A PRC embedding into such a system is a pair of maps (endpoints to tokens, traces to expressions) that preserve distinction of the two endpoints and monotonicity of trace extension.
The construction ofTwoDistinct builds a formal system from any type with two named unequal elements: tokens are the type's elements, expressions are natural numbers with the usual order as extension, and the two endpoints are sent to the two named elements. Expressiveness of a formal system means precisely that those two endpoint tokens are distinguished.
Upstream, FormalSystemEmbeddingTarget_proved states that every expressive formal system admits a PRC embedding (via PRCEmbeddingInto.ofExpressive). The companion lemma ofTwoDistinct_expressive records that the two-distinct construction is expressive exactly because $a_0 \neq a_1$.
proof idea
One-line term proof. Apply FormalSystemEmbeddingTarget_proved to the formal system ofTwoDistinct a₀ a₁ hne, supplying the expressiveness witness ofTwoDistinct_expressive a₀ a₁ hne. The general theorem returns a nonempty PRCEmbeddingInto structure; no further case analysis is required.
why it matters
This is Item 4 (generic) of the PRC inevitability instances: any foundation that exposes two distinguishable primitives realizes the δ core. Downstream it is the single workhorse for the concrete embeddings of Peano arithmetic (0 ≠ 1), set foundation (∅ ≠ univ on a one-point domain), and type theory (inl () ≠ inr () on Unit ⊕ Unit). Those three theorems, together with the Boolean two-valued carrier, widen Item 4 to four structurally different foundations, all forced to host the same endpoint distinction that PRC treats as primitive. In the Recognition Science forcing chain this sits at the foundation layer beneath T5–T8: before J-cost uniqueness, φ, the eight-tick octave, or D = 3 can be forced, the formal substrate must already distinguish two endpoints. The lemma closes that substrate obligation for every two-valued carrier without specializing the ambient logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.