PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_canonical_add_trace
plain-language theorem explainer
If prime calibration forces identity orientation through the canonical finite common extension (orbit-position trace of p+r), then it also forces identity orientation along native prime-axis trace connections. Anyone tracking the native-cost uniqueness ladder or the two prime-identity targets cites this implication. The proof is a one-line unpacking that applies the pointwise canonical-to-connected transport lemma.
Claim. Assume that every ratio-orbit character $\chi$ that is a PRC ratio character and is prime-direction calibrated has identity orientation respecting the canonical additive finite common extension $\mathrm{orbitPositionTrace}(p+r)$. Then every such $\chi$ has identity orientation invariant along native prime-axis trace connections.
background
In the Primitive Recognition Calculus, ratio-orbit characters are maps $\chi$ on ratio orbits that encode orientation data for the native cost. Prime-direction calibration is the constraint that $\chi$ aligns with the preferred prime axis. Two nested targets package what that calibration should force for identity orientation.
The stronger target asks that identity orientation transport through the concrete finite common extension $\mathrm{orbitPositionTrace}(p+r)$ (canonical add-trace). The weaker target asks only that identity orientation be invariant along native prime-axis trace connections; structural connectivity of that prime-axis trace graph is already established upstream.
The pointwise bridge is already proved: if a single character respects canonical add-trace, then it respects trace-connectedness, via common finite $\delta$-trace extensions. This declaration lifts that bridge from characters to the quantified calibration targets.
proof idea
Term-style unpacking of the target propositions. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed canonical-add-trace target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain the pointwise canonical-add-trace respect property. Feed that into PRCCharacterPrimeIdentityRespectsTraceConnected_of_canonical_add_trace, which reduces canonical add-trace respect to common-trace-extension respect and thence to trace-connectedness. No extra arithmetic is done here.
why it matters
Closes one direction of the equivalence between the canonical-add-trace target and the smaller trace-transport target, so the two formulations of "prime calibration forces prime identity orientation" may be swapped freely in the uniqueness ladder. Downstream, that equivalence and this implication feed the native-cost uniqueness blocker certificate and, through the foundation stack, the conditional universal-foundation certificate.
In Recognition Science terms this sits inside the PRC native-cost uniqueness program that pins the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) as the unique admissible cost once orientation and trace data are calibrated. It does not itself force uniqueness of $J$; it only tightens the prime-identity transport interface that uniqueness proofs consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.