threeOrbit_ne_twoOrbit
plain-language theorem explainer
The three-step distinction orbit is unequal to the two-step orbit. Anyone separating the prime-2 axis from the first odd-prime witness in PRC character or native-cost uniqueness cites this. The proof is a short term argument: push equality through the Nat embedding and discharge 3 ≠ 2 by norm_num.
Claim. On the base-neutral distinction naturals, the three-step orbit position is not equal to the two-step orbit position.
background
DistinctionNat is the inductive, base-neutral finite orbit of repeated distinction (zero and successor). Its verifier map toNat sends zero to 0 and successor to Nat.succ, so orbit equality is decided by ordinary natural numbers.
In the J-cost layer, twoOrbit is the two-step position (successor of one), with twoOrbit.toNat = 2. In this uniqueness module, threeOrbit is defined as the successor of twoOrbit and is documented as the canonical non-2 prime witness; its Nat image is 3.
The local setting is Primitive Recognition Calculus native-cost uniqueness: ratio characters, doubled-trace D'Alembert structure, and prime-direction calibration all need a concrete odd-prime orbit distinct from the 2-axis.
proof idea
Term-mode contradiction. Assume threeOrbit = twoOrbit. Apply congrArg DistinctionNat.toNat to obtain equality of Nat images. Rewrite with threeOrbit_toNat and twoOrbit_toNat to reach 3 = 2, then norm_num closes the goal. No further orbit or cost structure is used.
why it matters
Native-cost uniqueness treats 3 as the first odd-prime witness against the two-adic axis. Downstream results that consume this inequality include the two-three mixed image under a two-adic axis twist character, the derivation of non-two-prime mixed reciprocal-identity character from a two-adic twist, and several refutations of prime-calibration force targets (nonunit reciprocal branch transport, prime-floor identity contracting or extending successor steps, no-adjacent-mixed-orientation). It also feeds the absurdity of a two-adic axis-twist ratio character under prime-identity branch uniformity, and the two-identity clause of the three-adic axis-twist character. Without a proved 3 ≠ 2 at the orbit level, mixed two/three direction arguments and prime-calibration refutations cannot fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.