ExternalFoundationParsingTarget
plain-language theorem explainer
Names the remaining external-parsing obligation for PRC inevitability: once a corpus of external foundations and a faithful-parse relation are fixed, every external object must parse to some expressive formal system. The Step 13 inevitability certificate and the universal-foundation open-target ledger cite this schema so the parsing workload stays explicit. Pure definitional Prop; no proof content.
Claim. Fix a type $\mathcal{E}$ of external foundations and a relation $P$ of faithful parses from $\mathcal{E}$ into formal systems. The external parsing target is the assertion that for every $e \in \mathcal{E}$ there exists a formal system $F$ with $P(e,F)$ such that $F$ is expressive: $F$ distinguishes the two primitive endpoint tokens.
background
Primitive Recognition Calculus (PRC) inevitability works against a minimal formal-system interface: carriers for tokens and expressions, a binary distinction predicate on tokens, an extension relation on expressions, and a map sending the two primitive endpoints (left/right) to tokens. A formal system is expressive, for the first inevitability pass, precisely when it distinguishes those two endpoint tokens.
The module separates closed internal surface facts from residual external work. Admissible foundations and PRC embeddings into them are handled on the internal side. What remains, before inevitability can be applied to an outside corpus, is a uniform parsing demand: every external foundation object must land in some expressive formal system under a chosen faithful-parse relation.
This declaration is that demand as a Prop schema, parameterized by the external corpus type and the parse relation. It does not pick a particular logic or encoding; it only records the quantifier shape the later certificate treats as the external workload.
proof idea
Definitional, not a proved theorem. The body is the single quantified proposition $\forall e,,\exists F,, P(e,F)\land\mathrm{Expressive}(F)$, with $P$ the supplied faithful-parse relation and expressiveness the endpoint-distinction predicate on the minimal formal-system interface. No lemmas are applied; unfolding is the entire content.
why it matters
Keeps the external parsing burden visible rather than folding it into the closed admissible-interface theorem. Downstream, the Step 13 structure PRCInevitabilityCertificate packages nonempty admissible foundations, the inevitability target, and universal embedding into admissible systems; the companion doc states the admissible-interface theorem is closed and names the external parsing workload separately so it is not hidden. The universal-foundation open-target ledger likewise tracks residual obligations against the conditional top-level certificate.
In framework terms this sits under the foundation forcing story (distinction before cost, before $\phi$ and the eight-tick octave): inevitability only fires after outside foundations have been reduced to expressive formal systems that can see the primitive distinction. The schema is the exact remaining gate on that reduction, not a physics derivation itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.