AdmissibleFoundation
plain-language theorem explainer
An admissible foundation packages a formal system with a witness that it distinguishes the two endpoints of the primitive distinction δ. Anyone stating the first PRC inevitability theorem quantifies over this type: every such foundation must admit a PRC embedding. Pure structure definition; the only content is the pair (system, expressiveness).
Claim. An admissible foundation is a pair $(F, e)$ where $F$ is a formal system (tokens, expressions, a distinguishability relation, and endpoint tokens for $\delta$) and $e$ witnesses that $F$ distinguishes the left and right endpoint tokens of the primitive distinction $\delta$.
background
The Primitive Recognition Calculus (PRC) inevitability module asks which formal foundations already contain enough structure to host the first recognition step. A formal system here is a minimal interface: carrier types for tokens and expressions, a binary distinguishability predicate, an expression-extension relation, and a map sending each endpoint of $\delta$ to a token.
Expressiveness is the single gate for this pass: the system must distinguish the left endpoint token from the right. That is exactly the content needed so that $\delta$ is visible inside the foundation rather than smuggled in by metalanguage.
Upstream, the broader RS Inevitability Theorem asserts that any zero-parameter alternative that derives observables either reduces to RS (same cost and selection) or violates a necessity gate. This structure is the local, PRC-side domain for the first step of that program.
proof idea
No proof body: this is a structure declaration. It bundles a FormalSystem with a term of its Expressive predicate (distinguishability of the two $\delta$ endpoint tokens). Downstream objects inhabit the type by supplying those two fields.
why it matters
This is the quantification domain for the first PRC inevitability target: every admissible foundation admits a nonempty PRC embedding into its system. That target is the content of the Step-13 certificate surface, which records nonempty admissible foundations, that PRC itself is admissible, the embedding target, and the universal embedding claim.
PRC is exhibited as one inhabitant (its formal system plus the expressiveness witness). The structure therefore separates the interface hypothesis (what counts as a foundation for the theorem) from the external parsing workload of showing that a given foundation meets it. In the forcing-chain picture this sits under the inevitability / no-alternatives claim rather than under T5–T8 numerics: it is about which logics can host the primitive distinction at all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.