PRCNativeCostCharacterFactorizationTarget
plain-language theorem explainer
Every PRC-native cost on ratio orbits that obeys the discrete RCL hypotheses factors, up to cross-equivalence, through some multiplicative ratio character. Cost-classification and uniqueness arguments cite this as the discrete d'Alembert factorization target. The declaration is a pure Prop packaging that universal quantification; no proof is attached.
Claim. The following assertion holds: for every map $F$ from ratio orbits to ratio orbits satisfying the PRC-native cost hypotheses (reciprocity, normalization invariance, canonical RCL, and two-point calibration), there exists a ratio character $\chi$ (unit at $1$, multiplicative up to cross-equivalence) such that for every ratio orbit $q$, $F(q)$ is cross-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 is replaced by cross-equivalence: two orbits match when the cross-multiplied signed orbits balance. Costs are maps $F$ on this discrete rational surface.
The native cost hypotheses package the discrete Recognition Composition Law data: $F$ is reciprocal and normalization-invariant, obeys the canonical RCL identity, and is two-calibrated (ruling out the zero cost until an internal real completion exists). A ratio character $\chi$ is a multiplicative map with $\chi(1)\sim 1$ under cross-equivalence. The cost generated from a character is the orbit-level lift of $\chi$ (identity character recovers the canonical PRC cost).
This module isolates uniqueness of that native cost. The present definition names the first exact blocker: discrete d'Alembert factorization of every admissible native cost through some ratio character.
proof idea
No proof body: the declaration is a def equating a name to a universal Prop. The right-hand side quantifies over maps $F$, assumes the native cost hypotheses structure, and asserts existence of a ratio character $\chi$ such that $F(q)$ is cross-equivalent to costFromCharacter $\chi$ $q$ for every ratio orbit $q$. Downstream lemmas discharge or relate this Prop; the definition itself only packages the statement.
why it matters
This is the discrete d'Alembert factorization step for PRC-native RCL costs, the first exact blocker on the path to cost uniqueness inside Primitive Recognition Calculus. It sits upstream of the admissible-factorization target and is equivalent to the character-trace-lift target: several theorems convert between factorization, trace lift, doubled-trace coherent roots, and zero-calibrated doubled-trace hypotheses.
Parent results include the iff with the trace-lift target, the upgrade into the admissible character-factorization target, and constructors from doubled-trace coherent-root or zero-calibrated data. In the broader Recognition chain this is the discrete analogue of the continuous J-uniqueness step (T5): costs obeying the composition law must arise from characters, forcing the familiar $J(x)=(x+x^{-1})/2-1$ shape once the real completion is in place. Closing or refuting this Prop is the gate for native-cost classification on the ratio-orbit surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.