consistent_of_exclusive
plain-language theorem explainer
Every admissible trace judgment is consistent at every finite trace: it never asserts both sameness and witnessed difference on the same endpoint pair. Builders of the primitive recognition calculus (K2.6–K2.8, rule R6) cite this. The argument is a one-line unpack of the exclusivity field already required by the judgment surface.
Claim. For every admissible trace judgment surface $J$ and every finite trace $T$, $J$ is consistent at $T$: there do not exist endpoints $a,b$ such that both $\mathrm{Same}_T(a,b)$ and $\mathrm{Diff}_T(a,b)$ hold under $J$.
background
A finite trace is the inductive object of the primitive recognition calculus: empty, or extended by one distinction act (K2.4). Endpoints are the objects compared along a trace.
An admissible trace judgment surface packages object-level sameness and witnessed difference at each trace, together with the structural laws those relations must obey. Among those laws is exclusivity: sameness and difference cannot both hold for the same pair at the same trace.
Consistency (K2.8) is the global reading of that exclusivity at a fixed trace: for all endpoints $a,b$, it is not the case that both $\mathrm{Same}_T(a,b)$ and $\mathrm{Diff}_T(a,b)$. Rule R6 asserts that the exclusivity field already present on any admissible judgment yields consistency at every trace.
proof idea
Term-mode unpack of the structure field. Introduce endpoints $a,b$ and a hypothesis that both same and diff hold at $T$. Discharge by the judgment's built-in exclusivity field same_diff_exclusive applied to the two conjuncts. No auxiliary lemmas are needed beyond the structure axioms of the judgment surface.
why it matters
Closes rule R6 in the SameDiff layer of the primitive recognition calculus: exclusivity on the judgment surface is exactly consistency at every trace. That layer supplies the object-level Same/Diff interface (K2.6–K2.8) used to reason about recognition acts without collapsing equality and witnessed difference.
No downstream consumers are wired yet in the graph, so the result presently stands as a local sanity theorem for the judgment API rather than a step in a longer forcing chain (T0–T8). It keeps the recognition surface free of contradictory Same/Diff assertions before later modules build substitution, verifiers, or cost comparisons on top of it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.