or_inr
plain-language theorem explainer
Right-introduction for disjunction of stable trace predicates: if Q holds at a finite trace T, then the disjunction 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 around classical Or.inr.
Claim. Let $P$ and $Q$ be stable predicates on finite traces. If $Q$ holds at a trace $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 holds fields, with stability proved by case analysis on the disjunct that fires. The local module builds the first logic surface over these stable predicates (truth, conjunction, disjunction, implication, quantifiers).
Upstream, Trace is the inductive type of finite recognition histories; the or constructor packages the pointwise disjunction and its stability proof.
proof idea
One-line wrapper. The holds field of or P Q is definitionally P.holds T ∨ Q.holds T, so Or.inr applied to the given proof that Q holds at T yields the goal directly.
why it matters
Fills the right-introduction rule for the disjunction fragment of the first PRC logic pass. Downstream it is consumed by trace_logic_certificate, which packages the proposition surface, truth introduction, and conjunction introduction into a single certificate object. Without right-introduction, the certificate cannot treat disjunctive goals as first-class stable predicates. The result sits at the foundation layer before the forcing chain (T0–T8) and does not itself force phi, the eight-tick octave, or D = 3; it only equips the logic used to state later recognition claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.