FormalSystemEmbeddingTarget_proved
plain-language theorem explainer
Every expressive formal system admits a nonempty PRC embedding: a map of endpoint tokens and finite traces that preserves the left/right distinction and trace extension. Foundation and inevitability arguments cite this as Build Order step 12. The proof is a two-line tactic that packages the existing ofExpressive constructor into the universal target proposition.
Claim. For every formal system $F$, if $F$ is expressive (can distinguish two tokens and extend expressions), then there exists a PRC embedding into $F$: maps from endpoints and finite traces into $F$'s tokens and expressions that preserve the primitive left/right distinction and finite trace extension.
background
Primitive Recognition Calculus (PRC) treats recognition as the minimal distinction between two endpoints (left vs right) together with finite traces built by successive extension. A formal system here is an abstract carrier with tokens, expressions, a distinguishability relation, and an expression-extension operation.
Expressiveness means the system can separate at least two tokens and close expressions under extension. A PRC embedding into such a system is a structure-preserving map: endpoints go to tokens, traces to expressions, the endpoint distinction is reflected by the system's distinguishability, and trace extension is reflected by expression extension.
The target proposition (Build Order step 12) asserts that every expressive formal system carries at least one such embedding. The local module packages that claim as a single Prop so certificates and inevitability theorems can cite one closed fact rather than rebuild the quantifiers.
proof idea
Tactic proof. Introduce an arbitrary formal system $F$ and the hypothesis that $F$ is expressive. Discharge the goal by supplying a witness of type Nonempty (PRCEmbeddingInto F), namely the structure produced by the existing constructor PRCEmbeddingInto.ofExpressive applied to $F$ and that expressiveness hypothesis. No further case analysis or rewriting is required; the constructor already builds the endpoint and trace maps and proves the two preservation fields.
why it matters
Closes Build Order step 12: the formal-system embedding target is proved, not left as an interface. The step-12 certificate records this fact twice (as the embedding target and as the expressive-to-embedding arrow). Downstream, the same lemma is the one-line engine for concrete δ-core embeddings: Boolean logic (true/false), hereditarily finite set theory, full ZFC, and a topos-style categorical foundation each obtain a nonempty PRC embedding by applying this theorem to their expressive witnesses.
It also feeds the inevitability claim that any foundation already parsed into the admissible interface presupposes a PRC trace core: that argument simply specializes this universal statement to the parsed system. In the Recognition framework this is the bridge from the primitive left/right distinction (the δ core) to the claim that standard foundations already contain that core once they can distinguish and extend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.