PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget
plain-language theorem explainer
Names the open target that prime-direction calibration of a ratio character should force reciprocal orientation at the orbit-2 prime axis to travel along any finite δ-trace link to a native prime axis. Cited by the native-cost uniqueness blocker certificate and by the reciprocal/identity transport equivalence lemmas. Pure Prop abbreviation: no proof body beyond the quantified implication.
Claim. The following proposition is the two-prime reciprocal trace-connected target: for every map $\chi$ on ratio orbits that is a ratio character and is prime-direction calibrated (generated cost matches canonical $J$-cost on every native prime orbit), $\chi$ respects reciprocal branch transport along any finite $\delta$-trace connection from the orbit-$2$ prime axis to a native prime axis.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a map on those orbits; its generated cost is compared to the canonical $J$-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Prime-direction calibration means that on every native prime orbit the character-generated cost agrees with $J$ via the orbit cross-equality. The reciprocal automorphism swaps source and target and inverts the ratio; the two-prime reciprocal trace-connected predicate asks that the reciprocal branch at the orbit-$2$ prime axis transport along any finite $\delta$-trace connection to a target native prime axis.
This module isolates exact Lean targets for the still-open native cost uniqueness argument. The present definition packages one such target: calibration should force that reciprocal transport property.
proof idea
Definitional Prop, not a proved theorem. The body is the single quantified implication $\forall\chi,;\mathrm{ratio\ character}(\chi)\to\mathrm{prime\ calibrated}(\chi)\to\mathrm{two\text{-}prime\ reciprocal\ respects\ trace\ connected}(\chi)$. No tactics or lemmas are applied; downstream theorems treat the name as a hypothesis or as one side of an equivalence.
why it matters
Native cost uniqueness is not closed; the blocker certificate splits the gap into named targets, and this is the reciprocal trace-connected one. Downstream, it is equivalent to the two-prime identity trace-connected target (via reciprocal twist) and to the stronger-looking “forces prime reciprocal” form. Those equivalences feed the prime-identity trace-transport target used in the uniqueness chain.
In the broader forcing picture this sits under T5 $J$-uniqueness: once characters are calibrated on primes, orientation (identity vs reciprocal) must be rigid under $\delta$-trace transport so that the native cost cannot branch. Closing the target would discharge one exact blocker on the path from prime calibration to a unique native cost character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.