PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
plain-language theorem explainer
Defines the open target that prime-direction calibration of a ratio character forces identity-branch uniformity: if any native prime axis is identity-oriented under χ, every native prime axis is. Cited throughout the native-cost uniqueness blocker chain as the trace-free form of the prime-identity transport obstruction. Pure Prop abbreviation; no proof content.
Claim. The following proposition is the target: for every map $\chi$ on ratio orbits that is a ratio character (unit at $1$, multiplicative up to cross-equivalence) and whose induced cost agrees with canonical $J$-cost on every native prime direction, identity orientation is uniform across primes: if $\chi(p)\simeq p$ for any prime orbit $p$, then $\chi(r)\simeq r$ for every prime orbit $r$.
background
In the Primitive Recognition Calculus, costs on positive ratios are sought via d'Alembert factorization through a ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. A ratio character is quotient-native: it fixes the unit orbit and is multiplicative up to cross-equivalence (not definitional equality). The induced cost is compared to the canonical $J$-cost $J(x)=(x+x^{-1})/2-1$ on prime directions.
Prime-direction calibration says that for every native prime orbit $p$, the cost generated by $\chi$ at the prime direction agrees with $J$ on that orbit. Identity orientation of a prime axis means $\chi$ fixes that prime direction up to cross-equivalence. The identity event itself is the $J$-cost minimum at state $1$.
Branch uniformity is the trace-free content of the prime-identity transport blocker: one identity-oriented native prime axis forces every native prime axis onto the identity branch. Connectivity of the prime-axis trace graph is already established upstream; what remains is this uniformity statement under calibration.
proof idea
Definitional Prop packing only. The body is the universal quantification over ratio maps $\chi$, assuming the ratio-character axioms and prime-direction calibration, and concluding prime-identity branch uniformity. No tactics, no lemmas applied; downstream theorems treat this name as the hypothesis or as one side of an equivalence.
why it matters
This is the smaller, trace-free form of the prime-identity transport target inside native cost uniqueness. It feeds the Pass-25 blocker certificate PRCNativeCostUniquenessBlockerCertificate, which records that uniqueness is not closed but is split into exact Lean targets.
Downstream, assuming the target immediately yields no mixed prime orientation and rules out distinct prime-pair witness characters. It is also proved equivalent to several sibling targets: canonical additive trace transport, identity-forces-two, identity-iff-two, and the no-mixed-orientation / no-distinct-pair formulations. Closing any one of those equivalent forms discharges this branch of the uniqueness obstruction and advances the T5 J-uniqueness forcing chain at the PRC character level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.