TraceJudgment
plain-language theorem explainer
An admissible judgment surface packages, at each trace, a same-relation and a diff-relation on endpoints, with same an equivalence and exclusive of diff. Anyone building the primitive recognition calculus cites it as the K2.6–K2.8 interface that later forcing lemmas instantiate. It is a pure structure definition: fields plus the R5/R6 admissibility axioms, no proof body.
Claim. An admissible trace judgment is a pair of relations $\mathrm{Same}_T$ and $\mathrm{Diff}_T$ on endpoints, indexed by traces $T$, such that for every $T$, $\mathrm{Same}_T$ is reflexive, symmetric, and transitive, and $\mathrm{Same}_T(a,b)$ and $\mathrm{Diff}_T(a,b)$ cannot both hold.
background
In the Primitive Recognition Calculus, a trace is the syntactic carrier of a recognition act, and an endpoint is one side of the primitive distinction $\delta$ (left or right). The calculus needs an object-level notion of when two endpoints count as the same or as witnessed different at a given trace, before any quotient or logic surface is built.
This structure is the admissibility package for that surface (K2.6–K2.8). Same is intended as object-level equality-at-a-trace; Diff is witnessed difference. The R5 fields force Same to be an equivalence relation at each fixed trace. The R6 field forces Same and Diff to be exclusive on any ordered pair: they cannot both hold.
Upstream, Endpoint and Trace come from the Basic module of the same calculus. Downstream certificates treat a nonempty instance of this structure as the judgment surface stage of the first PRC kernel chain.
proof idea
No proof: this is a structure definition. It declares two relation fields (same, diff) and four proof fields encoding reflexivity, symmetry, and transitivity of same at each trace, plus mutual exclusion of same and diff. Instantiations (for example the act-forced verifier equality judgment) later supply concrete Props and discharge those fields.
why it matters
This is the load-bearing interface for "comparison" in the $\delta$ program. KernelFirstPassCertificate requires a nonempty judgment surface of this type as one stage of the first-pass PRC kernel. PRCOnePrimitive builds actJudgment as a concrete TraceJudgment, proves same decidable, and runs the core forcing lemmas genuine_judgment_same_is_equality and comparison_is_derived_not_primitive: any tight, separating admissible judgment has same equivalent to endpoint equality, so comparison is derived from the act rather than a second primitive.
PRCShrunkCertificate packages that one-primitive claim as clause (A) of the four load-bearing $\delta$ statements. Quotient constructions use same to form endpoint classes. In framework terms this sits under the foundation forcing chain: it is the formal surface on which recognition stays one primitive before arithmetic, Clifford/8-tick structure, and later physics extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.