Side
plain-language theorem explainer
A two-valued type naming the two poles of a primitive distinction: left and right. Anyone building the δ-core, endpoints, or FormalSystem parsers cites it as the atomic label set. It is a bare inductive definition with decidable equality, not a proved claim.
Claim. There is a type $\mathrm{Side}$ with exactly two inhabitants, $\mathrm{left}$ and $\mathrm{right}$, equipped with decidable equality. These are the two sides forced by a primitive distinction (K2.2).
background
Primitive Recognition Calculus treats a distinction as the minimal act that splits experience into two poles. Before endpoints, traces, or formal-system embeddings are defined, one needs a name for those poles.
Side is that name: an inductive type with constructors left and right. The module sits in Foundation.PrimitiveRecognitionCalculus.Basic and imports only Mathlib plus a Strength helper. Downstream, an endpoint is defined as a structure whose sole field is a side (K2.3), so every later map from endpoints into tokens of a formal system is ultimately a choice of side.
The same two labels reappear when discriminating foundations realize the δ-core: one relabels the primitive endpoints onto a distinguished pair by matching on side.
proof idea
No proof. This is an inductive definition with two nullary constructors, deriving DecidableEq and Repr. There is nothing to discharge.
why it matters
Side is the atomic carrier for the δ-core of Primitive Recognition Calculus. Endpoint is built directly on it (side : Side), and left/right endpoint constants are the canonical inhabitants.
Downstream parsers for topos theory, hereditarily finite set theory, and full ZFC all route endpoint tokens through a match on side, sending left and right to ⊤/⊥, ∅/{∅}, or analogous distinguished pairs. The dichotomy theorem that every discriminating foundation with a reflexive expression order realizes δ likewise matches on e.side when building the endpoint map.
In the broader Recognition chain this is pre-physics scaffolding: it fixes the binary split that later forcing steps (T5–T8, RCL, eight-tick octave) presuppose when they talk about distinction and cost. It does not itself force φ, dimension, or any constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.