comparison_is_derived_not_primitive
plain-language theorem explainer
Any tight, separating trace judgment has its sameness relation forced to ordinary endpoint equality, and therefore coincides with the act-generated judgment. Recognition theorists cite this to close the claim that comparison is not a second primitive beside the distinction act. The proof is a two-line term that chains the genuine-judgment equality lemma with the act-judgment characterization of sameness.
Claim. Let $J$ be a trace judgment that is tight ($J$ reports difference exactly when it does not report sameness) and separating (on every trace, left and right endpoints are judged different). Then for every finite trace $T$ and endpoints $a,b$: $J$ judges $a$ the same as $b$ if and only if $a=b$, and equivalently if and only if the act-generated judgment does.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction $\delta$, and a finite trace is built by starting empty and adjoining distinction acts. A trace judgment assigns, on each trace, a sameness and a difference relation on endpoints. The act-generated judgment is the canonical one forced by the act structure: sameness is decidable equality of endpoints, difference is disequality.
Tightness says difference is exactly the negation of sameness. Separating says left and right are always judged different. Under those admissibility conditions, the earlier lemma that a genuine judgment's sameness is equality already collapses $J$'s sameness to $a=b$. The present result packages that collapse with agreement against the act-generated judgment, so comparison is derived rather than primitive.
The local module is the one-primitive strand of PRC: it shows recognition needs only the distinction act, not an independent same/different primitive.
proof idea
Introduce an arbitrary trace $T$ and endpoints $a,b$. Apply genuine_judgment_same_is_equality to $J$ with the tightness and separating hypotheses to obtain $J.\mathrm{same},T,a,b \leftrightarrow a=b$. The second conjunct is that same equivalence composed with the symmetric form of actJudgment_same, which states that the act-generated judgment's sameness is exactly $a=b$. The pair of iff's is the claimed conjunction. Pure term-mode chaining; no case split.
why it matters
This is the Item 5 resolution in the PRC one-primitive program: recognition is one primitive. Downstream it is wired directly into prc_shrunk_certificate as the one_primitive field of the $\delta$ program certificate ("Seven proved headlines, no axioms, no sorry"). That certificate is the shrunk audit surface for the foundation layer that feeds the forcing chain and the cost calculus.
Framework-wise it underwrites the claim that same/different is not an independent second primitive beside the distinction act. Everything comparative is forced by the act-generated structure once tightness and separation hold. It does not itself invoke T5--T8 or the RCL, but it clears the primitive count before those later forcing steps are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.