twoAdicAxisTwistCharacter_succ_three_not_identity
plain-language theorem explainer
The two-adic axis twist character fails identity orientation at the successor of the three-orbit (the four-position). Anyone excluding non-native cost characters that only calibrate on primes cites this fact. The argument reduces the identity claim to a rational equality and kills it by direct numerical evaluation of the twist at four.
Claim. Let $\chi$ be the two-adic axis twist character on ratio orbits. Write $p=\mathrm{succ}(3)$ for the successor of the three-orbit (so $p\neq 0$). Then $\chi$ does not fix the orbit direction of $p$: the image $\chi(\mathrm{orbitDirection}(p))$ is not cross-equal to $\mathrm{orbitDirection}(p)$ itself.
background
This sits in the Primitive Recognition Calculus native-cost uniqueness development. Ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equality of two ratio orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq).
Identity orientation for a character $\chi$ at a nonzero distinction position $p$ means $\chi$ fixes the orbit direction of $p$ up to cross-equality. The doc-comment stresses this is for arbitrary nonzero orbits, not only prime axes, so trace transport can pass composite positions.
DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). The two-adic axis twist is a concrete candidate character under test against native cost; the four-position is the first composite successor step past the three-orbit.
proof idea
Term-mode proof by contradiction. Assume identity orientation at $\mathrm{succ}(3)$. Unfold the identity predicate, rewrite cross-equality to rational equality, and push both sides to rationals via the character-to-rat and orbit-direction-to-rat lemmas, together with toNat_succ and the three-orbit value. The resulting numerical claim is discharged by norm_num against the explicit two-adic twist rational at four.
why it matters
Feeds the immediate parent PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget_refuted, which shows that prime-direction calibration of the two-adic axis twist does not force identity orientation to extend along successor steps. That refutation is a negative step in the native-cost uniqueness argument: candidate characters that look calibrated on primes still break at composite orbit positions.
In the broader Recognition forcing picture this protects the uniqueness path toward the J-cost (T5) and the self-similar fixed point $\phi$ (T6). If identity orientation extended automatically from primes through successors, alternative twist characters could impersonate native cost on a denser set of orbits; this lemma blocks that impersonation at four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.