and_left
plain-language theorem explainer
Left elimination for conjunction on stable trace predicates: if the conjunction of two predicates holds at a finite recognition trace, the left conjunct holds there. Anyone assembling the first PRC propositional layer cites this for ∧-elim. The proof is a one-line projection of the underlying product of Props.
Claim. Let $P$ and $Q$ be stable predicates on finite traces, and let $T$ be a finite trace. If $(P \land Q)$ holds at $T$, then $P$ holds at $T$.
background
In the Primitive Recognition Calculus, a finite trace is built inductively: empty, or extended by one distinction act. A proposition in the first PRC logic pass is a TracePredicate: a predicate on traces that is stable under extension (if it holds at $T$ and $U$ extends $T$, it holds at $U$).
Conjunction is defined pointwise: $(P \land Q)$ holds at $T$ exactly when both $P$ and $Q$ hold at $T$, and stability of the pair follows from stability of each factor. This module packages the standard intro/elim rules for that surface so later certificates can treat PRC logic as an ordinary propositional fragment over traces.
proof idea
One-line wrapper. By definition of conjunction, the hypothesis is a pair of Props; exact h.1 projects the left component, which is exactly $P$ holding at $T$. No stability argument is needed at the elim site.
why it matters
Fills the left ∧-elim slot in the PRC trace-logic surface. Downstream, trace_logic_certificate packages top, truth-intro, and conjunction-intro into a single certificate object; left (and right) elim complete the classical conjunction interface that certificate assumes. In the broader foundation stack this is scaffolding for reasoning about recognition histories before the forcing chain (T5 J-uniqueness, T6 φ, T7 eight-tick, T8 D=3) is applied; it does not itself force physics constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.