PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
plain-language theorem explainer
Packages the exact remaining cross-prime obligation: every ratio character that is multiplicative and calibrated on native prime directions must send identity orientation on one prime axis to identity orientation on every prime axis. Native-cost uniqueness work cites this Prop as the hub equivalent to no-mixed-orientation, no-mixed-witnesses, and branch-uniformity targets. The body is a pure universal Prop abbreviation, not a proof.
Claim. The target assertion is: for every map $\chi$ on ratio orbits, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its induced cost matches canonical $J$-cost on every native prime orbit), then $\chi$ is prime-identity trace-coherent: whenever $\chi$ fixes one prime direction on the identity branch, it fixes every prime direction on the identity branch.
background
In the Primitive Recognition Calculus, costs factor through ratio characters on RatioOrbit (signed numerator over a nonzero distinction-nat denominator). A ratio character $\chi$ is quotient-native: it preserves the unit orbit and multiplies up to cross-equivalence, the PRC stand-in for equality after canceling common factors.
Prime-direction calibration demands that the cost built from $\chi$ agrees with the canonical $J$-cost on every native prime orbit. Separately, prime-identity trace-coherence is the missing cross-prime law: identity orientation at one calibrated prime forces identity orientation at every calibrated prime. As the upstream doc states, "the current ratio-character laws are local to multiplication and reciprocal and do not by themselves connect the orientation choices of different prime axes."
The identity event sits at the $J$-cost minimum $x=1$. Traces are finite distinction sequences; the present target is the exact Prop that calibration should force identity orientation to propagate across the prime lattice.
proof idea
No proof: this is a def of a Prop. The body is the single universal statement
$\forall,\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PrimeDirectionCalibrated},\chi\to\mathrm{PrimeIdentityTraceCoherent},\chi$.
Downstream theorems treat the name as a black-box hypothesis or as one side of an equivalence with sibling targets (no-mixed orientation, branch uniformity).
why it matters
This is the exact remaining trace-coherence target named in the doc-comment: prime calibration must make identity orientation propagate across prime axes. It is the hub of the Pass-25 native-cost uniqueness blockers. Downstream, it is definitionally equivalent (via iff theorems) to the no-mixed-prime-orientation target, the no-mixed-prime-witnesses target, and the prime-identity branch-uniformity target; each of those is recovered from this Prop by a short intro/apply argument.
The blocker certificate records that native cost uniqueness is not closed, but the missing mathematics is split into exact Lean targets of this shape. Closing this Prop would discharge the cross-prime gap that local multiplicative character laws leave open, a necessary step toward uniqueness of the native cost that feeds the Recognition Composition Law and the T5 $J$-uniqueness landmark $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.