all_intro
plain-language theorem explainer
Universal introduction for the first-pass PRC logic: if every member of a verifier-indexed family of stable trace predicates holds at a finite trace T, then the universally quantified predicate holds at T. Anyone assembling quantified statements over distinction traces cites this. The proof is a one-line wrapper: the claim is definitionally the hypothesis.
Claim. Let $P$ be a family of stable trace predicates indexed by a type $\alpha$, and let $T$ be a finite trace. If $\forall a\in\alpha$, $P(a)$ holds at $T$, then $(\forall a.\, P(a))$ 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$).
Universal quantification packages a verifier-indexed family $P : \alpha \to$ TracePredicate into a single stable predicate whose holding condition is pointwise: $(\mathrm{all}, P)$ holds at $T$ exactly when every $P(a)$ holds at $T$. Stability of the package is inherited componentwise from the family.
This sits in the TraceLogic module, which builds the connectives (truth, conjunction, disjunction, implication, negation, quantifiers) as stable predicates on traces before any continuum or field structure is imposed.
proof idea
One-line wrapper. By definition, $(\mathrm{all}, P).\mathrm{holds}, T$ is $\forall a,, (P, a).\mathrm{holds}, T$, which is exactly the hypothesis $h$. The proof is exact h; no rewriting or stability argument is needed at the introduction site.
why it matters
Fills the universal-introduction rule in the first PRC logic pass, parallel to top_intro and and_intro. Downstream it is collected into trace_logic_certificate, which packages the surface connectives and their introduction rules as a single certificate that the logic layer is inhabited and closed under the basic constructors.
In the Recognition framework this is scaffolding for reasoning about distinction histories before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) is applied. Quantified stable predicates let later stages state "for every verifier index, the cost or same/diff relation holds along the trace" without leaving the finite-trace fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.