PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
plain-language theorem explainer
Names the open target that prime-direction calibration of a ratio-orbit character forces identity orientation to respect finite δ-orbit trace comparability on every nonunit direction. Native-cost uniqueness and branch-transport reductions cite it as the trace-order form of nonunit identity transport. The body is a pure Prop abbreviation: universal quantification over calibrated characters into the comparable-trace predicate.
Claim. The following proposition holds as a named target: for every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character and is prime-direction calibrated, $\chi$ respects comparability of finite $\delta$-orbit traces under identity orientation on nonunit directions.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits; a PRC ratio character is the algebraic class used to rebuild native cost from doubled-trace data.
Prime-direction calibration pins the character on a distinguished prime ray so that local floor/successor data can be compared across directions. The comparable-trace predicate then asks that identity orientation (as opposed to the reciprocal branch) preserve finite $\delta$-orbit trace order whenever two nonunit directions are comparable.
This module packages native-cost uniqueness as a stack of exact Prop targets rather than a single closed theorem. The present definition is the trace-order sharpening of nonunit identity-branch transport: calibration should force identity orientation to respect comparability of those traces.
proof idea
No proof: the declaration is a def of a Prop. It expands to a single universal quantifier over maps $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, assuming the ratio-character and prime-direction-calibration hypotheses, and concluding the nonunit identity comparable-trace respect predicate. Downstream lemmas treat the name as an atomic target and prove equivalences or one-direction implications into branch-transport and prime-floor successor forms.
why it matters
Native cost uniqueness in Recognition Science needs J-cost (T5) recovered from character data on ratio orbits. This target is the trace-order form of the claim that prime calibration forces nonunit identity-branch agreement across directions.
It sits in a tight equivalence web: iff branch-transport, iff prime-floor successor transport, and iff the successor-step-pair target. Constructors and eliminators move freely between those shapes, so any proof of one discharges the others.
The Pass-25 blocker certificate lists the remaining open factorization and calibration goals; this comparable-trace target is one of the exact Lean hooks those certificates point at. Closing it (or an equivalent successor form) is a concrete step toward uniqueness of the native cost character and, upstream, toward the forced J-cost on the recognition ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.