ofTwoDistinct
plain-language theorem explainer
Any type with two unequal elements yields a minimal formal system for the PRC inevitability theorem: tokens are the type's carriers, expressions are natural numbers (trace lengths), and the two endpoints are the given primitives. Downstream witnesses for Boolean logic, Peano arithmetic, set theory, and type theory are instances of this constructor. The body is a structure instance that wires each FormalSystem field to the obvious carrier data.
Claim. Given a type $\alpha$ and two elements $a_0,a_1\in\alpha$ with $a_0\neq a_1$, there is a formal system whose token type is $\alpha$, whose expression type is $\mathbb{N}$, whose distinction relation is inequality on tokens, whose expression-extension relation is $\le$ on $\mathbb{N}$, and whose left and right endpoint tokens are $a_0$ and $a_1$ respectively. Trace length supplies the expression assigned to a finite trace, and length is monotone under trace extension.
background
The Primitive Recognition Calculus (PRC) studies when an arbitrary formal system is forced to contain the primitive distinction $\delta$. The minimal interface is a structure with a token type, an expression type, a binary distinction predicate on tokens, an expression-extension relation, a map from the two geometric endpoints (left/right sides of a distinction) to tokens, and a map from finite traces to expressions that respects extension.
A finite trace is either empty or obtained by extending a prior trace by one distinction act. Trace length is the obvious inductive count (empty has length $0$; each extension adds one). The two sides of a distinction are the inductive type with constructors left and right; endpoints are those sides.
This module builds concrete FormalSystem instances used by the inevitability theorem. The local lemma that finite-trace length is monotone under the trace-extension relation is the only nontrivial obligation when expressions are taken to be lengths.
proof idea
Pure structure construction, not a tactic proof. Token is the ambient type $\alpha$; Expr is $\mathbb{N}$; distinguishes is propositional inequality; exprExtends is $\le$ on naturals. The endpoint map sends left to $a_0$ and right to $a_1$. The trace-to-expression map is Trace.length. The sole proof obligation, that length respects extension, is discharged by applying the upstream monotone-length lemma length_le_of_extends. The inequality hypothesis $a_0\neq a_1$ is carried only as a parameter (used by the companion expressivity theorem, not inside the structure fields themselves).
why it matters
This is the generic factory for foundation-flavored PRC witnesses. Boolean logic is the instance on false/true; Peano arithmetic is the instance on $0\neq 1$; set foundation is the instance on $\emptyset\neq\mathrm{univ}$ over a one-point domain; type theory is the analogous two-point carrier. Each of those systems then inherits expressivity (the two endpoints are distinguished) and a nonempty PRC embedding, so they land on the $\delta$ side of the distinction dichotomy.
Downstream, the expressivity theorem for this constructor, the reflexivity of expression extension on it, and the concrete embedding theorems for logic/arithmetic/sets/types all cite this definition. In the Recognition forcing picture it supplies the formal-system side of the claim that any non-degenerate foundation already contains the primitive two-sided distinction that PRC treats as inevitable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.