PRCUniversalFoundationCertificate
plain-language theorem explainer
Bundles every closed Primitive Recognition Calculus surface into one top-level foundation certificate, with the exact native-cost uniqueness ledger. Anyone citing the PRC universal foundation points here: kernel, complete ordered field, trace logic, formal system, inevitability, recognizer bridge, and repaired-versus-refuted cost routes. Pure packaging of already-proved certificates; the inhabiting theorem fills fields from the conditional certificate.
Claim. A universal-foundation certificate for the Primitive Recognition Calculus is a proposition packing: a first-pass kernel certificate; a promoted complete ordered-field certificate on the internal null quotient; a trace-logic certificate; a formal-system certificate with embedding; an inevitability certificate for admissible foundations; a recognizer-bridge certificate; a native-cost uniqueness blocker; the open-target ledger of repaired versus refuted native-cost routes; the matching conditional certificate; and a trivial audit that no project-local strength-tag axioms were introduced.
background
Primitive Recognition Calculus (PRC) builds a foundation stack from a first-pass kernel (strength tags, finite traces, judgments, and a stable trace-logic surface) up through a promoted complete ordered field on the internal null quotient, a formal-system surface with embedding, and an inevitability layer for admissible foundations. The kernel certificate bundles concrete Lean objects for each stage of the first theorem chain; it is not yet the final inevitability claim.
Native cost uniqueness is handled separately. The blocker certificate records that uniqueness is not fully closed: missing mathematics is split into exact targets, with several weaker unsigned or signed-admissible routes already refuted. The open-targets ledger carries those positive repaired interfaces and negative refutations by name.
The conditional certificate is the same stack without the final audit field. Upstream inevitability (the RS core no-alternatives claim) sits one layer out: any zero-parameter alternative that derives observables either reduces to RS cost and selection or violates a necessity gate.
proof idea
No proof body: this is a Prop-valued structure definition. Each field is a named certificate or ledger already defined upstream (kernel first-pass, promoted real complete ordered field, trace logic, formal system, PRC inevitability, recognizer bridge, native-cost uniqueness blocker, open targets, and the conditional certificate). The final field is a trivial reflexivity audit on the classical-extension strength tag, forcing an explicit no-local-axioms check into the type. Inhabitation is deferred to the theorem that constructs an instance by projecting fields from the conditional certificate.
why it matters
This is the final PRC universal-foundation certificate: it closes the top-level theorem by carrying every built PRC surface together with the exact native-cost ledger (repaired signed/prime/zero-calibrated uniqueness route proved; weaker unsigned routes recorded as refuted). Downstream, the theorem prc_universal_foundation inhabits exactly this structure by copying fields from the conditional certificate.
In the Recognition framework it packages the foundation half of the forcing story before the T5-T8 chain (J-uniqueness, phi, eight-tick octave, D = 3). It keeps the inevitability surface honest: admissible-foundation and formal-system embeddings are present as certificates, while native-cost uniqueness remains a named blocker-plus-ledger rather than a hidden sorry. The open-targets ledger is the audit trail for which cost routes are closed and which are refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.