PRCNativeCostAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
Names the admissible character-factorization obligation for native costs: every native cost on ratio orbits must equal the cost generated by some admissible ratio character. Uniqueness arguments in the primitive recognition calculus cite this target as the repaired factorization half of the uniqueness package. Pure Prop definition; no proof content.
Claim. Every map $F$ from ratio orbits to ratio orbits that satisfies the native-cost hypotheses admits some character $\chi$ on ratio orbits such that $\chi$ is an admissible ratio character and, for every orbit $q$, $F(q)$ is cross-equal to the cost generated from $\chi$ at $q$.
background
In the primitive recognition calculus, a native cost is a map $F$ on ratio orbits obeying a fixed package of structural hypotheses (reciprocity, composition, and the doubled-trace/d'Alembert constraints that force the classical $J$-shape). Costs are compared up to crossEq, the orbit-level identification that equates a direction with its reciprocal, matching the fact that $J(\chi q)$ cannot tell $\chi$ from $\chi^{-1}$.
A ratio character is a multiplicative map on orbits; costFromCharacter rebuilds a cost functional from such a character. The weaker factorization target only asks for some ratio character. The admissible variant strengthens the demand: the factor must satisfy the repaired admissibility interface (PRCAdmissibleRatioCharacter), not an arbitrary character.
The reciprocal automorphism on positive ratios and the ledger reciprocal event (source/target swap with inverse ratio) are the algebraic reason admissibility is stated up to direction: native cost is insensitive to that flip.
proof idea
Definitional Prop, not a proved theorem. The body is a single universal-existential statement: for every $F$ meeting the native-cost hypotheses, there exists an admissible character $\chi$ whose generated cost is cross-equal to $F$ at every orbit. No tactics, no lemmas applied; downstream theorems discharge or consume this Prop as a named target.
why it matters
This is the repaired factorization half of native-cost uniqueness. Combined with admissible-character rigidity it yields the full uniqueness target (PRCNativeCostUniquenessTarget_of_admissible_character_targets). It is strictly stronger than bare character factorization, and the bare target is recovered from it by forgetting admissibility (PRCNativeCostCharacterFactorizationTarget_of_admissible_character_factorization).
An upgrade lemma is still missing on the factorization side: arbitrary character factors of native costs should be replaceable by admissible ones with the same generated cost. That upgrade plus bare factorization implies this target. In the broader RS chain this sits under T5 $J$-uniqueness: native costs must factor through the unique admissible character shape forced by the Recognition Composition Law, not through an unconstrained multiplicative map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.