verifierEqualityJudgment
plain-language theorem explainer
A concrete TraceJudgment that takes same to ordinary equality of endpoints and diff to disequality, independent of the trace. It is a verifier-language sanity model, not the object-level PRC primitive. Anyone building kernel certificates or act-forced judgments cites it as the inhabited equality surface. The proofs are the standard reflexivity, symmetry, transitivity, and exclusivity of propositional equality.
Claim. There is an admissible trace judgment surface whose sameness predicate is ordinary equality of endpoints ($a = b$) and whose difference predicate is disequality ($a \neq b$), both independent of the trace. Sameness is reflexive, symmetric, and transitive at every trace, and sameness and difference are mutually exclusive.
background
In the Primitive Recognition Calculus, a trace judgment surface (K2.6–K2.8) packages two object-level relations on endpoints at a trace: sameness (K2.7) and witnessed difference (K2.6). Rule R5 requires sameness to be an equivalence relation at each trace, and the surface must keep sameness and difference exclusive.
This module supplies that interface as a structure with five fields: the two predicates plus proofs of reflexivity, symmetry, transitivity, and exclusivity. The present definition is explicitly a verifier-level model: it shows Lean’s native equality inhabits the interface. It is not claimed to be PRC’s object-level SameT/DiffT primitive.
Upstream, the structure only needs the Trace and Endpoint types from the basic PRC layer; the multi-distinction difference operator and the exp/log field $T$ are ambient context for the calculus, not ingredients of this instance.
proof idea
The definition fills the TraceJudgment structure by setting same to propositional equality and diff to its negation, ignoring the trace argument. Reflexivity is rfl. Symmetry and transitivity are the corresponding lemmas on equality (symm, trans). Exclusivity is the contradiction obtained by applying a disequality hypothesis to an equality hypothesis. No external lemmas beyond equality’s built-in properties are required.
why it matters
The declaration exists to discharge inhabitance of the judgment-surface slot in the first-pass kernel certificate (K7/A2): that certificate packages strength tags, empty-trace syntax, this judgment surface, and a trace-logic certificate. Downstream, the act-forced judgment is defined to be exactly this surface, so every act that forces same/diff inherits equality and decidable disequality.
In the Recognition framework this is scaffolding for the primitive calculus rather than a forcing-chain step (T5–T8). It closes the meta-theoretic question “is the SameT/DiffT interface consistent in the verifier?” without committing to a geometric or cost-theoretic realization of difference. Parent consumers are the kernel first-pass certificate and the one-primitive act judgment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.