PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_iff_trace_transport
plain-language theorem explainer
Equivalence of two remaining native-cost obligations: full identity-orientation coherence across prime axes is the same as identity-orientation transport along already-proved prime-axis trace connections. Anyone collapsing or refuting the prime-calibration uniqueness blockers cites this. The proof is the pair of the two one-direction implications already established in-module.
Claim. The following are equivalent: (i) every ratio character that is prime-direction calibrated has identity orientation coherent across all prime axes; (ii) every such character has identity orientation invariant along native prime-axis trace connections.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws of the native cost. Prime-direction calibration means $\chi$ is fixed on the distinguished identity orientation of each native prime axis. Two residual targets remain for uniqueness of the native cost under that calibration.
The coherence target asks that identity orientation propagate across all prime axes once calibration holds. The transport target asks only that identity orientation be invariant along edges of the prime-axis trace graph. Structural connectivity of that graph is already proved, so transport is the smaller obligation: if identity is preserved along connections, coherence on the whole connected component follows.
Both targets are pure Prop interfaces in this module; the present result identifies them.
proof idea
Term-mode Iff introduction. The forward direction applies PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_trace_coherence, which reduces transport to the coherence hypothesis via the lemma that trace-connected identity respect follows from full coherence. The reverse applies PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_trace_transport, which, given transport, feeds the already-proved prime-axis trace-connectedness witness into the transport hypothesis to recover coherence on every prime pair. No new arithmetic is done here.
why it matters
This equivalence is the hinge that lets the module refute either residual target by refuting the other. Downstream, PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_refuted converts a transport assumption into coherence via the mpr direction and then invokes the coherence refutation. The same identification feeds prc_native_cost_uniqueness_blocker_certificate and the conditional universal-foundation certificate, which package which uniqueness obligations are closed versus still open.
In the Recognition forcing chain this sits inside the native-cost uniqueness program that pins the J-cost (T5) as the unique calibrated cost on ratio orbits. Collapsing coherence with transport removes a duplicate blocker without enlarging the hypothesis surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.