actJudgment_same
plain-language theorem explainer
For any finite recognition trace and any two endpoints, the act-forced "same" judgment holds if and only if the endpoints are equal. This is the definitional core of the one-primitive calculus: sameness is not an extra relation, it is equality on the act-generated structure. Anyone citing the Item 5 resolution (comparison derived, not primitive) needs this bridge. The proof is pure definitional reflexivity.
Claim. Let $T$ be a finite recognition trace and let $a,b$ be endpoints (sides of the primitive distinction). Writing $\mathsf{same}_T$ for the "same" component of the act-forced judgment, one has $\mathsf{same}_T(a,b)\leftrightarrow a=b$.
background
In the Primitive Recognition Calculus, an endpoint is a side of the primitive distinction $\delta$ (left or right). A finite trace is built from the empty history by successive distinction acts. The act-forced judgment is the TraceJudgment whose "same" and "diff" components are the equality and disequality relations on those endpoints, both decidable from the act-generated structure.
The local module isolates the claim that recognition has a single primitive: the distinction act. Comparison (same versus different) is not introduced as a second free primitive; it is read off the act. The present lemma records the equality half of that reading: the act judgment's "same" predicate is literally endpoint equality.
proof idea
One-line definitional proof. The act judgment is defined to be the verifier equality judgment, whose "same" field is propositional equality of endpoints. Unfolding that definition makes the biconditional hold by Iff.rfl; no lemmas are applied.
why it matters
This lemma is the equality half of the bridge used by comparison_is_derived_not_primitive (Item 5 resolution). That parent theorem states: for any judgment that is an equivalence (tight same/diff) and separating (left differs from right on every trace), the "same" relation is forced to be the decidable equality carried by the act-generated structure. Hence same/different is derived from the act, not an independent second primitive.
In the broader Recognition Science forcing picture this is foundation-level bookkeeping: before J-cost uniqueness (T5), the eight-tick octave (T7), or D=3 (T8), one must fix that the recognition calculus has one generative act and that comparison is not smuggled in as a second free notion. The lemma pins that bookkeeping at the definitional level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.