PRCStrengthenedNativeCostAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
For every cost map on ratio orbits that obeys the strengthened native-cost package (ordinary native axioms plus cost-level prime-pair product calibration), some admissible ratio character generates that cost up to cross-multiplication equivalence. Uniqueness and factorization arguments in the PRC native-cost stack cite this Prop as the intermediate target. It is a pure interface definition, not a proved theorem.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the strengthened native-cost hypotheses (native RCL/normalization/calibration plus prime-pair product calibration at the cost level), then there exists a map $\chi$ on ratio orbits that is an admissible ratio character (ratio-character laws, prime-direction calibration, and prime-pair product cost consistency) such that for every ratio orbit $q$, $F(q)$ is cross-multiplication equivalent to the cost generated from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is internal cross-multiplication balance (crossEq): the scaled numerators match as signed orbits. Costs are maps $F$ on those orbits.
A character $\chi$ produces a cost by post-composing with the canonical on-orbit cost map; the identity character recovers the native cost. After a two-adic countermodel, admissibility was repaired: a character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product cost consistency, so global orientations survive while valuation twists are excluded.
The strengthened native-cost hypotheses keep the older RCL, normalization, and calibration fields and add prime-pair product calibration directly at the cost level. This definition packages the claim that every such strengthened $F$ factors through some admissible character up to cross-equivalence.
proof idea
No proof: the declaration is a def equating a name to a Prop. The body is the universal-existential statement above (strengthened hypotheses on $F$ imply existence of an admissible $\chi$ with pointwise crossEq to costFromCharacter). Downstream theorems inhabit or consume this Prop; they do not expand inside the definition itself.
why it matters
This is the strengthened factorization waypoint in the PRC native-cost uniqueness chain. After cost-level prime-pair calibration enters the hypotheses, factorization is required to land on an admissible character, not a bare ratio character. One parent theorem discharges the target from ordinary character factorization plus the two-calibration force that upgrades prime calibration. Another parent feeds the inhabited target, together with admissible-character rigidity, into the strengthened uniqueness target: any two strengthened native costs that factor admissibly and rigidly must agree.
In the broader Recognition stack this sits under native $J$-cost uniqueness (T5 / RCL lineage): costs on the rational orbit display must arise from calibrated characters so the unique cost shape is forced before continuum and physical constants are read off. It records the post-countermodel repair path rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.