PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget
plain-language theorem explainer
Names the open target that prime-direction calibration of a ratio character forces identity orientation to respect comparability of finite δ-orbit traces on prime axes. Native-cost uniqueness work cites it as the exact trace-order obligation. The body is a pure Prop abbreviation packing three named hypotheses into one universal claim.
Claim. For every map $\chi$ on 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 induced cost matches canonical $J$-cost on each prime orbit), then identity orientation under $\chi$ transports between any two prime axes whose finite $\delta$-orbit traces are comparable by extension.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: integer numerators over nonzero orbit denominators. A ratio character $\chi$ is a candidate d'Alembert factor at that level: it fixes the unit orbit and is multiplicative up to cross-equivalence, so the construction stays quotient-native rather than demanding definitional equality.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. The identity event is the $J$-cost minimum at state $1$. The conclusion property is the exact trace-order law: when two prime orbit-position traces are comparable by one-step $\delta$-extension, identity orientation must transport between those prime axes. Structural comparability of orbit traces is already available; what remains is that the character itself respect that order.
proof idea
No proof obligation: this is a definitional Prop packing. The body is the universal quantification over maps $\chi$ of the implication chain ratio-character plus prime-direction calibration implies prime-identity comparable-trace respect. Downstream theorems treat the name as a single hypothesis and discharge or transport it via one-line wrappers (e.g. reducing to the nonunit-identity or common-trace-extension forms).
why it matters
This is a named blocker target inside native cost uniqueness. The Pass-25 certificate structure records that uniqueness is not closed and splits the missing mathematics into exact Lean targets; this declaration is the sharper trace-order piece of that split.
It feeds a web of equivalences and one-way implications in the same module: it implies the nonunit-identity comparable-trace target, the common-trace-extension target, and is equivalent (via those bridges) to the prime-floor successor-transport target. Closing it would discharge a concrete step toward forcing the unique native cost compatible with the Recognition Composition Law and $J$-uniqueness (T5), rather than leaving orientation free on comparable prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.