PRCAdmissibleFoundation
plain-language theorem explainer
Primitive Recognition Calculus is packaged as an admissible foundation: a formal system expressive enough to separate the two endpoints of the primitive distinction. Anyone proving the first inevitability theorem or assembling the Step 13 certificate cites this instance. The definition is a two-field structure value that plugs in the PRC formal system and its expressiveness theorem.
Claim. Let an admissible foundation be a pair $(S,E)$ where $S$ is a formal system and $E$ asserts that $S$ can distinguish the two endpoints of the primitive distinction $\delta$. Then Primitive Recognition Calculus, with endpoint tokens, finite-trace expressions, and inequality as distinction, is such a pair: its expressiveness holds because the left and right endpoints are unequal.
background
In the Primitive Recognition Calculus inevitability module, an admissible foundation is the minimal interface for the first inevitability theorem: a formal system together with a proof that it is expressive enough to distinguish the two endpoints of $\delta$. Expressiveness is the system's ability to separate those endpoints; without it the embedding story cannot start.
Upstream, PRC is already presented as a concrete formal system: tokens are endpoints, expressions are finite traces, distinction is inequality of endpoints, and expression extension is trace extension. A short theorem records that this system is expressive, by the elementary fact that the left endpoint is not the right endpoint.
The local setting is the admissible-interface layer of the inevitability argument: fix what counts as a foundation, exhibit PRC as one, then show every such foundation presupposes distinction and therefore admits a PRC embedding.
proof idea
Definitional construction, not a tactic proof. The structure AdmissibleFoundation has two fields. The system field is filled by the existing PRC formal system (endpoints as tokens, traces as expressions). The expressive field is filled by the theorem that this system is expressive, which itself is a one-line appeal to inequality of the two endpoints. No further rewriting is required.
why it matters
This instance is the concrete witness that the admissible-foundation surface is inhabited by PRC itself. Downstream, the embedding theorem applies the general "any foundation presupposes distinction" result to this instance, yielding a nonempty PRC embedding into PRC's own system. The Step 13 inevitability certificate structure records both a nonempty admissible foundation and a specifically PRC-admissible foundation; both fields are discharged by pointing at this definition. The certificate deliberately separates the closed admissible-interface theorem from the remaining external-parsing workload, so this def closes the internal half without smuggling in corpus-level claims. In the broader Recognition forcing picture it sits at the formal-system root: before J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$, one needs a foundation that can even state distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.