TraceLogicCertificate
plain-language theorem explainer
Packages the first-pass PRC logic surface: stable predicates on finite traces with classical intro/elim rules for truth, connectives, quantifiers, and persistence under extension. Kernel and universal-foundation certificates cite it as the judgment layer. The declaration is a Prop-valued structure, not a proved theorem; the inhabitant is built separately.
Claim. A trace-logic certificate is a proposition asserting: the surface of stable trace predicates is inhabited; truth holds at every finite trace; conjunction, disjunction, implication, and negation satisfy the usual introduction and elimination laws relative to trace extension; universal and existential quantification over families of predicates obey intro/elim; every predicate that holds at $T$ still holds at any extension $U$ of $T$; and the strength tag is fixed at the delta-only level.
background
In the Primitive Recognition Calculus, a finite trace is the basic observational object. Extension means one trace is another followed by a suffix (Extends T U iff there exists $V$ with append $T$ $V$ = $U$). A trace predicate is a proposition on traces that is stable under every such extension: if it holds at $T$ and $U$ extends $T$, it holds at $U$.
The first PRC logic pass treats these stable predicates as the proposition surface. Truth is the constantly-true stable predicate. Connectives and quantifiers are defined pointwise on the holds field, inheriting stability from the components. Implication and negation are evaluated along extensions of the current trace, so the logic is sensitive to future growth of the observation.
This module sits under Foundation and feeds the kernel bundling layer. The certificate does not yet claim inevitability of the logic; it only names the interface that a first-pass construction must discharge.
proof idea
No proof body: this is a structure definition whose fields are the required Prop obligations. An inhabitant is assembled elsewhere by supplying witnesses for each field (nonempty surface via the top predicate, intro/elim lemmas for each connective and quantifier, the persistence axiom already built into TracePredicate.stable, and a trivial strength-tag equality). The companion theorem trace_logic_certificate fills those fields from the in-module TracePredicate API.
why it matters
This is the headline target for the first trace-logic pass. Downstream, KernelFirstPassCertificate requires a trace_logic field of this type, recording that stable finite-trace predicates carry the first PRC logic surface. Both PRCUniversalFoundationCertificate and PRCUniversalFoundationConditionalCertificate re-export the same field, so the universal-foundation closeout cannot assemble without it.
In the Recognition stack this is scaffolding for the judgment layer above raw traces, not yet a forcing-chain step (T0–T8). It makes the logic surface nameable and composable so later certificates can treat connectives and quantifiers as fixed data rather than ad-hoc lemmas. Open work remains on the full inevitability theorem; this certificate is explicitly a bundling interface, not that theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.