FormalSystemEmbeddingTarget
plain-language theorem explainer
Exact Build Order step-12 target: every expressive formal system admits a Primitive Recognition Calculus embedding that preserves endpoint distinction and finite trace extension. Cited by the step-12 certificate and by anyone closing the formal-system inevitability layer. Pure Prop definition packaging that universal claim; the companion theorem discharges it by constructing the embedding from expressiveness.
Claim. For every formal system $F$, if $F$ distinguishes the two primitive endpoints, then there exists a PRC embedding of endpoints and finite traces into $F$ that preserves distinction and trace extension.
background
The module supplies a minimal formal-system interface for the Primitive Recognition Calculus (PRC) inevitability theorem: carriers for tokens and expressions, a distinction relation, an expression-extension relation, and a map sending the two primitive endpoints to tokens. Expressiveness means the system distinguishes those two endpoint tokens, i.e. it can see the primitive distinction $\delta$.
A PRC embedding into such a system is a pair of maps (endpoints to tokens, finite traces to expressions) that preserve endpoint distinction and finite trace extension. The local setting is Build Order step 12: state the precise surface claim that every expressive formal system hosts such an embedding, before certifying that the surface and the embedding theorem are closed.
Upstream, expressiveness is exactly the first-inevitability-pass condition that the two endpoint tokens are distinguished; the embedding structure records the preservation obligations that make $\delta$ and trace growth visible inside an arbitrary verifier-side formal system.
proof idea
Definition only: the body is the Prop $\forall F,, \mathrm{Expressive}(F)\to \mathrm{Nonempty}(\mathrm{PRCEmbeddingInto}, F)$. No proof work here. The companion theorem discharges it in one step by introducing an expressive $F$ and packing the constructive embedding PRCEmbeddingInto.ofExpressive.
why it matters
Pins the exact target proposition for Build Order step 12 on the formal-system surface. Downstream, FormalSystemCertificate requires this target as a field and records that the surface and embedding theorem are closed, while leaving the broader claim that every external foundation satisfies the interface to a later inevitability layer. The proved companion fills the target by constructing the embedding from expressiveness alone. In the Recognition stack this is scaffolding for the inevitability chain: once expressive systems must host a PRC embedding, the primitive distinction and eight-tick trace structure can be read inside any such calculus, feeding the forcing path toward unique $J$, $\varphi$, and the octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.