actJudgment_diff
plain-language theorem explainer
Under any finite distinction trace, the act-level “diff” judgment on two endpoints is definitionally the same proposition as ordinary inequality of those endpoints. Cite this when arguing that comparison is not a second primitive but is read off the free act-generated structure. The proof is pure definitional reflexivity (`Iff.rfl`).
Claim. For every finite trace $T$ and endpoints $a,b$ (sides of the primitive distinction), the act-judgment that $a$ and $b$ differ holds if and only if $a \neq b$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction $\delta$ (left or right). A finite trace is the empty history or a history extended by one distinction act; it is the free inductive record of acts, not a second semantic layer.
The local module develops the one-primitive thesis: comparison (“same” vs “diff”) is not an independent primitive alongside distinction. The act-judgment is the classification of a pair of endpoints relative to a trace, generated from that inductive structure. Sibling facts treat the “same” case and decidability of the forced comparison.
Upstream scaffolding includes the endpoint and trace constructors from Basic, the multi-distinction difference operator (channel-wise compare holding other channels fixed), and the broader reduction from seven independent axioms to four structural conditions plus definitional facts in PrimitiveDistinction.
proof idea
Term-mode one-liner: Iff.rfl. By definition of the act-judgment, the proposition “diff on $T$ at $a,b$” is definitionally identical to $a \neq b$, so the biconditional holds by reflexivity of Iff. No lemmas are applied; no case split on the trace is required.
why it matters
This is a definitional hinge in the one-primitive package: once “diff” is just endpoint inequality, comparison does not smuggle in a second ontological primitive. It sits beside the matching “same” characterization and the decidability claim that “compare” is decide on a freely generated type.
No downstream consumers are wired in the current graph (used_by empty), so its role is local foundation hygiene rather than a bridge into the T5–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$). It still supports the broader Recognition claim that the calculus is generated from distinction acts alone, with judgment derived rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.