PRCPrimeCalibrationForcesOrbitSuccessorAdditiveCompatibilityTarget
plain-language theorem explainer
Defines the proposed forcing claim that every prime-calibrated ratio character on rational orbits is additively compatible with the δ-successor on nonzero directions. Native-cost uniqueness work cites it as a sharp bridge from multiplicative characters to trace/additive structure. The body is a pure Prop abbreviation (no proof); the claim was later refuted by the reciprocal character.
Claim. Every map $\chi$ from rational orbits to rational orbits that is a ratio character and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit) is additively successor-compatible: for every nonzero orbit $p$, $\chi$ of the successor direction of $p$ equals $\chi$ of the direction of $p$ plus the unit orbit (equality up to cross-equivalence of ratio orbits).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-orbit denominator. Ratio characters are structure-preserving maps on these displays. Cost is recovered from a character via costFromCharacter and compared to the canonical $J$-cost on orbits.
Prime-direction calibration means that on every native prime orbit direction the character-generated cost agrees with canonical $J$ (cross-equivalence of ratio orbits). Additive successor compatibility is the bridge named upstream: for nonzero $p$, $\chi$ of the successor direction equals the orbit-sum of $\chi$ of the direction of $p$ with the unit orbit. The module is isolating exact Lean targets for native cost uniqueness after the forcing chain has fixed $J$ (T5) and the self-similar scale $\phi$ (T6).
Upstream, the reciprocal automorphism and reciprocal recognition event supply the natural involution that later falsifies this target; the native unit predicate marks the one-step orbit as the only multiplicative unit in the finite $\delta$-orbit.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over maps $\chi$: assume ratio-character and prime-direction calibration, conclude orbit-successor additive compatibility. No tactics or lemmas are applied; downstream results either assume the Prop as a hypothesis or refute it.
why it matters
This target was meant to close the gap between multiplicative ratio characters and the additive/trace structure needed for native cost uniqueness (the doubled-trace / d'Alembert side of the PRC cost story, tying back to RCL and T5 $J$-uniqueness). Downstream, PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_of_additive_compat shows that if the target held then successor-transport would follow. In fact the target is false: PRCPrimeCalibrationForcesOrbitSuccessorAdditiveCompatibilityTarget_refuted applies it to the reciprocal character (which is a prime-calibrated ratio character) and obtains a contradiction with reciprocal non-compatibility. The Pass-25 blocker certificate records the split of remaining uniqueness gaps into exact Lean targets after this correction. The inline note points to the repaired goal: prime calibration should force successor transport above the self-reciprocal unit floor, not additive transport out of the unit orbit itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.