or
plain-language theorem explainer
Disjunction of two stable trace predicates is again a stable trace predicate: it holds on a finite trace exactly when at least one disjunct does. Anyone building the first-pass PRC logic (connectives on extension-persistent propositions) cites this constructor. Stability is proved by case-splitting the classical disjunction and applying each operand’s stability along the same extension.
Claim. If $P$ and $Q$ are predicates on finite traces that persist under trace extension, then $P \lor Q$ defined by $(P \lor Q)(T) \iff P(T) \lor Q(T)$ is again extension-persistent: whenever $T$ extends to $U$ and $(P \lor Q)(T)$ holds, so does $(P \lor Q)(U)$.
background
In the Primitive Recognition Calculus (PRC) first logic pass, a proposition is not an arbitrary formula: it is a TracePredicate, a predicate on finite traces together with a stability law. Stability says that if the predicate holds on $T$ and $U$ extends $T$, then it holds on $U$. That matches the physical reading that once a recognition fact is settled on a finite history, later ticks cannot retract it.
The module builds a small connective calculus on these stable predicates (truth, falsity, conjunction, disjunction, implication, negation, quantifiers). Disjunction is the classical pointwise join of the two holds maps. The only nontrivial obligation is to re-establish stability for the combined predicate, using the stability of each operand and the fact that classical $\lor$ is closed under the same case split along any fixed extension.
proof idea
The holds field is the pointwise classical disjunction of $P$ and $Q$. For stable, fix traces $T,U$ with $U$ extending $T$, and assume $(P\lor Q)(T)$. Case-split that assumption: if $P(T)$, apply $P$'s stability along the same extension to get $P(U)$, then inject left; if $Q(T)$, apply $Q$'s stability and inject right. No extra lemmas beyond the structure fields and Or.inl/Or.inr.
why it matters
This is infrastructure for the PRC trace logic layer in Foundation: without closure of stable predicates under $\lor$, the first-pass logic cannot express alternative recognition outcomes while remaining extension-persistent. Sibling connectives (and, imp, not, all, exists_) form the same package; introduction rules such as and_intro sit beside it.
Downstream graph edges that merely mention the token or (cost-algebra reciprocal facts, crystal-system strings, path interpolation) are name collisions, not semantic clients. The real consumers are other TraceLogic constructions and any later PRC development that treats stable trace propositions as the atomic assertions of recognition histories. Relative to the forcing chain, this sits below T5–T8: it equips the language in which recognition facts are stated, rather than forcing $J$, $\varphi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.