FormalSystem
plain-language theorem explainer
Minimal interface for an arbitrary formal system that can host the primitive recognition calculus. It packages token and expression carriers, a distinction relation, expression extension, and maps from PRC endpoints and traces, with a coherence law that trace extension is reflected in expressions. Downstream inevitability and embedding theorems cite it as the surface every candidate foundation must present. The declaration is a pure structure definition with no proof obligations beyond the field types.
Claim. A formal system is a 6-tuple $(T, E, \mathrm{dist}, \preceq_E, \iota, \tau)$ where $T$ and $E$ are types (tokens and expressions), $\mathrm{dist} : T \to T \to \mathrm{Prop}$ is a distinction predicate, $\preceq_E : E \to E \to \mathrm{Prop}$ is expression extension, $\iota$ sends each side of the primitive distinction $\delta$ to a token, $\tau$ sends each finite recognition trace to an expression, and $\tau$ is monotone: if trace $U$ extends trace $T$ then $\tau(T) \preceq_E \tau(U)$.
background
Primitive Recognition Calculus (PRC) treats the first act of recognition as a two-sided distinction $\delta$ with endpoints (left/right) and finite traces built by successive extension. An endpoint is one side of that distinction; a trace is a finite chain of recognition steps, ordered by the extension relation Trace.Extends.
This module sits under the foundation layer that feeds the Inevitability Theorem: any zero-parameter alternative that derives observables must reduce to RS structure or violate a necessity gate. Before that comparison can be stated inside Lean, external foundations need a common surface on which $\delta$ and finite traces are visible.
The structure supplies exactly that surface. Tokens and expressions are opaque carriers belonging to the candidate system; distinguishes and exprExtends are the only structural relations required so that the primitive distinction and trace extension can be read off inside it. The maps endpointToken and traceExpr are the interpretation arrows from PRC data into those carriers, with monotonicity of traceExpr as the sole coherence axiom.
proof idea
No proof body: this is a structure definition. The only propositional field is the monotonicity axiom traceExpr_extends, which asserts that whenever one finite trace extends another, the corresponding expressions stand in the system's extension relation. Instantiating the structure means choosing carriers, relations, and maps that satisfy that single forall.
why it matters
This is the Build Order step-12 surface for PRC inevitability. Every later object in the module is typed over it: expressiveness (the system distinguishes the two endpoint tokens), PRC embeddings into a system (maps that preserve distinction and trace extension), the canonical PRC formal system (endpoints as tokens, traces as expressions), the embedding-target proposition (every expressive system admits a PRC embedding), and the FormalSystemCertificate that closes the surface and embedding theorem.
Downstream, AdmissibleFoundation and ExternalFoundationParsingTarget in the Inevitability module consume the same interface, so alternative foundations are forced to present tokens, expressions, and a readable $\delta$. That is the first gate on the path to the core inevitability claim (no zero-parameter alternative derives observables without reducing to RS or violating a necessity gate). The structure itself does not yet assert uniqueness of RS; it only fixes the language in which that claim is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.