PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_nonunit_identity_comparable_trace
plain-language theorem explainer
Prime calibration plus the nonunit identity-branch comparable-trace target already yields the sharper prime-identity comparable-trace target. Cited by anyone equating the two targets or assembling the native-cost uniqueness blocker and universal-foundation certificates. Proof specializes the hypothesis at a calibrated ratio character and applies the character-level nonunit-to-prime transport lemma.
Claim. Assume that whenever a map $\chi$ on ratio orbits is a ratio character and is prime-direction calibrated, its identity orientation respects comparability of finite $\delta$-orbit traces on nonunit directions. Then the same hypotheses force identity orientation to respect comparability of finite $\delta$-orbit traces on prime directions.
background
Primitive Recognition Calculus studies ratio characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ as candidate cost orientations. Prime-direction calibration pins $\chi$ on prime generators. Native-cost uniqueness asks when such calibrated characters must reproduce the doubled-trace native cost built from the $J$-cost.
Two Prop targets package the desired trace-order conclusion at different strengths. The nonunit target requires identity orientation to respect comparability of finite $\delta$-orbit traces along nonunit directions. The prime-identity target asks the same along prime directions (the sharper one-step form). Upstream, at character level, nonunit identity respect already implies prime identity respect by restricting quantifiers: the lemma specializes the nonunit statement to primes.
proof idea
Short specialization proof. Introduce a ratio character $\chi$ that is prime-direction calibrated. Apply the assumed nonunit target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain nonunit identity comparable-trace respect for $\chi$. Feed that fact to the character-level lemma that nonunit identity respect implies prime identity respect (by restricting the nonunit quantifiers to the prime case). The conclusion is exactly the prime-identity target at $\chi$.
why it matters
Supplies one direction of the equivalence between the nonunit and prime-identity comparable-trace targets under prime calibration. That equivalence is consumed by the native-cost uniqueness blocker certificate and, via the certificate stack, by the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing chain, native-cost uniqueness is the bridge from $J$-uniqueness (T5) and the Recognition Composition Law to a unique cost on ratio orbits. Closing these trace-order targets removes a named blocker on that path; the present implication shows the sharper prime form is no stronger than the nonunit form once prime calibration is assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.