typeTheorySystem

The Primitive Recognition Calculus (PRC) inevitability layer works against a thin formal-system interface: a token type, an expression type, a distinction relation on tokens, an extension preorder on expressions, and a map from abstract endpoints to tokens. That interface is enough to ask whether the primitive distinction δ is visible inside the system.

The two-distinct constructor builds such a system from any type with two unequal elements: tokens are the type's elements, distinction is inequality, expressions are natural-number lengths, and extension is ≤. Endpoint tokens are the two chosen primitives.

Here the carrier is the type-theoretic two-point type $\mathbf{2} = \mathrm{Unit} \oplus \mathrm{Unit}$, whose left and right injections are definitionally distinct closed terms. This is the type-theory instance parallel to Boolean logic, Peano arithmetic ($0 \neq 1$), and set theory ($\emptyset \neq {\emptyset$).

One-line definitional wrapper. Instantiate the two-distinct formal-system builder at $\alpha = \mathrm{Unit} \oplus \mathrm{Unit}$ with $a_0 = \mathsf{inl}(\star)$ and $a_1 = \mathsf{inr}(\star)$, discharging $a_0 \neq a_1$ by decide. No further lemmas.

Supplies the type-theory leg of the four named foundations in the PRC inevitability instances. Downstream, the companion embedding theorem shows a nonempty PRC embedding into this system (via the generic two-distinct realizes-δ lemma). That fact is conjoined in the widened Item-4 theorem: Boolean logic, Peano arithmetic, set theory, and type theory each realize the δ core, so the primitive distinction is not an artifact of one foundation's notation. It also feeds the dichotomy theorem that all four named foundations are non-degenerate (hence lie on the δ side). Within Recognition Science this is foundation-layer scaffolding for the forcing chain: before T5–T8 force J, φ, the eight-tick octave, and D = 3, one needs that any non-degenerate formal substrate already carries a primitive distinction.