threeOrbit_primeOrbit
plain-language theorem explainer
The three-step distinction orbit is a native prime orbit: nonzero, non-unit, and free of nontrivial factorization. Anyone working the PRC native-cost uniqueness or two-adic axis-twist arguments cites this as the canonical odd prime witness. The proof reduces via the toNat characterization and uses that 3 is prime in Nat.
Claim. The three-step orbit position $p_3$ on the base-neutral distinction orbit satisfies the native prime-orbit predicate: $p_3 \neq 0$, $p_3$ is not a unit, and $p_3$ admits no nontrivial factorization.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor), the native stand-in for $\mathbb{N}$ before any external prime theory is imported. An orbit position is a prime orbit when it is nonzero, non-unit, and has no nontrivial factorization in that native monoid.
The three-step orbit is defined as the successor of the two-step orbit and is the canonical non-$2$ prime witness in this module. Its underlying natural number is $3$ by a simp lemma. The bridge lemma primeOrbit_iff_toNat_no_nontrivial_factor states that the native prime-orbit predicate is equivalent to the corresponding no-nontrivial-factor statement on toNat, without defining primality by importing Nat.Prime as the definition of the native notion.
This sits in the PRC native-cost uniqueness development, where prime orbit positions calibrate ratio characters and cost functionals along two-adic and mixed prime directions.
proof idea
Rewrite the goal with primeOrbit_iff_toNat_no_nontrivial_factor, so it remains to show threeOrbit.toNat \neq 0, \neq 1, and that no pair of naturals both outside ${0,1}$ multiplies to that value. The first two conjuncts are immediate from threeOrbit_toNat and norm_num.
For the factorization clause, unpack a putative factor pair $(a,b)$ with $a\cdot b = \mathrm{toNat}(p_3)$. After simplifying with threeOrbit_toNat, one has $a\cdot b = 3$. Since $3$ is prime (decide), any divisor is $1$ or $3$; each case forces one of $a,b$ to be $1$, contradicting the nontriviality hypotheses. The arithmetic cleanup uses omega.
why it matters
Native cost uniqueness in PRC needs a concrete odd prime orbit so that two-adic axis twists and mixed two-three directions can be separated from pure two-power calibration. This lemma supplies that witness.
It is consumed throughout the uniqueness and refutation cluster: mixed-image statements for two-adic axis-twist characters, the main PRCNativeCostUniquenessTarget_refuted, admissibility blocks for twist-generated costs, and several prime-calibration force-target refutations (nonunit local orientation, reciprocal branch transport, prime-floor successor contracts/extends). Those results show that candidate cost characters forced by two-adic twists cannot stay prime-calibrated once the three-orbit is available as a genuine native prime.
In the broader Recognition forcing picture this is local scaffolding for the uniqueness of the J-cost side of the composition law, not a T5–T8 landmark itself, but it is the arithmetic pin that lets the module refute non-native cost generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.