PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget
plain-language theorem explainer
Defines the open target that every ratio character calibrated on prime directions must keep identity orientation under one successor step on every nonzero orbit. Native-cost uniqueness work cites it as a sharper one-step forcing claim between prime calibration and additive-trace compatibility. The body is a pure Prop abbreviation packing three named hypotheses into a single universal statement; downstream it is both implied by a transport target and outright refuted.
Claim. For every map $\chi$ from rational orbits to rational orbits: if $\chi$ is a ratio character and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), then identity orientation of $\chi$ is invariant under one successor step on every nonzero $\delta$-orbit direction.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a structure-preserving self-map of these orbits. Prime-direction calibration means that the cost reconstructed from $\chi$ agrees, via cross-equality, with the canonical $J$-cost on every prime orbit direction.
The successor-step identity law is strictly smaller than prime-to-prime transport: it only asks that identity orientation of $\chi$ at a nonzero orbit $p$ be equivalent to the same orientation at $\mathrm{succ}(p)$. The module comment stresses that this isolates additive-trace compatibility missing from purely multiplicative ratio-character laws (cf. multiplicativity of $J$-automorphisms in CostAlgebra).
Local setting is native cost uniqueness: forcing the recognition cost from character data alone, without external calibration beyond primes.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification $\forall,\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{SuccessorIdentity}(\chi)$, with the three named predicates inlined by reference. No tactics or lemmas discharge anything here; discharge happens only at use sites (transport implication, or the global refutation).
why it matters
This target sits on the native-cost uniqueness forcing ladder. Downstream, transport implies it (..._of_transport), and it implies the comparable-trace prime-identity target (..._of_successor_step). Both feed PRCNativeCostUniquenessBlockerCertificate, which records that uniqueness is not closed and splits the gap into exact Lean targets.
Crucially, the target is refuted: PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_refuted shows no such forcing holds in general. That negative result is carried into PRCUniversalFoundationOpenTargets as part of the historical ledger of routes that cannot force the final surface. In framework terms it separates multiplicative ratio-character structure (RCL / $J$-automorphisms) from the additive one-step trace law needed for full native uniqueness, clarifying why prime calibration alone does not close T5-style $J$-uniqueness at the PRC layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.