PRCUniversalFoundationOpenTargets
plain-language theorem explainer
A Prop-valued ledger of native-cost and prime-orientation targets for the Primitive Recognition Calculus universal-foundation layer. Positive fields name repaired interfaces that hold; negated fields record exact refutations of routes that cannot force the final surface. Cited by the conditional and final universal-foundation certificates when they expose the repaired/refuted cost ledger by name. Definitional structure only: no proof body.
Claim. The open-target ledger is the proposition whose fields are: (i) uniqueness and factorization statements for zero-calibrated native cost (some asserted, some refuted); (ii) prime-orientation coherence, two-prime branch control, identity/reciprocal forcing, and mixed-witness exclusion for characters on ratio orbits; (iii) a large family of equivalences and one-way implications among prime-floor calibration targets (trace coherence, branch uniformity, successor transport, nonunit orientation); (iv) refutations of unsigned or over-strong calibration routes; (v) the external-foundation parsing schema identity. Holding the ledger means every named repaired interface and every named refutation is available as a hypothesis package.
background
Primitive Recognition Calculus (PRC) builds recognition from distinction data, ratio orbits, and a native cost tied to the J-functional $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness). Characters $\chi$ act on ratio orbits; prime-local orientation, identity vs reciprocal branches, and two-prime control are the combinatorial levers that try to force global calibration of that cost.
This module sits at the universal-foundation layer: kernel first-pass, real complete ordered field, trace logic, and formal-system certificates compose into a top-level PRC foundation claim. Upstream, cost appears as summed ratio weights, as derived cost of a multiplicative recognizer, and as $J$-cost of a recognition event. Formal systems supply tokens/expressions so external foundations can be parsed expressively before inevitability applies.
The doc-comment frames the structure as a historical target ledger for the conditional certificate: positive entries are repaired proved interfaces; negative entries are exact refutations of dead routes.
proof idea
No proof: the declaration is a structure (definitional Prop bundle). Each field is a named hypothesis interface imported from the native-cost uniqueness and prime-calibration development (zero-calibrated uniqueness/factorization, signed admissible rigidity, prime-orientation coherence, mixed-witness characters, two-adic axis-twist failures, external parsing schema). Instantiating the structure means supplying proofs or refutations for every field; the structure itself only packages those obligations.
why it matters
The conditional and final universal-foundation certificates both depend on this ledger. Downstream, the final certificate closes the top-level theorem by carrying built PRC surfaces together with the exact native-cost ledger: repaired signed/prime/zero-calibrated uniqueness proved, weaker unsigned routes recorded as refuted. The conditional certificate exposes the same repaired/refuted ledger by name while composing kernel, real-field, trace-logic, and formal-system surfaces.
In framework terms this is bookkeeping for T5-style J-uniqueness inside PRC: which calibration paths actually force the native cost, and which over-claims (two-to-prime forcing, unsigned character rigidity, global orientation from prime calibration alone) are dead. It does not itself force $\phi$, eight-tick structure, or $D=3$; it stabilizes the cost-uniqueness side of the foundation stack so those later forcings sit on a clean ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.