exists_intro
plain-language theorem explainer
Existential introduction for the first PRC logic layer: if a witness a makes the stable predicate P(a) hold on a finite trace T, then the existential quantification of P holds on T. Anyone assembling the TracePredicate connectives or the trace-logic certificate cites this. The proof is a one-line pair constructor packaging the witness with its holding proof.
Claim. Let $\alpha$ be a type, $P:\alpha\to\mathrm{TracePredicate}$ a family of stable trace predicates, and $T$ a finite trace. If $a\in\alpha$ and $P(a)$ holds at $T$, then the existential quantification $\exists P$ holds at $T$.
background
In the Primitive Recognition Calculus, a finite trace is built inductively: empty, or extended by one distinction act (K2.4). A TracePredicate is a proposition on such traces that is stable under extension: once it holds, it continues to hold on every longer trace.
Existential quantification over a verifier-indexed family is itself a TracePredicate. Its holding clause is ordinary existence of a witness $a$ with $(P,a)$ holding at $T$; stability is inherited by reusing the same witness after extension. This sits in the first PRC logic pass, which equips traces with a small stable-proposition calculus (truth, conjunction, disjunction, implication, negation, universal and existential quantifiers).
proof idea
One-line wrapper. The holding clause of $\exists P$ is defined as $\exists a,,(P,a).\mathrm{holds},T$. The proof applies exact to the pair $\langle a, h\rangle$, which is exactly that existential witness. No stability argument is needed at the introduction site; stability was already discharged when exists_ was defined.
why it matters
Fills the introduction rule for the existential connective in TraceLogic, parallel to top_intro, and_intro, and the other intro/elim lemmas in the same module. Downstream it is consumed by trace_logic_certificate, which packages the whole connective surface (truth, conjunction, and the remaining rules) into a single certificate object for the first PRC logic pass.
In the broader Recognition stack this is scaffolding for reasoning about finite distinction histories before the forcing chain (T0–T8) and the J-cost calculus are invoked. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only guarantees that existential claims about stable trace properties are well-formed and closed under extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.