genuine_judgment_same_is_equality
plain-language theorem explainer
On the two-endpoint type, any tight separating TraceJudgment has same coinciding with equality of endpoints. Anyone arguing that recognition is a single primitive (Item 5) cites this forcing step. The proof is a four-case exhaustion on left/right after deriving that left is not same as right.
Claim. Let $J$ be a trace judgment whose same-relation is reflexive and symmetric. Suppose $J$ is tight ($J.\mathrm{diff}\,T\,a\,b \leftrightarrow \neg J.\mathrm{same}\,T\,a\,b$) and separating ($J.\mathrm{diff}\,T\,\mathrm{left}\,\mathrm{right}$ for every trace $T$). Then for every trace $T$ and endpoints $a,b$, one has $J.\mathrm{same}\,T\,a\,b \leftrightarrow a = b$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction $\delta$ (left or right). A trace is a finite word in distinction acts: empty or extended by one act. A TraceJudgment packages, for each trace, a same-relation and a diff-relation on endpoints, together with admissibility fields (reflexivity and symmetry of same are the ones used here).
Tightness says diff is exactly the negation of same. Separation says the two geometric sides left and right are always judged different. The module sits in the foundation layer that reduces recognition to a single act-generated primitive rather than an independent same/different comparator.
Upstream, Endpoint and Trace are the K2.3–K2.4 carriers: endpoints are sides of $\delta$, traces are act-generated histories. The two-point geometry is what makes the forcing work: there are only four endpoint pairs to check.
proof idea
From tightness and separation, left is not same as right on $T$. The biconditional is proved by constructor.
Forward: assume same on $a,b$. Case-split each endpoint via the sibling fact that every endpoint is left or right, then substitute. Same-side pairs give reflexivity (equality). Cross pairs contradict the derived non-sameness of left and right, using symmetry of same for the right-left order.
Backward: if $a=b$, substitute and apply reflexivity of same from the judgment's admissibility fields. No other structure of $J$ is needed.
why it matters
This is the core forcing lemma behind Item 5 of the one-primitive program. Its sole downstream consumer is comparison_is_derived_not_primitive, whose doc-comment states the resolution: for any judgment that is an equivalence (admissibility), tight, and separating, same is forced to be the decidable equality carried by the act-generated structure, so the same/different judgment is derived from the act, not an independent second primitive.
In Recognition Science terms, the result closes the door on treating comparison as a second foundation alongside distinction. It feeds the Primitive Distinction reduction path (from many axioms toward fewer structural conditions) by showing that once the act generates the two-endpoint type, equality is the only admissible tight separating same-relation. No T5–T8 constants are involved; the lemma is pure foundation geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.