Endpoint
plain-language theorem explainer
An endpoint is just a labeled side of the primitive distinction δ: left or right. Anyone building the Primitive Recognition Calculus, formal-system embeddings, or expressivity predicates cites it as the atomic carrier of that binary cut. The declaration is a one-field structure over Side, with canonical constructors for the two poles.
Claim. An endpoint is a side of the primitive distinction $\delta$. Formally it is a structure carrying a single field of type $\mathrm{Side}$, where $\mathrm{Side}$ is the two-element type $\{\mathrm{left},\mathrm{right}\}$. The canonical endpoints are $\mathrm{left}$ and $\mathrm{right}$.
background
Primitive Recognition Calculus begins with a forced binary cut. K2.2 introduces $\mathrm{Side}$ as the inductive type with constructors left and right: the two poles any distinction must present. K2.3 packages that pole as an endpoint, so later layers can talk about tokens, maps, and distinctions without reopening the inductive definition of Side.
The surrounding module builds finite traces by successive distinction acts and records extension relations on those traces. Endpoints are the vertices those acts connect. Downstream, a minimal formal-system interface exposes an endpointToken map from endpoints into an arbitrary token type, and expressivity is exactly the ability to distinguish the images of the two endpoints.
No analytic cost functional appears yet. This layer is purely combinatorial scaffolding for the inevitability argument that any sufficiently expressive formal system must already contain the primitive distinction.
proof idea
Definitional, not a proof. The structure has one field side : Side and derives decidable equality and a printer. Two abbreviations supply the poles: left is the structure value with side left, right with side right. No lemmas are invoked.
why it matters
Endpoints are the atomic vocabulary of the PRC inevitability pass. The formal-system interface requires an endpointToken : Endpoint → Token map; a system is expressive precisely when it distinguishes the tokens of left and right. PRC embeddings demand that the endpoint map preserve that distinction, and the native PRC formal system takes Token to be Endpoint itself with inequality as distinction.
Those interfaces feed every later claim that a host calculus can see δ and finite trace extension. Usage also reaches circle-winding and cosmology staging modules that import the same carrier. In the broader Recognition chain this sits before J-uniqueness (T5), φ-forcing (T6), and the eight-tick octave (T7): it is the discrete cut those analytic steps presuppose, not a substitute for them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.