PRCEmbeddingInto
plain-language theorem explainer
An embedding of the primitive recognition calculus into a formal system is a pair of maps sending the two endpoints to tokens and finite traces to expressions, required to preserve left/right distinction and the extension order on traces. Anyone showing that an expressive formal system can host the PRC surface cites this structure. The canonical instance is assembled from the system's own endpoint and trace interpretation fields once expressiveness holds.
Claim. For a formal system $F$ (token type, expression type, a distinction predicate on tokens, and an extension relation on expressions), a PRC embedding into $F$ is a pair of maps $e:\{\mathrm{left},\mathrm{right}\}\to\mathrm{Token}_F$ and $t:\mathrm{Trace}\to\mathrm{Expr}_F$ such that $F$ distinguishes $e(\mathrm{left})$ from $e(\mathrm{right})$, and whenever a finite trace $T$ extends to $U$, the image $t(T)$ extends to $t(U)$ under $F$'s expression-extension relation.
background
The Primitive Recognition Calculus (PRC) treats a bare two-point distinction (left versus right endpoint) and finite traces built by successive extension as the minimal data any foundation must already support before arithmetic or dynamics appear. The ambient module supplies a thin formal-system interface: carrier types for tokens and expressions, a binary distinction predicate on tokens, an extension relation on expressions, plus built-in interpretation maps from endpoints and traces into those carriers, with the interpretation required to respect trace extension.
A formal system is called expressive (for the first inevitability pass) precisely when its own endpoint interpretation already distinguishes left from right. That single propositional condition is the gate for the embedding construction. The local setting is Build Order step 12: close the formal-system surface and the embedding theorem before the broader claim that every external foundation satisfies the interface.
proof idea
The declaration is a structure (data plus two preservation fields), not a proved theorem. The companion constructor from expressiveness is a one-line field assembly: send endpoints through the system's endpoint-token map, send traces through its trace-expression map, discharge distinction by the expressiveness hypothesis, and discharge trace-extension preservation by the system's built-in traceExpr_extends axiom. Downstream, the step-12 target is proved by introducing an arbitrary expressive $F$ and packaging that constructor as a witness of nonemptiness.
why it matters
This structure is the payload of Build Order step 12. The exact target states that every expressive formal system admits a nonempty PRC embedding; that target is discharged by the of-expressive constructor, and the certificate records surface nonemptiness, expressiveness of the PRC system, a nonempty embedding into it, and the closed target. The same embedding type is required of every admissible foundation in the step-13 inevitability certificate (any_foundation_embedding), and appears in the category-theory parse that external foundations realize the primitive distinction. It does not yet claim that every external foundation is expressive; that is the next inevitability layer, kept explicit rather than hidden inside the structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.