PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_successor_step
plain-language theorem explainer
If prime calibration forces identity orientation to stay fixed under one successor step on every nonzero orbit, then it also forces identity orientation to respect comparability of finite δ-orbit traces. Native-cost uniqueness work cites this as the bridge from the one-step successor target to the sharper trace-order target. The proof is a one-line pointwise application of the character-level successor-to-trace lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has identity orientation invariant under one successor step on every nonzero orbit direction. Then every such $\chi$ has identity orientation that respects comparability of finite $\delta$-orbit traces.
background
In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode multiplicative structure on orbit directions. Prime-direction calibration pins how $\chi$ acts on prime generators. Two sharper targets package what calibration should force about identity orientation.
The successor target asserts that identity orientation is invariant under one successor step on every nonzero orbit direction. The comparable-trace target asserts that identity orientation respects comparability of finite $\delta$-orbit traces (the additive-trace side missing from purely multiplicative character laws).
Upstream, the character-level lemma already shows that any single character whose identity respects successor steps automatically respects comparable traces. This declaration lifts that implication to the quantified calibration targets.
proof idea
Term-mode, four lines. Introduce a ratio character $\chi$ together with the character and prime-calibration hypotheses. Apply the assumed successor-target hypothesis at $(\chi, h\chi, h\mathrm{prime})$ to obtain that $\chi$ respects successor identity. Feed that fact into the upstream character lemma PRCCharacterPrimeIdentityRespectsComparableTrace_of_successor_step, which returns that $\chi$ respects comparable traces. Discharge the goal.
why it matters
This is the target-level reduction used to refute the successor identity target. Downstream, PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_refuted assumes the successor target, applies this implication, and contradicts the already-refuted comparable-trace target. That refutation feeds the native-cost uniqueness blocker certificate, which records which factorization and calibration targets are proved versus refuted in the PRC native-cost uniqueness program.
In the broader Recognition Science forcing picture, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward a unique cost functional on ratio orbits. Closing or blocking these calibration targets decides how much of the cost law is forced by prime calibration alone versus needing extra additive-trace structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.