actJudgment
plain-language theorem explainer
Names the act-forced same/diff judgment on traces: sameness is endpoint equality and difference is disequality, both read off the act-generated structure. Anyone proving that comparison is not a second recognition primitive cites this binding. It is a one-line alias of the verifier equality model of the TraceJudgment interface.
Claim. Define the act-forced trace judgment to be the verifier model in which, for every trace $T$ and endpoints $a,b$, sameness means $a=b$ and difference means $a\neq b$ (with reflexivity of sameness immediate).
background
In the Primitive Recognition Calculus, a trace judgment is an admissible same/diff surface on endpoints of a trace: object-level sameness, object-level witnessed difference, and the usual admissibility constraints (reflexivity of same, and related fields). The module develops the claim that recognition is one primitive: the act generates the structure on which comparison is computed, so same/diff is not an independent second primitive.
Upstream, the verifier equality judgment is a Lean-level model of that interface: same is ordinary equality of endpoints, diff is disequality, with reflexivity proved by rfl. The doc-comment stresses that this model is not PRC's object-level primitive; it is a sanity inhabitant of the interface in the verifier language. The present definition simply installs that model as the judgment the act forces, so later lemmas can speak of act-forced same and diff without reopening the interface.
proof idea
One-line definitional alias: the act judgment is set equal to the verifier equality judgment. No tactics or lemmas are applied; all content (same as $=$, diff as $\neq$, reflexivity) is inherited from that upstream definition.
why it matters
This binding is the named carrier for Item 5 of the one-primitive program. Downstream, actJudgment_same and actJudgment_diff are definitional iff-facts ($\mathrm{same}\leftrightarrow{=}$, $\mathrm{diff}\leftrightarrow{\neq}$), and decidability of same reduces to decidable equality on the freely generated endpoint type: compare needs no second primitive, only decide on act-generated structure.
The core forcing theorem then shows that any tight, separating equivalence judgment is forced to this same relation, so comparison is derived from the act. That statement is load-bearing clause (A) of the shrunk PRC certificate: recognition is one primitive. In the broader Recognition Science foundation, this is the formal sense in which the recognition act alone generates the same/diff surface used later in the forcing chain, rather than positing an independent comparison primitive beside the act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.