imp_elim
plain-language theorem explainer
Implication elimination for stable predicates on finite recognition traces: if P implies Q at trace T, U extends T, and P holds on U, then Q holds on U. Anyone assembling the first-pass PRC propositional surface cites this as modus ponens along growing traces. The proof is a one-line application of implication as universal quantification over future extensions.
Claim. Let $P$ and $Q$ be predicates on finite traces that are stable under extension. If the implication $P \Rightarrow Q$ holds at a trace $T$, the trace $U$ extends $T$, and $P$ holds at $U$, then $Q$ holds at $U$.
background
In the Primitive Recognition Calculus, a finite trace is either empty or built by successive distinction acts. Extension means one trace is a prefix of another: there exists a suffix whose append yields the longer trace.
A stable trace predicate is a proposition on traces that persists under every extension. Once it holds at $T$, it holds at every longer $U$. Implication is defined so that $P \Rightarrow Q$ holds at $T$ exactly when, for every extension $U$ of $T$, $P$ at $U$ forces $Q$ at $U$. That definition is itself stable under further extension (by transitivity of extension).
This module supplies the first-pass propositional surface for PRC logic: truth, conjunction, disjunction, implication, negation, and quantifiers, before packaging the rules into a certificate.
proof idea
One-line wrapper. The hypothesis that implication holds at $T$ is already the universal statement that every extension $U$ of $T$ with $P$ at $U$ yields $Q$ at $U$. Instantiating that statement at the given $U$, the given extension proof, and the given proof that $P$ holds produces $Q$ at $U$ by exact application. No extra lemmas are required beyond the definition of implication.
why it matters
Feeds the assembled trace-logic certificate in the same module, which packages introduction and elimination rules of the PRC propositional surface into one certificate structure. Implication elimination is the modus ponens step of that surface: without it, conditional reasoning cannot be discharged as the recognition history lengthens.
Traces record successive distinction acts; stable predicates are the propositions that survive discrete recognition steps. Keeping implication usable under extension is the minimal logical hygiene needed before later foundation layers treat recognition evolution and the discrete tick structure. The lemma closes a basic elimination rule rather than an open forcing-chain gap; it is infrastructure for the certificate, not a T0–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.