and_intro
plain-language theorem explainer
If two stable predicates on finite recognition traces both hold at a trace T, their conjunction holds at T. Anyone assembling the first-pass PRC propositional calculus cites this as the conjunction-introduction rule. The proof is a one-line pair constructor against the definition of conjunction.
Claim. Let $P$ and $Q$ be stable predicates on finite traces (predicates that persist under trace extension). If $P$ holds at a finite trace $T$ and $Q$ holds at $T$, then the conjunction $P \land Q$ 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 such 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 conjunction is inherited from the two factors. This module packages the standard connectives (truth, falsehood, $\land$, $\lor$, $\to$, $\neg$, quantifiers) as operations that preserve stability, so the logic lives entirely on the trace side of the calculus.
proof idea
One-line wrapper. By definition, $(P \land Q).\mathrm{holds}, T$ is the pair $P.\mathrm{holds}, T \land Q.\mathrm{holds}, T$. The tactic exact ⟨hP, hQ⟩ supplies that pair from the two hypotheses. No stability argument is needed at the introduction site; stability was already discharged when conjunction was defined.
why it matters
This is the introduction half of conjunction in the first PRC logic pass. Downstream, trace_logic_certificate packages the surface of that logic and sets conjunction_intro by applying this lemma directly. Without a proved intro rule, the certificate cannot claim that the stable-predicate fragment supports ordinary propositional reasoning on traces. The result is local plumbing inside Foundation, not a forcing-chain step (T0–T8), but it is required infrastructure before trace-level statements can be composed and certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.