TracePredicate
plain-language theorem explainer
A proposition in the first Primitive Recognition Calculus logic is a predicate on finite traces that is stable under extension: once true of a prefix, it remains true of every longer continuation. Anyone building PRC connectives (conjunction, universal quantification, implication) cites this carrier type. The declaration is a pure structure definition packing the hold-map with its monotonicity witness.
Claim. A trace predicate is a pair $(H, S)$ where $H$ assigns to each finite trace a proposition, and $S$ asserts stability under extension: whenever $U$ extends $T$ (i.e., $U$ is $T$ followed by a finite suffix) and $H(T)$ holds, then $H(U)$ holds.
background
In the Primitive Recognition Calculus, a finite trace is the empty sequence or a prior trace extended by one distinction act. Extension is the suffix relation: $U$ extends $T$ when some finite continuation $V$ satisfies $\mathrm{append}(T,V)=U$. That relation is reflexive, so stability is a genuine monotonicity constraint rather than a vacuous filter.
The TraceLogic module treats propositions of the first PRC pass as data of this shape. Stability is the key design choice: truth is allowed to depend only on what has already been recognized, never on unrealized future distinctions. Downstream connectives (conjunction, disjunction, implication, quantifiers) are defined by pointwise operations on the hold-maps, with stability proved componentwise from the factors' stability witnesses.
The surrounding foundation links traces to the recognition forcing chain and the eight-tick octave, but this structure itself is purely logical: it does not yet encode costs, $J$-values, or dimensional forcing.
proof idea
No proof body: this is a structure declaration. It packages two fields, a map from traces to propositions and a universal stability lemma quantifying over extension pairs. Inhabitants are constructed by supplying both fields (as in the sibling definitions of top, conjunction, and universal quantification), after which the stability proof obligations are discharged by the corresponding component lemmas.
why it matters
This is the carrier type for the entire first PRC logic layer. Every connective and introduction/elimination rule in TraceLogic is typed over it: conjunction, disjunction, implication, negation, top, bottom, universal and existential quantification, plus their intro/elim lemmas. Without the stability field, later theorems could not guarantee that derived propositions remain meaningful under further recognition steps.
In the broader Recognition framework the structure implements the slogan that logical content is prefix-stable on the distinction stream. That matches the forcing-chain picture in which later ticks refine earlier structure (eight-tick octave, $D=3$) without retracting prior recognition. It does not itself force $\phi$, $J$, or the mass ladder; those enter only when concrete physical predicates are instantiated as stable trace predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.