trace_logic_certificate
plain-language theorem explainer
The first-pass Primitive Recognition Calculus logic is fully inhabited: stable predicates on finite traces support truth, conjunction, disjunction, implication, negation, quantifiers, and persistence under extension. Anyone assembling the PRC kernel or the universal-foundation certificate cites this packing result. The proof is a field-by-field assembly that wires each connective to its already-proved TracePredicate intro/elim lemma.
Claim. There exists a first-pass trace-logic certificate: the type of stable predicates on finite traces is nonempty (witnessed by the constantly-true predicate), and those predicates satisfy the standard intro/elim rules for $\top$, $\land$, $\lor$, $\to$, $\neg$, $\forall$, $\exists$, together with persistence under trace extension, at the declared strength tag.
background
In the Primitive Recognition Calculus, a first-pass proposition is a TracePredicate: a predicate holds : Trace → Prop that is stable under extension (if it holds on $T$ and $U$ extends $T$, then it holds on $U$). Connectives are defined pointwise on traces and inherit stability from their components.
The certificate structure packages the whole surface: nonempty proposition type, truth introduction, conjunction intro and projections, disjunction injections, implication and negation elimination, universal intro/elim, existential intro, and a persistence rule under Trace.Extends. Its doc-comment calls it the "headline target for the first trace-logic pass."
Local setting is the TraceLogic module of PRC Foundation, which builds the connective lemmas (and_intro, all_elim, persists, etc.) before packing them. Upstream units and field constructions appear only as ambient imports; the logical content is pure trace-predicate algebra.
proof idea
Construct the certificate structure by filling each field. Proposition surface is the singleton of the constantly-true stable predicate. Truth intro is top_intro. Each remaining field is a short tactic block that intros the relevant predicates and traces, then applies the matching TracePredicate lemma: and_intro / and_left / and_right for conjunction, or_inl / or_inr for disjunction, imp_elim and not_elim for implication and negation, all_intro / all_elim for universals, exists_intro for existentials, and persists for extension stability. Strength tag is reflexivity. No new reasoning: pure wiring of already-proved connective lemmas.
why it matters
This is the logic layer of the first PRC kernel pass. Downstream, kernel_first_pass_certificate (K7/A2: "the first-pass kernel certificate is inhabited") installs it as the trace_logic field alongside strength tags, empty-trace syntax, and the verifier-equality judgment. The larger prc_universal_foundation_conditional_certificate reuses the same packing, so every universal-foundation claim that needs a working trace logic routes through here.
In framework terms it is scaffolding closure for the recognition calculus before mass ladders, eight-tick structure, or forcing-chain steps (T5–T8) are invoked: without a certified connective surface on traces, later PRC judgments have nothing to evaluate. It does not itself force $\phi$, $D=3$, or the RCL; it only certifies that the predicate logic on traces is live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.