and_right
plain-language theorem explainer
Right elimination for conjunction of stable trace predicates: if P∧Q holds on a finite recognition trace, then Q holds there. Anyone assembling the first PRC logic layer or the TraceLogicCertificate cites it. The proof is a one-line projection of the underlying And pair.
Claim. Let $P$ and $Q$ be stable predicates on finite traces (propositions that persist under trace extension). If $(P \land Q)$ holds at a finite trace $T$, then $Q$ holds at $T$.
background
In the Primitive Recognition Calculus, a finite trace is built inductively: empty, or extended by one distinction act. A TracePredicate is a proposition in the first PRC logic pass: a predicate on such traces that is stable under extension (if it holds on $T$ and $U$ extends $T$, it holds on $U$).
Conjunction is defined pointwise: $(P \land Q)$ holds at $T$ exactly when both $P$ and $Q$ hold at $T$, and stability is inherited componentwise from $P$ and $Q$. The companion left-elimination rule and the introduction rule sit beside this declaration in the same module.
proof idea
One-line wrapper. The hypothesis is definitionally a pair of propositions $P.holds,T \land Q.holds,T$; exact h.2 projects the right conjunct.
why it matters
Fills the right half of conjunction elimination in the first PRC logic surface. Downstream, trace_logic_certificate packages the logic API (truth introduction, conjunction introduction, and the surrounding surface) as a single certificate object; this lemma is the matching right-elim fact that keeps the conjunction fragment classical and usable. It is pure foundation scaffolding for later recognition logic, not a physics forcing step (T5–T8), but it makes stable trace propositions behave like ordinary propositions under $\land$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.