Consistent
plain-language theorem explainer
Consistency of a judgment surface at a fixed finite trace means the surface never marks the same pair of endpoints as both equal and different. Anyone building cost-from-distinction, logic-from-cost, or gauge certificates cites this predicate as the local no-contradiction condition. The body is a one-line universal quantification over endpoints forbidding the conjunction of Same and Diff.
Claim. A judgment surface $J$ is consistent at a finite trace $T$ when, for every pair of endpoints $a,b$, it is not the case that $J$ asserts both object-level equality of $a$ and $b$ at $T$ and object-level witnessed difference of $a$ and $b$ at $T$.
background
In the primitive recognition calculus, an endpoint is one side of a primitive distinction, and a finite trace is either empty or built by successive distinction acts. A trace judgment surface packages two object-level relations at each trace: Same (equality) and Diff (witnessed difference), together with the R5 requirements that Same be an equivalence relation at every trace.
Consistency (K2.8) is the exclusivity demand on that surface: Same and Diff cannot both hold for the same endpoint pair at the same trace. The sibling structure TraceJudgment is exactly the admissible package of those two relations plus the equivalence proofs for Same. Downstream cost and logic layers treat failure of this exclusivity as the source of positive cost.
proof idea
Definitional, not a proof. The predicate is the universal statement that no endpoint pair simultaneously satisfies both the Same and Diff components of the judgment at the given trace. No lemmas are applied; the body is the Prop itself.
why it matters
This is the local consistency gate (K2.8 / R6) that later layers turn into cost and logic. cost_pos_iff_inconsistent equates positive cost with inconsistency of a configuration, and consistent_cost / consistent_minimum_cost in LogicFromCost use the same exclusivity idea to pin zero cost at consistent states. Gauge and cosmology certificates (gauge_group_certificate, OmegaLambdaCert, vacuum-fluctuation structural certs) sit further downstream on that cost/logic spine. In the forcing picture it is bookkeeping for the distinction calculus that feeds T5–T8, not a forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.