PRCNativeCostFactorizationAdmissibilityUpgradeTarget
plain-language theorem explainer
Names the factorization-side upgrade target: every ratio-character factor of a native cost must be replaceable by an admissible character that generates the same cost. Uniqueness arguments cite it when reducing raw character factorization to the admissible case. The body is a pure Prop (universal over native costs and characters); no proof content. Downstream work has since refuted the target via two-adic axis twists.
Claim. For every map $F$ on ratio orbits obeying the native-cost hypotheses, and every ratio character $\chi$ such that $F(q)$ is cross-equal to the cost generated by $\chi$ at every orbit $q$, there exists an admissible ratio character $\psi$ whose generated cost is cross-equal to $F$ on all orbits.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits satisfying a fixed structural package (symmetry, normalization, and the orbit form of the Recognition Composition Law). A ratio character $\chi$ is a multiplicative map on those orbits; the cost generated by $\chi$ is the composition of $\chi$ with the canonical $J$-cost $J(x)=(x+x^{-1})/2-1$ forced at T5. Cross-equality on ratio orbits identifies values that agree after the orbit quotient, so $J$ cannot see orientation: $\chi$ and its reciprocal yield the same cost.
The module aims at uniqueness of native costs against the canonical $J$-ladder. Factorization says every native cost arises as cost-from-character for some $\chi$. Admissibility is a stricter filter (characters that survive calibration and prime-propagation). This definition isolates the upgrade step between those layers.
The doc-comment states the intent directly: an arbitrary ratio-character factor must be replaceable by an admissible factor with the same generated cost, weaker than demanding the original factor itself be admissible, "because $J(\chi q)$ cannot distinguish a direction from its reciprocal."
proof idea
Definitional packing only. The declaration is a Prop abbreviation, not a proved statement: it quantifies over native-cost maps $F$ and ratio characters $\chi$, assumes pointwise cross-equality of $F$ with the character-generated cost, and asserts existence of an admissible character $\psi$ with the same generated cost. No tactics or upstream lemmas fire here. Downstream results either assume this Prop as a hypothesis in a composition lemma or discharge it by refutation.
why it matters
This target sits on the native-cost uniqueness spine. Assumed together with character factorization, it yields the admissible-factorization target; with prime-calibration propagation added, it feeds the full native-cost uniqueness target. The intended bridge is from raw factorization to the admissible layer that uniqueness actually needs.
Framework landmarks are T5 $J$-uniqueness and the Recognition Composition Law: costs live on the $J$-image, so character orientation is free and the upgrade (replace factor, do not rigidify it) is the natural statement.
The upgrade as stated is false. A constructed two-adic axis-twist cost satisfies the native hypotheses yet admits no admissible replacement character, and the module records an explicit refutation of this Prop. Uniqueness arguments must therefore route around a blanket upgrade and treat twist pathologies separately rather than absorb them into admissibility replacement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.