PRCFormalSystem_embedding
plain-language theorem explainer
There is a non-empty embedding of the primitive recognition calculus into its own minimal formal-system presentation: endpoints map to endpoint tokens and finite traces map to expressions, preserving distinction and extension. Anyone assembling the Step 12 formal-system certificate cites this. The proof is a one-line application of the general expressive-to-embedding target to PRC itself.
Claim. The set of embeddings of the primitive recognition calculus into the minimal formal system $F_{\mathrm{PRC}}$ (tokens $=$ endpoints, expressions $=$ finite traces, distinction $=$ inequality, expression extension $=$ trace extension) is non-empty: there exist maps on endpoints and traces that preserve left/right distinction and finite trace extension.
background
In this module a formal system is a token/expression surface with a distinction predicate on tokens and an extension relation on expressions, plus interpretations of the two primitive endpoints and of finite traces. Expressiveness means the two endpoint tokens are distinguished.
A PRC embedding into a formal system $F$ is a pair of maps (endpoints $\to$ tokens, traces $\to$ expressions) that preserve the left/right distinction and send trace extension to expression extension. The structure PRCEmbeddingInto packages exactly those preservation laws.
$F_{\mathrm{PRC}}$ is the identity presentation: tokens are endpoints, expressions are traces, distinction is $\neq$, and extension is trace extension. Upstream, every expressive formal system admits such an embedding via its own interpretation fields (FormalSystemEmbeddingTarget_proved), and $F_{\mathrm{PRC}}$ is expressive because the two endpoints are unequal.
proof idea
One-line term proof. Apply FormalSystemEmbeddingTarget_proved to $F_{\mathrm{PRC}}$ together with the already-proved fact that $F_{\mathrm{PRC}}$ is expressive (PRCFormalSystem_expressive, which is just Endpoint.left_ne_right). The general target returns a witness of PRCEmbeddingInto F for any expressive $F$, hence a non-emptiness proof for the self-embedding.
why it matters
This closes the self-embedding half of the Step 12 formal-system surface. Downstream, formal_system_certificate bundles the surface, expressiveness, this embedding, and the general embedding-target theorem into one certificate; its doc-comment states that the broader claim that every external foundation satisfies the interface is the next inevitability layer, not hidden here.
In the Recognition forcing picture this is bookkeeping for the primitive calculus that underwrites later structure (eight-tick octave, $D=3$, cost uniqueness), not a physics derivation itself. It feeds the inevitability stack by showing the native formal system meets the same embedding interface demanded of external foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.