PRCAdmissibleFoundation_embeds
plain-language theorem explainer
Primitive Recognition Calculus, treated as an admissible foundation, admits a nonempty embedding of its own endpoint-and-trace core into its formal system. Anyone citing the PRC inevitability certificate needs this self-embedding fact. The proof is a one-line specialization of the general lemma that every admissible foundation already presupposes a PRC distinction core.
Claim. There exists a PRC embedding into the formal system of the admissible foundation given by Primitive Recognition Calculus itself: a map of endpoints and finite traces that preserves the left/right distinction and trace extension.
background
In the Primitive Recognition Calculus (PRC) layer, a formal system is expressive when it can distinguish two primitive endpoints and extend finite traces. A PRC embedding into such a system is a structure that maps the two endpoints and traces into the system's tokens and expressions while preserving distinction and finite trace extension.
An admissible foundation is a pair of an expressive formal system together with that expressiveness witness. The module treats PRC itself as one such admissible foundation: its system is the PRC formal system, already shown expressive.
Upstream, any foundation already parsed into this admissible interface is known to presuppose a PRC trace core: specializing that target to a concrete admissible foundation yields a nonempty embedding of the PRC primitives into that foundation's system. The broader RS inevitability claim (any zero-parameter alternative either reduces to RS or violates a necessity gate) sits one layer above this parsing interface.
proof idea
One-line term proof. Apply any_foundation_presupposes_distinction to the concrete admissible foundation PRCAdmissibleFoundation. That general lemma is itself a short intro-and-exact over the proved embedding target for any expressive formal system, so specializing to PRC's own system immediately gives Nonempty (PRCEmbeddingInto PRCFormalSystem).
why it matters
This closes the self-application leg of the PRC inevitability surface: PRC is not only the source of the distinction core, it embeds into itself as an admissible foundation. The sole downstream consumer is prc_inevitability_certificate, which packages the admissible-foundation surface, the PRC-admissible witness, the general inevitability target, and the any-foundation embedding into one certificate structure.
In the Recognition Science forcing picture this is bookkeeping for the "no alternatives" claim at the formal-system layer, not a derivation of J-cost, phi, the eight-tick octave, or D = 3. It ensures the inevitability interface applies cleanly when the foundation under audit is PRC itself, so the certificate does not leave a self-reference hole.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.