PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget_refuted
plain-language theorem explainer
The forward prime-floor successor target is false: prime-direction calibration of a ratio character does not force identity orientation to extend along successor steps on every prime floor orbit. Anyone tracking native-cost uniqueness blockers or the universal-foundation certificate will cite this. The proof is a concrete counterexample: the two-adic axis-twist character is calibrated yet fails the three-orbit successor identity.
Claim. It is not the case that every map $\chi$ on ratio 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) necessarily has the property that prime-floor orbit identity orientation extends through successor steps.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and generate a native cost via costFromCharacter. Prime-direction calibration means that cost agrees with the canonical $J$-cost on every prime orbit direction: for each prime distinction $p$, the cross-equality of the character cost with the on-orbit $J$-value holds.
Identity orientation on an arbitrary nonzero orbit direction is the statement that $\chi$ fixes that direction up to the orbit cross-equality (not only on prime axes). The successor-step extension property asks that once identity holds on a prime-floor orbit, it propagates along the successor construction used in the prime-floor ladder.
The target proposition packages the hopeful implication: every calibrated ratio character automatically enjoys that successor extension. The local module is building uniqueness of the native cost by forcing character orientation; this declaration is the negative half of that forcing analysis.
proof idea
Assume the universal target. Instantiate it on the two-adic axis-twist character. First obtain prime-direction calibration of that character from the dedicated two-adic axis-twist calibration lemma (using its branch data). The target then yields successor-step extension of prime-floor identity for this character.
Separately, the branch data of the twist character give orbit-direction identity on the three-orbit (distinct from the two-orbit). Feeding that identity into the successor-extension instance produces the three-orbit successor identity. That conclusion is exactly what twoAdicAxisTwistCharacter_succ_three_not_identity denies, yielding the contradiction.
why it matters
Native-cost uniqueness in PRC needs a clean account of which orientation constraints actually follow from prime calibration. This refutation kills the over-strong forward target that would have forced successor identity from calibration alone, so the uniqueness path must route through a corrected, weaker target (or an explicit blocker).
It feeds prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization/orientation targets into a single certificate object. That certificate is part of the conditional universal-foundation stack (prc_universal_foundation_conditional_certificate), sitting beside kernel, real-complete ordered field, and trace-logic certificates.
In framework terms this is foundation hygiene on the character side of $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), not a direct forcing of $\phi$, eight-tick, or $D=3$. It closes a false branch so the remaining uniqueness argument does not silently assume an orientation law the two-adic twist already breaks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.