PRCPrimeCalibrationPropagationTarget
plain-language theorem explainer
Once a ratio character is calibrated on every prime direction, its generated cost must agree with canonical J-cost on every rational orbit. This packages the unique-factorization half of native cost rigidity as a named Prop target. Uniqueness and rigidity assembly theorems cite it as a hypothesis. Pure definition: no proof obligations inside the declaration.
Claim. For every map $\chi$ from rational orbits to rational orbits that is a ratio character and is calibrated on every prime direction, and for every rational orbit $q$, the character-generated cost of $q$ is cross-equivalent (by balanced cross-multiplication of numerator and denominator orbits) to the canonical rational $J$-cost $J(q)=((q+q^{-1})/2)-1$.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-orbit denominator. Two such orbits are identified by cross-equivalence: the signed products of numerator with the other denominator balance. The native rational $J$-cost on an orbit $q$ is the ratio-orbit object $J(q)=((q+q^{-1})/2)-1$, not yet the real-analytic uniqueness theorem.
A ratio character is a multiplicative, unit-preserving map on rational orbits, stated with cross-equivalence so it stays quotient-native. Cost generated from a character is simply $J$ applied after the character. Prime-direction calibration means that generated cost already matches canonical $J$ on every native prime orbit.
This module isolates native cost uniqueness into exact Lean targets. The present definition is the sharper target B on the unique-factorization side: calibration on primes should force agreement on all rationals.
proof idea
Definitional packaging only. The body is the universal Prop that every ratio character calibrated on all prime directions has character-generated cost cross-equivalent to canonical $J$ at every rational orbit. No tactics, no lemmas applied, no sorry.
why it matters
This is the unique-factorization leg of character rigidity for native PRC cost, the discrete counterpart of T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$). Downstream, admissible-character rigidity is obtained by feeding this target into the admissible wrapper; full character rigidity is the conjunction of two-calibration-forces-prime-calibration with this propagation target; native cost uniqueness assembles from factorization plus this propagation (with or without the two-calibration bridge). The Pass-25 blocker certificate and Pass-26 sharpened rigidity target both name it explicitly, so closing this Prop is on the critical path to discharging native cost uniqueness without analytic bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.