exists_
plain-language theorem explainer
Existential quantification over a family of stable trace predicates again yields a stable trace predicate: it holds on a finite trace exactly when some witness in the family holds there. The same witness is kept under trace extension, so stability is inherited pointwise. Builders of the first PRC logic pass and of TraceLogicCertificate cite this connective. The body is a short stability check that reuses the chosen family's stability lemma.
Claim. For any type $\alpha$ and family $P:\alpha\to$ (stable trace predicates), the map $T\mapsto\exists a\in\alpha.\,P(a)\text{ holds on }T$ is itself a stable trace predicate: if it holds on $T$ and $U$ extends $T$, then it holds on $U$.
background
In the first Primitive Recognition Calculus (PRC) logic pass, a proposition is not an ordinary Prop. It is a TracePredicate: a predicate on finite traces that is required to persist under trace extension. Formally, holds : Trace → Prop comes with a stability law: whenever Trace.Extends T U and the predicate holds on T, it holds on U.
This module packages the usual logical connectives so that each connective returns another stable trace predicate. Existential quantification is the quantifier half of that surface, dual to the universal connective all in the same file. The witness is an index in an arbitrary type $\alpha$ (a verifier-indexed family), not a term of the trace itself.
Upstream, the only structural dependency that matters is the TracePredicate structure and the extension relation on traces. Other U/T names in the dependency graph are ambient RS units or field carriers and do not enter the proof.
proof idea
The holds field is defined directly as classical existence: some $a:\alpha$ with $(P,a).\mathrm{holds},T$.
Stability is a three-line tactic proof. Assume Trace.Extends T U and a proof that the existential holds on $T$. Destructure that proof to a concrete witness $a$ and a proof that $(P,a)$ holds on $T$. Apply the stability field of that same $P,a$ along the given extension to obtain a proof that $(P,a)$ holds on $U$. Re-pack the same $a$ to conclude the existential on $U`. No other lemmas are invoked.
why it matters
This definition is one of the primitive connectives of the first PRC trace-logic surface. Downstream, exists_intro is the introduction rule: from a concrete witness $a$ and $(P,a).\mathrm{holds},T$ one obtains (exists_ P).holds T. The headline structure TraceLogicCertificate lists a nonempty proposition surface together with introduction laws for truth and conjunction; existential quantification sits in the same connective suite that makes that certificate inhabitable.
In the broader Recognition stack this is scaffolding for reasoning about finite observation traces before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) is re-derived at the logical layer. It does not yet encode mass ladders or coupling constants; it only guarantees that "there exists a verifier for whom the claim is stable" remains a legitimate stable claim under trace growth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.