PRCNativeCostUniquenessBlockerCertificate
plain-language theorem explainer
Pass-25 ledger for discrete native-cost uniqueness in the primitive recognition calculus. It records which factorization, rigidity, and uniqueness routes are proved, which older claims are refuted, and the exact remaining targets (zero-calibrated prime-signed strengthened uniqueness among them). Universal-foundation certificates cite it as the native-cost status block. Pure structure definition: no proof body.
Claim. A proposition that packages the status of native-cost uniqueness on ratio orbits: zero-calibrated factorization of admissible native costs through ratio characters holds; the signed-admissible zero-calibrated factorization, several older uniqueness and rigidity claims, and many prime-calibration propagation claims are refuted; a strengthened zero-calibrated prime-signed uniqueness target is retained; together with equivalences among orientation-coherence, reciprocal-twist, and trace-connected formulations, and with the identity and reciprocal maps as explicit ratio characters.
background
In the primitive recognition calculus, costs live on ratio orbits built from distinction naturals and traces. A ratio character is a multiplicative map on those orbits; the native cost built from a character is the discrete stand-in for the continuous $J$-cost that satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ (forcing-chain T5 uniqueness of $J$).
Native-cost hypotheses encode the discrete d'Alembert / doubled-trace axioms needed for that factorization. Zero-calibration fixes the doubled-trace root at the identity; signed-admissible characters add orientation and unit-calibration constraints. Trace extension (a finite distinction sequence is a prefix of another) and orbit directions supply the arithmetic backbone used to compare prime axes and successor steps.
This module sits after the continuous $J$-uniqueness story and asks the harder discrete question: which admissible native costs are forced to equal the canonical on-orbit cost. Pass-25 answers by splitting that question into named targets rather than a single closed theorem.
proof idea
No proof: the declaration is a structure ... : Prop whose fields are either named target propositions, explicit refutations $\neg$ target, tautological self-equalities that pin definitions, or quantified bridges (implications and iff chains) among orientation, reciprocal-twist, and trace-coherence predicates.
The inhabiting theorem prc_native_cost_uniqueness_blocker_certificate fills each field from previously proved or refuted lemmas (for example the zero-calibrated factorization proof and the signed-admissible factorization refutation). Several fields are pure bookkeeping equalities that lock a definition name to itself so downstream certificates can quote a stable ledger.
why it matters
Native-cost uniqueness is the discrete counterpart of T5 $J$-uniqueness inside the recognition calculus. Closing it would force every admissible PRC-native cost to the canonical on-orbit cost and feed the mass/yardstick ladder downstream. This certificate does not close that theorem; it freezes the exact gap after Pass-25.
Downstream, prc_native_cost_uniqueness_blocker_certificate inhabits the structure, and both PRCUniversalFoundationCertificate and the conditional universal-foundation certificate import the ledger: the repaired signed/prime/zero-calibrated uniqueness route is the live path, while weaker unsigned routes are recorded as refuted. The doc-comment states the intent directly: uniqueness is not closed, but the missing mathematics is split into exact Lean targets.
Framework role: keeps the foundation audit honest. Strength tag deltaOnly marks that only incremental (not full) uniqueness strength is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.