actJudgment_same_decidable
plain-language theorem explainer
The act-generated "same" judgment on two endpoints of a finite trace is a decidable proposition. Anyone wiring automation, `decide`, or case splits over the primitive recognition calculus cites this instance. The proof unfolds the judgment to ordinary endpoint equality and reuses the existing `DecidableEq` instance on endpoints.
Claim. For every finite trace $T$ and endpoints $a,b$, the proposition that the act-generated judgment declares $a$ the same as $b$ is decidable (i.e.\ one can algorithmically answer yes or no from the inductive structure alone).
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction (left or right), and a finite trace is built from the empty trace by successive distinction acts. Both carry derived equality and decidable equality from their inductive presentations.
The act-generated judgment package records, for a fixed trace, when two endpoints are judged the same or different. By construction the "same" clause is ordinary equality of endpoints: no extra relational data is stored. The surrounding module argues that comparison is therefore not a second primitive; it is decision on a freely generated type.
Upstream, Endpoint is declared with DecidableEq, so Lean already knows how to decide $a=b$. This instance simply exposes that fact at the judgment interface.
proof idea
One-line wrapper. The goal Decidable (actJudgment.same T a b) is rewritten, by definitional unfolding of the act-generated same-clause, to Decidable (a = b). The proof then calls inferInstance, which finds the DecidableEq Endpoint instance already derived on the endpoint structure. No case analysis on the trace is required.
why it matters
This instance is the computational half of the claim that "compare needs no second primitive": once endpoints and traces are freely generated, sameness is decide on equality, not a new ontological act. The module doc-comment states exactly that formal sense.
It sits beside the core forcing lemma that an admissible equivalence on the two-endpoint type which never relates left to right must be equality (using only reflexivity and symmetry from the judgment admissibility fields), and beside the sibling that comparison is derived rather than primitive. Together they support the PRC one-primitive thesis in the Foundation layer: distinction acts generate the type, and judgment is recovered by decidable equality rather than by an independent comparison operator of the kind appearing in the Law of Logic / functional-equation package.
No downstream theorems currently depend on the instance in the graph; it is infrastructure for automation and for stating that the forced comparison is effective.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.