or_inl
plain-language theorem explainer
Left introduction for disjunction of stable trace predicates: if P holds at a finite recognition trace T, then P∨Q holds at T. Anyone assembling the first PRC logic pass or the trace-logic certificate cites this. The proof is a one-line wrapper that applies classical Or.inl to the holding hypothesis.
Claim. Let $P$ and $Q$ be stable predicates on finite traces, and let $T$ be a finite trace. If $P$ holds at $T$, then the disjunction $P \lor Q$ holds at $T$.
background
In the Primitive Recognition Calculus, a finite trace is either empty or built by successive distinction acts. A TracePredicate is a proposition on such traces that is stable under extension: once it holds, it continues to hold on every longer trace.
Disjunction of two TracePredicates is defined pointwise by classical or on the holding relation, with stability proved by case analysis on the disjunct that holds and re-applying each conjunct's stability. The local module builds the first logic surface over these stable predicates (truth, conjunction, disjunction, implication, negation, quantifiers).
This lemma is the left introduction rule for that disjunction, parallel to the usual Or.inl of propositional logic but typed over Trace and TracePredicate.
proof idea
One-line wrapper. Unfolding the definition of disjunction, the goal is exactly $P.holds,T \lor Q.holds,T$. The proof applies classical Or.inl to the given hypothesis that $P$ holds at $T$. No stability argument is needed at the introduction site; stability was already sealed inside the definition of disjunction.
why it matters
The lemma is one of the introduction rules packaged by trace_logic_certificate, which records that the first PRC logic pass has a working proposition surface with truth, conjunction, and related rules. Without left (and right) disjunction introduction, the certificate cannot claim a usable classical fragment over stable trace predicates.
In the broader Recognition framework this sits in Foundation, before the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3). It does not yet touch mass ladders or coupling constants; it only ensures that the primitive recognition logic can form alternatives over finite distinction histories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.