PRCInevitabilityCertificate
plain-language theorem explainer
Step-13 certificate packaging the closed admissible-interface half of PRC inevitability: every admissible foundation admits a PRC embedding, PRC itself is admissible, and the external-parsing workload is named as a separate schema rather than buried in the theorem. Foundation auditors and universal-foundation certificate builders cite it. It is a pure Prop-structure bundling nonempty witnesses and a tautological schema tag; no proof body.
Claim. A Step-13 inevitability certificate is a proposition asserting: (i) the class of admissible foundations is inhabited; (ii) PRC itself is an admissible foundation; (iii) the first inevitability target holds, namely every admissible foundation $A$ admits a PRC embedding into $A$'s formal system; (iv) PRC embeds into its own admissible system; (v) the external-foundation parsing schema is recorded by name (for any external corpus and faithful-parse relation, every external object must parse to an expressive formal system before inevitability applies); (vi) the strength tag is fixed at $\delta$-only.
background
The Primitive Recognition Calculus (PRC) inevitability module works over a minimal formal-system interface: carriers for tokens and expressions, a distinction relation, and an expression-extension relation, together with endpoint tokens for the two sides of the primitive distinction $\delta$. A PRC embedding into such a system maps endpoints and finite traces so that endpoint distinction and trace extension are preserved.
An admissible foundation is exactly a formal system expressive enough to distinguish the two endpoints of $\delta$. The first inevitability target is the statement that every such foundation admits a PRC embedding. PRC itself is packaged as one admissible foundation via its native formal system. Separately, the external parsing target schema says: once a corpus of external foundations and a faithful-parse relation are fixed, every external object must parse to an expressive formal system before the inevitability theorem applies to it.
The module doc and certificate doc fix the division of labor: the admissible-interface theorem is closed inside this certificate; the external parsing workload is named so it is not hidden inside the theorem statement.
proof idea
No proof body: this is a Prop-valued structure (certificate schema), not a theorem. Each field is a named obligation. The nontrivial mathematical content is the inevitability target and the universal embedding clause, both of type $\forall A,,\mathrm{Nonempty}(\mathrm{PRCEmbeddingInto}, A.\mathrm{system})$, i.e. every admissible foundation carries a PRC embedding. The external-parsing field is intentionally a reflexive equality on the named schema, recording the residual workload without asserting it. The strength tag is a trivial $\delta$-only identity. Instantiation is deferred to the companion theorem that fills the fields with concrete witnesses (PRC as admissible foundation, and the any-foundation-presupposes-distinction lemma).
why it matters
This is the Step-13 bundling point for the first PRC inevitability theorem on the admissible interface. Downstream, prc_inevitability_certificate constructs an inhabitant by supplying PRC as the admissible surface and routing the embedding clauses through the any-foundation-presupposes-distinction result. The same certificate type is consumed by the kernel first-pass certificate and by both the unconditional and conditional universal-foundation certificates, which close the top-level PRC stack (kernel, ordered field, trace logic, formal system) with the native-cost ledger.
In framework terms it sits under the foundation forcing chain: before J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8) can be forced inside a host system, that host must already carry a PRC embedding of the primitive $\delta$-distinction. Naming external parsing separately keeps the closed half of the theorem honest: inevitability is proved for admissible interfaces; applying it to an arbitrary external foundation still requires a faithful parse into an expressive formal system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.