PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_iff_nonunit_identity_comparable_trace
plain-language theorem explainer
Prime-calibration forcing of identity orientation on comparable finite δ-orbit traces is equivalent whether stated for all prime directions or only for nonunit directions. Anyone chaining native-cost uniqueness targets through the identity-branch transport ladder cites this bridge. The proof is a pure Iff constructor from the two one-direction implications already proved in-module.
Claim. The following are equivalent: (i) every ratio character that is prime-direction calibrated has identity orientation respecting comparability of finite $\delta$-orbit traces on prime directions; (ii) every such character has identity orientation respecting that comparability on nonunit directions.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding multiplicative recognition data. Prime-direction calibration means $\chi$ is fixed to a preferred orientation on prime orbit directions. The native-cost uniqueness program then asks whether that calibration forces identity orientation to respect order comparisons among finite $\delta$-orbit traces (partial sums of the doubled-trace cost along orbit steps).
Two target propositions package that demand. The prime-identity target requires the respect property on every prime direction. The nonunit-identity target requires it only on nonunit directions (orbits not at the unit class). Both sit inside the same module that builds native cost from characters and doubled traces, and both feed the uniqueness-blocker certificate stack.
Upstream, each direction of the equivalence is already a short theorem: the prime target implies the nonunit target by restriction, and the nonunit target implies the prime target by a dedicated transport lemma that lifts nonunit identity-comparable-trace respect back to the prime case.
proof idea
Term-mode Iff introduction. The forward arrow is the already-proved implication from the prime-identity comparable-trace target to the nonunit-identity target (restriction plus the nonunit-of-prime lemma). The reverse arrow is the already-proved implication from the nonunit target back to the prime target (apply the nonunit hypothesis at a character and invoke the prime-of-nonunit transport lemma). No new calculus is done here; the declaration only packages the two arrows as a single equivalence.
why it matters
This equivalence is the first link in a short transport chain that rewrites the prime-identity comparable-trace target as the prime-floor successor-transport target. The immediate parent theorem composes this iff with the nonunit-to-floor-successor equivalence, so later uniqueness certificates can quote whichever formulation is convenient.
Downstream it appears in the native-cost uniqueness blocker certificate and in the conditional universal-foundation certificate, both of which assemble proved PRC targets into a single structured witness. In the broader Recognition Science forcing picture, these targets constrain how prime calibration pins identity orientation on the cost side before J-uniqueness and the self-similar fixed point $\phi$ are invoked; they are bookkeeping lemmas on the character/trace layer, not the T5–T8 geometric steps themselves.
The declaration closes no open sorry; it only collapses two already-proved formulations so the uniqueness ladder can move freely between prime and nonunit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.