PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget
plain-language theorem explainer
Names the open target that prime-direction calibration of a ratio character should force identity orientation at the orbit-2 prime axis to transport along any finite δ-trace link to a native prime axis. Native-cost uniqueness work cites it as the identity-side twin of reciprocal trace transport (Pass 81). The body is a pure Prop abbreviation, not a proved implication; downstream it is shown equivalent to the prime-identity trace-transport target and then refuted.
Claim. The two-prime identity trace-connected target asserts: for every map $\chi$ on rational orbits that is a ratio character and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every native prime orbit), identity orientation at the orbit-$2$ prime axis transports along any finite $\delta$-trace connection from that axis to an arbitrary native prime axis $p$.
background
In the Primitive Recognition Calculus, costs are studied through ratio characters: maps $\chi$ on RatioOrbit (signed numerator over nonzero orbit denominator) that fix the unit and are multiplicative up to cross-equivalence. Cross-equivalence is the quotient-native equality on orbits, so characters stay well-defined on the display rather than on raw integers.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every native prime orbit direction. Separately, the two-prime identity trace-connected property says: if the orbit-$2$ prime axis is $\delta$-trace-connected to a target native prime $p$, and $\chi$ fixes the orbit-$2$ prime direction up to cross-equivalence, then $\chi$ also fixes the prime direction of $p$.
This module packages native-cost uniqueness blockers as exact Lean targets. The present definition is the universal quantification that calibration should force the identity trace-connected property for every such character.
proof idea
Definitional Prop, not a proved theorem. The body is the single quantified implication: every ratio character that is prime-direction calibrated satisfies the two-prime identity trace-connected transport property. No tactics or lemmas are applied; downstream theorems treat the name as a hypothesis or as a goal to refute.
why it matters
Pass 81 isolates this as the identity-orientation twin of reciprocal trace transport, related by reciprocal twist. It sits inside the native-cost uniqueness blocker certificate, which records that uniqueness is not closed and splits the missing mathematics into exact targets.
Downstream, the target is proved equivalent to the prime-identity trace-transport target, and both directions of the equivalence are available as one-line wrappers. A further theorem derives it from the reciprocal two-prime trace-connected target. Critically, the target is refuted: the corresponding _refuted theorem reduces negation to the already-refuted prime-identity trace-transport target via the equivalence. That closes this branch of the uniqueness program and forces the search for a different factorization or calibration route toward T5-style $J$-uniqueness at the PRC layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.