bottom
plain-language theorem explainer
Logical falsehood in the first PRC pass: the stable predicate on finite traces that never holds. Anyone building the Boolean algebra of trace predicates (conjunction, implication, negation) cites it as the zero element. Stability is immediate: from a false hypothesis one eliminates, so extension cannot break the property.
Claim. Define the bottom (false) stable trace predicate by $\mathrm{holds}(T) := \bot$ for every finite trace $T$. It is stable under trace extension: if $U$ extends $T$ and $\mathrm{holds}(T)$, then $\mathrm{holds}(U)$ (vacuously, since $\mathrm{holds}(T)$ is never true).
background
In Primitive Recognition Calculus, a first-pass proposition is not an ordinary Prop on configurations. It is a TracePredicate: a predicate on finite traces that is required to persist under extension. Formally, holds : Trace → Prop together with the stability law that whenever $U$ extends $T$ and the predicate holds at $T$, it holds at $U$.
This module equips that structure with the usual logical connectives. The dual of bottom is top, the predicate true at every trace. Stability is the only nontrivial obligation when packaging a raw predicate into the structure; without it, later rules (introduction and elimination for $\land$, $\to$, $\forall$) would not be well-typed as operations on the same class of objects.
The ambient setting is the foundation layer of Recognition Science: traces record finite recognition histories before continuum or metric structure is imposed.
proof idea
Definitional construction of a TracePredicate structure instance. The holds field is the constantly-false predicate. Stability is discharged in one tactic block: assume an extension $T \preceq U$ and a proof $h$ that bottom holds at $T$; then False.elim h yields the required conclusion at $U$. No external lemmas are invoked.
why it matters
Bottom is the zero of the PRC trace-logic algebra. Sibling constructors (and, or, imp, not, all, exists_) and the introduction lemmas (top_intro, and_intro, and_left, ...) treat it as the canonical absurdity, so every derived connective inherits a coherent falsehood.
Downstream, foundation results that quantify over stable trace predicates (for example uniqueness and non-forcing statements in PRCNativeCostUniqueness, and multi-distinction geometry that builds chains and faces from logical structure) rely on having a well-typed bottom element rather than an ad-hoc False. In the broader RS forcing picture this sits below the continuum and metric layers: it is pure discrete logic on traces, not yet J-cost, $\varphi$-ladder masses, or the T5–T8 geometric constraints.
Name collisions with unrelated bottom symbols (bottom quark species, geometric bottom edges of a face) are separate declarations; this one is only the logical falsehood.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.