PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_refuted
plain-language theorem explainer
Prime calibration does not force identity orientation to stay invariant along native prime-axis trace connections. Anyone auditing native-cost uniqueness blockers or the two-prime identity chain cites this negative result. The proof is a one-line reduction: the transport target is equivalent to a coherence target already shown false.
Claim. It is false that every ratio-orbit character $\chi$ that is prime-direction calibrated has identity orientation respecting connectivity of the native prime-axis trace graph. In other words, prime calibration alone does not force identity-orientation invariance along those trace connections.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits encoding how multiplicative structure is read. Prime-direction calibration constrains that character along the prime axis. The trace graph on that axis is already known to be structurally connected; the open question was whether calibration upgrades connectivity into identity-orientation invariance along trace links.
The transport target asserts exactly that upgrade: for every ratio character, prime calibration implies identity respects prime-axis trace connectivity. A sharper coherence form of the same demand is equivalent to this transport form (proved as an iff in-module). The local module is building a uniqueness story for the native cost by systematically proving or refuting candidate forcing targets.
proof idea
Assume the transport target. Apply the right-to-left direction of the in-module equivalence between the coherence target and the transport target to obtain the coherence target. Discharge the assumption by the already-proved refutation of the coherence target (itself reduced earlier to a branch-uniformity refutation). Pure term-mode chaining; no new analytic work.
why it matters
This closes one link in the negative half of the native-cost uniqueness ledger: a natural "prime calibration forces identity along traces" hope fails. Downstream, the two-prime identity trace-connected target is refuted by reducing to this statement. The result is also wired into the native-cost uniqueness blocker certificate and, via that ledger, into the conditional universal-foundation certificate. In the broader RS forcing picture it is a local obstruction, not a hit on T5 J-uniqueness or the RCL; it narrows which calibration hypotheses can still pin the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.