PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget
plain-language theorem explainer
Names the global target that every prime-calibrated ratio character must globalize an identity witness from any prime axis to all nonunit orbit directions. Native-cost uniqueness work cites it as one exact Lean blocker for the prime-floor path. The body is a pure Prop abbreviation: quantify over characters, impose ratio-character and prime-calibration hypotheses, and demand the witness-globalization predicate.
Claim. The following proposition holds as a named target: for every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit), then $\chi$ globalizes prime identity witnesses to nonunits: whenever $\chi$ fixes any prime direction, it fixes every nonunit nonzero orbit direction.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: each orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). A ratio character $\chi$ is a candidate factor in a d'Alembert factorization of a PRC cost. It is stated at the orbit level with cross-equivalence rather than definitional equality, so it stays quotient-native: it fixes the unit orbit and is multiplicative under orbit multiplication.
Prime-direction calibration means that the cost reconstructed from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. The identity-witness globalization predicate then says: if any such calibrated prime axis is fixed by $\chi$ (cross-equal to itself), identity propagates to every nonunit nonzero orbit direction. The no-prime-identity case is handled separately by a prime-witness reflection lemma.
This module packages native-cost uniqueness into exact Prop targets rather than a single closed theorem. The present definition is the witness-globalized form of the prime-floor blocker.
proof idea
Definitional, not a proved theorem. The right-hand side is a single universal quantification: for all orbit maps $\chi$, assume the ratio-character structure and prime-direction calibration, then assert the already-named predicate that prime identity witnesses globalize to nonunits. No tactics, no lemmas applied at this site; downstream theorems treat the whole Prop as a hypothesis or as one side of an equivalence.
why it matters
Sits on the prime-floor branch of the native-cost uniqueness blocker split. Downstream it is equivalent to the no-mixed-prime-witnesses target and to the prime-floor successor-transport target; each direction is a short intro-and-apply theorem. The Pass-25 blocker certificate records that uniqueness is not closed and lists the missing mathematics as exact Lean targets; this name is one of those targets (and a sibling _refuted declaration appears in the same module).
In the broader Recognition chain, native $J$-cost uniqueness feeds T5 (uniqueness of $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Closing or refuting this globalization step decides whether prime-calibrated characters can still branch away from the canonical cost on composite nonunit directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.