PRCFormalSystem
plain-language theorem explainer
The Primitive Recognition Calculus is packaged as a minimal formal system: tokens are endpoints of the primitive distinction, expressions are finite traces, and distinction is ordinary inequality. Anyone citing the PRC inevitability layer or the Step 12 formal-system certificate uses this carrier. The construction is definitional: identity maps on endpoints and traces, with extension preserved by the given hypothesis.
Claim. Instantiate the minimal formal-system interface by taking tokens to be endpoints of the primitive distinction $\delta$, expressions to be finite traces, distinction to be inequality of endpoints, and expression extension to be trace extension. The maps from endpoints to tokens and from traces to expressions are the identity, and they send trace extension to expression extension.
background
The module supplies a thin formal-system interface used by the PRC inevitability theorem. A FormalSystem carries two types (tokens and expressions), a binary distinction relation on tokens, an extension preorder on expressions, and structure maps that embed the PRC primitives: endpoints into tokens and finite traces into expressions, with the requirement that trace extension is preserved.
Upstream, an endpoint is one side of the primitive distinction $\delta$ (K2.3). A finite trace is a word in those sides; Extends T U means $U$ is $T$ followed by some suffix (K2.5). Distinction inside PRC is simply inequality of endpoints.
The local goal is not to invent a new logic, but to exhibit PRC itself as one concrete instance of that interface, so later certificates can quantify over arbitrary foundations that look like PRC from the outside.
proof idea
Pure structure instantiation. Tokens are endpoints, expressions are traces, distinction is $\neq$, and expression extension is trace extension. Both structure maps are the identity function. The only proof obligation is preservation of extension under the trace-to-expression map: given Trace.Extends T U, the same hypothesis is returned unchanged, since the map is id.
why it matters
This is the canonical carrier for Step 12 of the formal-system surface. Downstream, PRCFormalSystem_expressive records that left and right endpoints are distinct, and PRCFormalSystem_embedding obtains a nonempty embedding of PRC into itself via the proved embedding-target lemma. Those two facts, together with this instance, close FormalSystemCertificate ("the formal-system surface and embedding theorem are closed").
In the inevitability layer it is the system field of PRCAdmissibleFoundation, so PRC counts as an admissible foundation in its own interface. The distinction dichotomy uses it as the reflexive example: prcFormalSystem_exprReflexive is just trace-extension reflexivity, feeding the headline that distinction is not optional except for the fully degenerate foundation.
Framework-wise this sits under the Primitive Recognition Calculus foundation work that precedes the forcing chain (T0–T8); it does not itself force $\phi$, the eight-tick octave, or $D=3$, but it is the formal-system witness those later layers assume when they treat PRC as admissible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.