PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_prime_floor_successor_transport
plain-language theorem explainer
Prime calibration that forces identity successor transport above the self-reciprocal unit floor also forces identity orientation to respect comparability of finite δ-orbit traces. Native-cost uniqueness and prime-calibration propagation cite this implication. The proof is a one-line lift: apply the pointwise successor-transport-to-comparable-trace lemma under the universal quantifiers of the two target Props.
Claim. Assume that every ratio-orbit character $\chi$ that is prime-direction calibrated has identity successor transport on prime-floor orbits (above the self-reciprocal unit floor). Then every such $\chi$ has identity orientation that respects comparability of finite $\delta$-orbit traces.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read. Prime-direction calibration fixes the orientation of $\chi$ along a distinguished prime axis. The native cost is recovered from such characters via doubled-trace and d'Alembert-type identities; uniqueness arguments therefore track which orientations calibration is allowed to force.
Two global target Props sit in this chain. The floor-successor target says prime calibration forces identity successor transport above the self-reciprocal unit floor, not additive transport out of the unit orbit. The comparable-trace target is sharper on order: prime calibration should force identity orientation to respect comparability of finite $\delta$-orbit traces.
Upstream, the pointwise lemma already shows that any single character with prime-floor identity successor transport automatically respects comparable trace under identity orientation. The present declaration only globalizes that implication to the two calibration-forced targets.
proof idea
Term-style tactic proof with two steps. Introduce a ratio character $\chi$ together with the hypotheses that it is a PRC ratio character and prime-direction calibrated. Apply the hypothesis target to those data to obtain prime-floor identity successor transport for $\chi$. Feed that witness into the upstream pointwise theorem, which converts floor successor transport into the comparable-trace identity property. Discharge; no further case splits.
why it matters
This is a pure target-implication step inside native-cost uniqueness for the Primitive Recognition Calculus. It lets the development keep the corrected floor-successor formulation (after the reciprocal-character check) while still discharging the sharper trace-order obligation used by orientation propagation.
Downstream it is consumed by the sharpened-orientation route to the prime-calibration propagation target, and it appears in the native-cost uniqueness blocker certificate's dependency web. In framework terms it supports the uniqueness path toward the forced J-cost (T5) and the Recognition Composition Law, by ensuring calibrated prime axes cannot scramble finite orbit-trace order when identity is selected.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.