all
plain-language theorem explainer
Universal quantification for the first PRC logic pass: given a family of stable trace predicates indexed by an arbitrary type, form the predicate that holds on a finite trace exactly when every member holds. Stability under trace extension is inherited pointwise from the family. Anyone building quantified statements in TraceLogic cites this connective; the proof is a one-line pointwise appeal to each component's stability.
Claim. For any type $\alpha$ and any family $P:\alpha\to\mathrm{TracePredicate}$, define a new stable trace predicate $\forall P$ by $(\forall P)(T)\iff\forall a\in\alpha,\, P(a)\text{ holds on }T$. If $T$ extends to $U$ and $\forall P$ holds on $T$, then $\forall P$ holds on $U$.
background
In the Primitive Recognition Calculus (PRC) first logic pass, a proposition is not an ordinary Lean Prop. It is a TracePredicate: a predicate on finite traces together with a stability certificate that the property, once true on $T$, remains true on every extension $U\supseteq T$.
The module assembles a small connective suite (top, bottom, and, or, imp, not, and the quantifiers) so that verifier-facing statements can be written in a logic whose every formula is automatically stable under lengthening the observed trace. The index type $\alpha$ is pure verifier bookkeeping; it does not enlarge the trace or change the finite-trace character of stability.
Upstream, the only structural dependency is the TracePredicate structure itself (holds + stable under Trace.Extends).
proof idea
Definitional construction, not a deep theorem. The holds field is ordinary universal quantification over the family: $\forall a,,(P,a).\mathrm{holds},T$.
Stability is discharged in four tactics: introduce the extension $T\preceq U$, the hypothesis that $\forall a$ holds on $T$, and a fresh index $a$; then apply the component stability law $(P,a).\mathrm{stable}$ to the same extension and to the instantiated hypothesis. No other lemmas are required.
why it matters
This is the $\forall$ connective of TraceLogic, the first PRC logic pass. Together with exists_, and, or, imp, and not, it lets the foundation express verifier-indexed families of recognition claims while preserving the finite-trace stability invariant that every PRC proposition must satisfy.
Downstream, the connective is the building block for quantified stability lemmas and introduction rules in the same module (siblings such as top_intro, and_intro). In the broader Recognition stack it supports writing "for all slots / all ticks / all admissible labels" statements without leaving the stable-trace fragment, which is the logical substrate under later cost, action, and forcing-chain arguments.
It does not itself invoke T5–T8 or the Recognition Composition Law; it only equips the language in which those claims can be stated as stable trace properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.