PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
The target asserts that every zero-calibrated native cost on ratio orbits factors as the cost generated by some signed admissible ratio character. Cost-classification and uniqueness work cite it as the signed-admissible route from native hypotheses to character form. It is a bare Prop definition: a universal quantifier over native-cost maps F, zero-calibration of the doubled trace, and existence of χ matching F under cross-multiplication.
Claim. For every map $F$ from ratio orbits to ratio orbits that satisfies the native cost hypotheses (reciprocity, normalization invariance, canonical RCL, and two-calibration), if the doubled trace $T_F(q)=2(F(q)+1)$ is zero-calibrated ($T_F(0)\sim 0$ under cross-multiplication), then there exists a signed admissible ratio character $\chi$ such that $F(q)$ is cross-multiplication equivalent to the character-generated cost of $\chi$ at every ratio orbit $q$.
background
In the primitive recognition calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-multiplication when the scaled numerators balance as signed orbits; that internal relation is the PRC stand-in for rational equality.
A native cost $F$ is a self-map of ratio orbits obeying reciprocity $F(q)\sim F(q^{-1})$, invariance under denominator normalization, the canonical recognition composition law on the discrete rational surface, and a two-calibration that rules out the zero cost. From any such $F$ one forms the doubled d'Alembert trace $T_F(q)=2(F(q)+1)$. Zero-calibration of that trace demands $T_F(0)\sim 0$, the discrete analogue of fixing the character image at the zero orbit.
Costs generated from characters are the comparison class: costFromCharacter applies the on-orbit cost construction to $\chi(q)$, and for a genuine character the doubled trace recovers $\chi(q)+\chi(q)^{-1}$. The target asks whether every zero-calibrated native cost arises this way from a signed admissible character.
proof idea
Definitional packaging only: the declaration is a Prop abbreviation whose body is the quantified statement itself. No tactics or lemmas discharge anything. The constituents are assembled by name: native-cost hypotheses on $F$, zero-calibration of nativeCostDoubledTrace F, existence of a signed admissible ratio character $\chi$, and pointwise cross-equivalence of $F$ with costFromCharacter χ.
why it matters
This is the signed-admissible factorization route toward zero-calibrated native-cost uniqueness, the discrete PRC analogue of the continuous J-uniqueness step (T5) that forces $J(x)=(x+x^{-1})/2-1$ from the recognition composition law. Downstream, an implication theorem shows that if the target held then the full zero-calibrated uniqueness target would follow by transporting cross-equivalence through the character cost. In fact the target is refuted: the absolute-value-generated native cost satisfies the hypotheses and zero-calibration yet admits no signed admissible factor, so the negation is proved and recorded in the uniqueness blocker certificate and in the universal-foundation open-target ledger. The ledger keeps the (still open) unsigned character-factorization target separate from this refuted signed-admissible branch, splitting the missing mathematics into exact Lean interfaces rather than a single opaque gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.