endpoint_eq_left_or_right

In the Primitive Recognition Calculus, a distinction is the atomic act of separating two sides. An endpoint is defined as a side of that primitive distinction: the structure Endpoint wraps a Side value, and the two canonical inhabitants are the left and right endpoints of $\delta$.

The local module develops the one-primitive setting: judgments generated by a single distinction, with same and diff forced by the act. The two-endpoint character of that type is the combinatorial fact this lemma records. Upstream, Endpoint is introduced as K2.3 ("a side of the primitive distinction"); the present statement makes the exhaustiveness of those two sides explicit for later equality forcing.

Term/tactic hybrid by structure elimination. Unpack the endpoint to its underlying Side field, then case-split on the two constructors of Side. The left case yields the left disjunct by reflexivity; the right case yields the right disjunct. No external lemmas are required beyond the inductive definition of Side and the structure of Endpoint.

This is the elementary exhaustiveness fact that the core forcing lemma genuine_judgment_same_is_equality relies on. That downstream result states: on the two-endpoint type, a TraceJudgment whose diff separates left from right, and whose same is complementary to diff, collapses same to equality. Without knowing every endpoint is left or right, the case analysis that forces $a = b$ from $J.\mathrm{same},T,a,b$ cannot close.

In the Recognition Science foundation, the primitive distinction is the seed of the forcing chain (toward T5 J-uniqueness and the later octave/dimension steps). Recording that a distinction has exactly two endpoints keeps the one-primitive calculus tight: comparison is derived, not primitive, and equality is the only admissible "same" on this carrier.