FormalSystemCertificate
plain-language theorem explainer
Step-12 certificate bundling the closed formal-system surface for Primitive Recognition Calculus: PRC is itself a formal system, is expressive, embeds into itself, and every expressive formal system admits a PRC embedding. Foundation auditors cite it when assembling kernel and universal-foundation certificates. It is a pure Prop structure; the witnessing theorem fills the fields from prior lemmas.
Claim. A Step-12 formal-system certificate is the conjunction of: (i) the class of minimal formal systems is inhabited; (ii) the PRC formal system (endpoints as tokens, finite traces as expressions) distinguishes the two primitive endpoints; (iii) there is a PRC embedding of that system into itself; (iv) the embedding target holds: every expressive formal system $F$ admits a nonempty PRC embedding into $F$; and (v) a trivial strength-tag identity recording the $\delta$-only strength level.
background
In the Primitive Recognition Calculus formal-system module, a formal system is a minimal interface: carrier types for tokens and expressions, a distinction relation on tokens, an extension relation on expressions, and interpretations of endpoints and finite traces. Expressiveness means the system distinguishes the two endpoints of the primitive distinction $\delta$.
A PRC embedding into a formal system $F$ is a pair of maps (endpoints to tokens, traces to expressions) that preserve endpoint distinction and finite-trace extension. The embedding target (Build Order step 12) asserts that every expressive $F$ admits such an embedding. PRC itself is realized as a formal system by taking tokens to be endpoints, expressions to be traces, distinction to be inequality, and extension to be trace extension.
The certificate packages surface existence, PRC expressiveness and self-embedding, the universal embedding target, and a $\delta$-only strength tag. The doc-comment stresses that broader inevitability for every external foundation is a later layer, not smuggled into this bundle.
proof idea
No proof body: this is a structure ... : Prop definition. Inhabitation is supplied by the sibling theorem formal_system_certificate, which fills each field from prior results: nonempty surface via PRCFormalSystem; expressiveness via PRCFormalSystem_expressive; self-embedding via PRCFormalSystem_embedding; and both the embedding-target field and the quantified embedding-from-expressive field via FormalSystemEmbeddingTarget_proved. The strength tag is the reflexivity identity on StrengthTag.deltaOnly.
why it matters
This is the closed Step-12 surface in the PRC foundation stack. Downstream, formal_system_certificate witnesses the structure; KernelFirstPassCertificate sits in the same first-pass bundling layer (analytic stages with concrete Lean objects, not yet full inevitability); and both PRCUniversalFoundationCertificate and PRCUniversalFoundationConditionalCertificate require a formal_system : FormalSystemCertificate field when composing kernel, real-complete ordered field, trace logic, and formal-system surfaces into the top-level universal-foundation claim.
In Recognition Science terms it records that the primitive distinction and finite-trace calculus sit inside a minimal formal-system interface and embed into every expressive host, so later forcing (J-uniqueness, $\phi$, eight-tick structure) is not hostage to a proprietary syntax. The doc-comment explicitly leaves open the next inevitability layer: that every external foundation satisfies the interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.