PRCNativeCostCharacterFactorizationTarget_of_admissible_character_factorization
plain-language theorem explainer
If every PRC-native cost factors through an admissible ratio character, then it also factors through an ordinary ratio character. Anyone tracking the discrete d'Alembert factorization blocker for native RCL costs would cite this. The proof is a one-line projection: drop the extra admissibility data and keep the underlying ratio character and the cross-equality.
Claim. Assume that every map $F$ on ratio orbits satisfying the PRC-native cost hypotheses factors through some admissible ratio character $\chi$ via the character cost, up to cross-equality on orbits. Then every such $F$ also factors through some (ordinary) ratio character with the same cross-equality.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying a discrete Recognition Composition Law package (the PRC-native cost hypotheses). The first exact factorization blocker asks that every such $F$ equal, up to orbit cross-equality, the cost built from a ratio character $\chi$.
That blocker is the discrete d'Alembert step: costs should arise as $q \mapsto \mathrm{costFromCharacter}(\chi,q)$ for a ratio character $\chi$. A repaired, stronger interface replaces ordinary ratio characters by admissible ones (characters satisfying the fixed interface rather than an arbitrary ratio character).
The admissible target therefore asserts existence of an admissible character factor; the original target asserts existence of any ratio-character factor. This lemma records that the stronger target implies the weaker one.
proof idea
Term-style unpacking of the universal quantifiers. Fix $F$ and the native-cost hypotheses. Apply the admissible factorization hypothesis to obtain $\chi$ together with admissibility and the cross-equality $F(q)\sim\mathrm{costFromCharacter}(\chi,q)$. Project admissibility to its underlying ratio-character field, and return that character with the same cross-equality. No further algebraic work.
why it matters
Inside PRC native-cost uniqueness, character factorization is the first exact blocker on the path from native RCL costs to the unique $J$-cost shape forced by T5 ($J(x)=(x+x^{-1})/2-1$). The admissible interface is the repaired stand-in for that blocker; this lemma shows the repair still discharges the original factorization target.
No downstream consumers are wired yet (used_by is empty), so the lemma currently closes a local implication in the uniqueness module rather than feeding a named parent theorem. It keeps the discrete d'Alembert factorization step aligned with the Recognition Composition Law while the admissible-character repair is in force. Once the admissible target is proved, this implication immediately yields the classical factorization target used elsewhere in the uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.