PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget
plain-language theorem explainer
Names the proposition that every prime-calibrated ratio character automatically obeys successor-step transport (forward and backward one-step laws on nonzero orbit directions). Cited by the native-cost uniqueness blocker ledger and the universal-foundation open-target list. The body is a pure Prop packaging: no proof content. Downstream work refutes the claim.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (the cost generated by $\chi$ matches canonical $J$-cost on every prime orbit), then $\chi$ satisfies successor-step transport: both the forward and backward one-step identity laws on nonzero orbit directions.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a candidate factor for the d'Alembert factorization of a PRC cost: it sends the unit orbit to itself and is multiplicative, both up to cross-equivalence rather than definitional equality, so the statement stays quotient-native.
Prime-direction calibration asks that the cost built from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. Successor-step transport bundles the two one-step laws (extends and contracts the additive $\delta$-successor) needed for trace coherence. The ambient module isolates exact Lean targets for native-cost uniqueness; this definition is one such named target, exposing additive-trace compatibility missing from purely multiplicative character laws.
proof idea
Definitional Prop abbreviation, not a proved theorem. The body is the universal quantification over maps $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ of the implication chain ratio-character and prime-direction calibration imply successor-step transport. No tactics, no lemmas applied at this site; downstream lemmas either assume the target, derive it from a stronger additive-compatibility target, or refute it.
why it matters
Sits in the native-cost uniqueness program that aims to force the Recognition $J$-cost (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$) as the unique admissible cost. The doc-comment frames it as the sharper directional successor target that would supply the missing additive-trace compatibility.
Downstream, PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_of_transport weakens this target to the identity-successor form, and PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_of_additive_compat derives it from additive compatibility. Critically, PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_refuted proves the target false, so the route cannot force the final surface. The blocker certificate and PRCUniversalFoundationOpenTargets record this split: exact missing mathematics named, and this particular forcing route closed negatively.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.