not_elim

In Primitive Recognition Calculus, a finite trace is built from the empty trace by successive distinction acts. Extension means the later trace is the earlier one followed by some suffix: $\mathrm{Extends}, T, U$ iff there exists $V$ with $\mathrm{append}, T, V = U$.

A trace predicate is a proposition in the first PRC logic pass: a predicate on traces together with a stability witness that truth, once established at $T$, persists at every extension of $T$. Connectives (top, bottom, and, or, imp, not, quantifiers) are defined so that the resulting predicate remains stable.

Negation is the connective whose holding at $T$ packages the claim that $P$ never holds on any extension of $T$. The present lemma is the corresponding elimination rule: a positive holding of $P$ on an extension immediately contradicts that package.

One-line wrapper. The hypothesis that $(\mathrm{not}, P)$ holds at $T$ is already the function that, given any extension $U$ of $T$ and a proof that $P$ holds at $U$, returns $\mathrm{False}$. The proof simply applies that function to $U$, the extension witness, and the holding of $P$ at $U$ (exact hn U hTU hP). No extra lemmas are needed.

This is the contradiction rule for the PRC trace-logic fragment. It sits beside the introduction and projection rules for the other connectives (top, and, or, imp, quantifiers) and is consumed by trace_logic_certificate, which packages the whole surface (proposition type, truth intro, conjunction intro, and the remaining rules) into a single certificate object.

In the Recognition framework this is foundation-layer scaffolding for reasoning about finite recognition histories before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) is invoked. It does not itself force physical constants; it guarantees that the stable-predicate logic used to talk about traces has classical negation elimination.