PRCCharacterNonunitOrbitAllReciprocal_of_all_prime_reciprocal
plain-language theorem explainer
If a ratio character is multiplicative, product-display compatible, and reciprocal on every prime orbit direction, then it is reciprocal on every nonunit orbit direction. Cost-uniqueness arguments cite this to globalize prime-local reciprocal orientation before identity-witness reflection. The proof is strong induction on the natural size of the distinction, reducing composites via factorization and a product-reciprocal lemma.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal under cross-equivalence) that is compatible with native display of orbit products. Suppose that for every prime distinction $p$, $\chi$ sends the prime direction of $p$ to the reciprocal of that direction (cross-equivalence). Then for every nonzero nonunit distinction $p$, $\chi$ sends the orbit direction of $p$ to the reciprocal of that direction.
background
In the Primitive Recognition Calculus, costs factor through ratio-orbit characters. A PRCRatioCharacter is a map $\chi$ on ratio orbits that fixes the unit orbit, is multiplicative, and intertwines reciprocal, all up to cross-equivalence (the internal rational equality via balanced signed orbits), so the interface stays quotient-native.
Orbit directions package nonzero distinctions as ratio-orbit displays. Reciprocal orientation on a direction means $\chi$ of that display is cross-equivalent to its reciprocal. Product-display compatibility is the extra quotient-respect step: $\chi$ on the product orbit agrees with $\chi$ on the ratio product of the factor orbits; it is not automatic from bare multiplicativity under cross-equivalence.
The local setting is native cost uniqueness: one wants to force the character branch of a PRC cost. Arithmetic is recovered from logic naturals via toNat, with multiplication agreeing under that map, so induction on ordinary Nat size controls factorization of distinctions.
proof idea
Fix $\chi$ with the three hypotheses. Define a predicate $P(n)$: every distinction of size $n$ that is nonzero and nonunit has reciprocal orientation under $\chi$. Strong-induct on $n$.
For $q$ of size $n$, case-split on primality. If $q$ is prime, the prime-reciprocal hypothesis applies directly (after unfolding the direction definitions).
If not prime, nontrivial factorization $q = a\cdot b$ exists (else $q$ would be prime). Both factors are nonzero nonunits, so their toNat values are strictly between $1$ and $n$ (using toNat_mul, positivity, and mul_lt_mul). Induction gives reciprocal orientation on $a$ and on $b$. The product-reciprocal lemma for characters then glues them to reciprocal orientation on $q$.
Instantiate at $n = p.\mathrm{toNat}$.
why it matters
This is the globalization step from prime-local reciprocal orientation to all nonunit directions. Downstream, mixed and pure nonunit identity-witness reflection lemmas consume it (or the same pattern) once prime-local orientation is fixed, and the positive-orbit reciprocal theorem extends the same idea under cross-equivalence respect. The native-cost uniqueness blocker certificate sits at the end of that chain.
In the Recognition framework this supports uniqueness of the native cost character before J-cost identification (T5: $J(x)=(x+x^{-1})/2-1$). Reciprocal orientation is the character-level shadow of the $x\leftrightarrow x^{-1}$ symmetry in the Recognition Composition Law. Without lifting primes to composites, factorization of costs along the phi-ladder cannot be forced uniquely.
No open scaffold here: the claim is fully proved. It closes the inductive gap between prime calibration and full nonunit reciprocal display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.