top
plain-language theorem explainer
Truth in the first Primitive Recognition Calculus logic pass: the stable predicate that holds on every finite trace. Anyone building Boolean or quantifier structure over traces cites it as the unit of the lattice. The definition is immediate: holds is constantly True, and stability under trace extension is trivial.
Claim. Define the truth predicate $\top$ on finite traces by $\top(T) \Leftrightarrow \mathsf{True}$ for every trace $T$. It is stable: whenever $U$ extends $T$ and $\top(T)$ holds, then $\top(U)$ holds.
background
In the Primitive Recognition Calculus (PRC) first logic pass, a proposition is not an arbitrary Prop. It is a TracePredicate: a predicate on finite traces that is stable under extension. Formally, if $T$ extends to $U$ and the predicate holds at $T$, it must still hold at $U$. That monotonicity is the only structural constraint at this layer.
The module builds a small internal logic (truth, falsehood, conjunction, disjunction, implication, negation, universal and existential quantification) entirely out of such stable predicates. Truth is the top element of that lattice: the predicate true at every history.
Upstream, the structure TracePredicate packages the pair (holds, stable). No deeper forcing-chain or J-cost material is required here; this is pure logical scaffolding on traces.
proof idea
Definitional construction, not a derived theorem. Set holds to the constantly-true function on traces. Stability is discharged by intro on the four arguments (two traces, an extension witness, and a holds hypothesis) followed by trivial, since the goal is True.
why it matters
Supplies the unit for the PRC trace logic. Downstream introduction rules such as top_intro and the Boolean combinators (and, or, imp, not, all, exists_) treat this as the always-available true proposition. Without a stable top, the lattice of trace propositions would lack a greatest element and introduction/elimination lemmas would have no canonical true case.
This sits at the foundation layer before mass ladders, eight-tick structure, or $D=3$ forcing. It does not itself encode physics content; it is the logical carrier on which later recognition statements are written as stable predicates on traces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.