PRCUniversalFoundationConditionalCertificate
plain-language theorem explainer
Packages every built Primitive Recognition Calculus surface into one conditional Prop: kernel first-pass, promoted reals, trace logic, formal system, inevitability, recognizer bridge, native-cost blocker, and the open-target ledger of repaired versus refuted uniqueness routes. Anyone citing the PRC universal-foundation stack uses this bundle. It is a pure structure definition, not a proved theorem; the inhabitant is assembled elsewhere.
Claim. A proposition asserting simultaneous possession of: a kernel first-pass certificate; a promoted real complete ordered-field certificate; a trace-logic certificate; a formal-system certificate; a PRC inevitability certificate; a recognizer-bridge certificate; a native-cost uniqueness blocker certificate; the historical open-target ledger (refuted unsigned/zero-calibrated routes together with the repaired signed/prime/zero-calibrated uniqueness surface); and a trivial classical-extension strength-tag audit $s=s$.
background
Primitive Recognition Calculus (PRC) is the foundation layer that forces the recognition cost, the real continuum, and the formal skeleton before physics constants appear. The module assembles those surfaces into a single top-level certificate rather than leaving them as scattered lemmas.
The open-target ledger records which native-cost uniqueness routes survive. Positive entries name repaired interfaces (signed, prime, zero-calibrated uniqueness); negative entries are explicit refutations of weaker unsigned or inadmissible factorizations. That ledger is the mathematical content of the historical-target structure carried here.
Upstream inevitability states the no-alternatives claim: any zero-parameter framework that derives observables either reduces to the RS cost and selection or violates a necessity gate. Cost throughout is the $J$-cost on positive ratios (or its multiplicative-recognizer derived form). The kernel, rung-coarsen, and observer-forcing cost defs supply the same $J$-shaped recognition cost that T5 uniqueness later pins down.
proof idea
No proof body: this is a structure definition of type Prop. Each field is a named hypothesis surface (certificate) that a later theorem must supply. The only non-certificate field is the trivial equality audit on the classical-extension strength tag, which is definitionally true and serves as a project-local axiom check rather than mathematical content. Instantiation is deferred to the companion theorem that fills every field from existing certificates.
why it matters
This is the conditional spine of the PRC universal foundation. Downstream, the final unconditional certificate reuses the same surface list and closes the top-level theorem by carrying the built PRC surfaces with the exact native-cost ledger: repaired signed/prime/zero-calibrated uniqueness proved, weaker unsigned routes recorded as refuted. The companion inhabitant theorem constructs one instance of this structure from the already-proved component certificates.
In the Recognition forcing chain this sits above T5 $J$-uniqueness and the Recognition Composition Law: it packages the formal and cost surfaces that make those uniqueness results usable as a single foundation claim. The open-target ledger is the honest residual: which native-cost routes are closed and which are permanently blocked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.