PRCInevitabilityTarget
plain-language theorem explainer
The first inevitability target asserts that every admissible foundation admits a nonempty PRC embedding into its formal system. Anyone citing the PRC inevitability certificate or the admissible-interface theorem will reference this proposition. It is a pure Prop abbreviation packaging a universal quantification over admissible foundations.
Claim. The first inevitability target is the proposition that for every admissible foundation $A$ (a formal system expressive enough to distinguish the two endpoints of $\delta$), the type of PRC embeddings into $A$'s system is nonempty. A PRC embedding maps endpoints and traces so as to preserve primitive endpoint distinction and finite trace extension.
background
The Primitive Recognition Calculus (PRC) treats recognition as a minimal formal system built from endpoint distinction and finite trace extension. An admissible foundation is a pair consisting of a formal system together with an expressiveness witness: the system can distinguish the two endpoints of the primitive distinction $\delta$.
A PRC embedding into a formal system $F$ is a structure with maps on endpoints and traces that preserve distinction of the left and right endpoints and preserve finite trace extension. The inevitability module packages the claim that every such admissible foundation already contains a PRC core via such an embedding.
Local setting: this module states the first inevitability theorem at the admissible-interface level, separating the closed interface theorem from any external parsing workload that would turn an arbitrary foundation into an admissible one.
proof idea
No proof body: this is a definitional abbreviation of a proposition. The right-hand side is the universal statement $\forall A : \mathrm{AdmissibleFoundation},; \mathrm{Nonempty}(\mathrm{PRCEmbeddingInto}, A.\mathrm{system})$. Downstream theorems discharge it by introducing an arbitrary admissible foundation and applying the proved embedding target for expressive formal systems.
why it matters
This Prop is the exact first inevitability target named in the module. The theorem any_foundation_presupposes_distinction proves it: any foundation already parsed into the admissible interface presupposes a PRC trace core. The Step 13 certificate structure PRCInevitabilityCertificate records it as a named field (inevitability_target), keeping the closed admissible-interface result separate from external parsing obligations.
In the Recognition Science forcing picture, this is the interface-level claim that distinction-capable foundations cannot avoid a PRC core. It does not itself invoke T5–T8 (J-uniqueness, $\varphi$, eight-tick octave, $D=3$), but it sits under the foundation layer those landmarks rest on: without forced distinction structure, the later chain has nothing to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.