PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_prime_identity_comparable_trace
plain-language theorem explainer
If prime calibration already forces identity orientation to respect comparability of finite δ-orbit traces on prime directions, the same holds on every nonunit direction. Native-cost uniqueness and the universal-foundation certificate cite this implication. The proof is a short term application of a character-level reduction, feeding two already-proved calibration targets as side hypotheses.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has identity orientation respecting comparability of finite $\delta$-orbit traces on prime directions. Then every such $\chi$ also has identity orientation respecting comparability of finite $\delta$-orbit traces on all nonunit directions.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how recognition orients multiplicative directions. Prime-direction calibration constrains $\chi$ on prime generators. Finite $\delta$-orbit traces are the discrete path sums used to compare orientations; "comparable trace" means identity orientation preserves the order relation among those traces.
Two Prop-targets sit in this module. The prime-identity target asks that calibrated characters respect trace comparability on prime directions. The nonunit-identity target asks the same on every nonunit direction (a strictly larger class). The character-level bridge lemma states that if $\chi$ is orbit-product display compatible, has local prime orientation, and already respects prime-identity comparable traces, then it respects nonunit-identity comparable traces.
Orbit-product display compatibility and local prime orientation are already discharged unconditionally for prime-calibrated characters in this module.
proof idea
Term-mode proof. Introduce a calibrated ratio character $\chi$. Apply the character-level bridge lemma, supplying four ingredients: the character hypothesis; the already-proved orbit-product display compatibility target at $\chi$; the already-proved local prime-orientation target at $\chi$; and the assumed prime-identity comparable-trace target evaluated at $\chi$. No further case split is needed.
why it matters
This is one direction of the equivalence between the prime-identity and nonunit-identity comparable-trace targets under prime calibration. That equivalence collapses two successive sharpenings of the identity-branch transport story into a single Prop, which the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both consume.
In the Recognition forcing chain, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward a unique cost functional on ratio orbits. Closing the nonunit trace-order target from the prime one removes a residual gap between local prime data and global nonunit identity transport, tightening the path to a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.