prc_universal_foundation_conditional_certificate
plain-language theorem explainer
Assembles every built Primitive Recognition Calculus foundation surface into one conditional certificate, with the native-cost uniqueness ledger of proved and refuted targets named explicitly. Anyone citing the universal foundation stack uses this as the single composition point. The proof is a structure assembly that wires already-proved certificates and the open-target ledger field-by-field.
Claim. There is a conditional universal foundation certificate for the Primitive Recognition Calculus: the first-pass kernel, the promoted real complete ordered field, trace logic, the formal system, inevitability, the recognizer bridge, and the native-cost uniqueness blocker all hold, together with an explicit ledger of proved and refuted native-cost character and calibration targets.
background
Primitive Recognition Calculus (PRC) packages the Recognition Science foundation as a stack of certificate surfaces: a first-pass kernel (strength tags, empty trace, equality judgment), a promoted real complete ordered field, trace logic, a formal system with embedding, an inevitability surface, and a recognizer bridge. The native-cost side tracks uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$ under admissible characters, calibration choices, and prime-orientation constraints.
The conditional certificate is the Prop that all of those surfaces inhabit simultaneously, while exposing a named open-target ledger of which native-cost uniqueness and orientation claims are proved versus refuted. Upstream, the first-pass kernel certificate (K7/A2) already bundles strength tags and trace logic; the inevitability certificate records that any admissible foundation presupposes distinction; the formal-system certificate records expressiveness and embedding. The native-cost uniqueness module supplies the proved/refuted targets that fill the ledger (prime-orientation coherence, mixed-pair absurdities, calibration refutations, and related character rigidity facts).
Local setting: this module is the composition layer for the universal foundation claim, not a new analytic derivation of $J$ or of the forcing chain.
proof idea
Tactic-mode structure construction. Each field of the conditional certificate is filled by an existing certificate theorem: first-pass kernel, promoted real complete ordered field, trace logic, formal system, PRC inevitability, recognizer bridge, and the native-cost uniqueness blocker.
The open_targets record is assembled entry-by-entry from the native-cost uniqueness module: zero-calibration uniqueness and signed-admissible factorization are marked refuted; character factorization, strengthened prime-signed uniqueness, and signed-admissible rigidity are marked proved; two-to-prime and prime-propagation calibrations are refuted; coherent prime orientation and two-prime branch control lemmas are wired in; mixed prime-pair witnesses are reduced to absurdity under branch uniformity; reciprocal/identity globalization and trace-connectedness implications close the remaining ledger rows. No new analytic argument appears here; the work is composition and naming of the repaired ledger.
why it matters
This is the single composition point for the PRC universal foundation stack. Downstream, prc_universal_foundation reads the kernel and promoted real-field fields (and the rest of the stack) off this certificate to inhabit the unconditional-looking universal foundation certificate surface.
In the Recognition framework it sits under the inevitability claim: any zero-parameter alternative that derives observables must match RS cost and selection or violate a necessity gate. The native-cost ledger is the concrete bookkeeping for T5-style J-uniqueness under admissible characters, recording which calibration and prime-orientation strengthenings survive and which overclaims are refuted. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live on the forcing chain. Its role is to make the foundation composition and the repaired native-cost status citable as one object rather than a scatter of module-local theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.