primeOrbit
plain-language theorem explainer
Native primality on the finite distinction orbit: a position is prime when it is nonzero, not the multiplicative unit, and admits no nontrivial factorization. Factorization and coordinate-uniqueness layers cite it as the δ-native stand-in for ordinary Nat primality. The body is a three-conjunct Prop assembled from the local unit and factorization predicates, with no proof obligation.
Claim. For an orbit position $p$ in the base-neutral finite distinction orbit $\mathrm{DistinctionNat}$, $p$ is a prime orbit position when $p \neq 0$, $p$ is not the multiplicative unit (the one-step orbit), and there do not exist nonzero non-unit factors $a,b$ with $a \cdot b = p$.
background
The ambient type is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals with constructors zero and succ, carrying native multiplication from the orbit-arithmetic layer.
A unit is defined natively as equality with the one-step orbit; the doc states that in the finite δ-orbit this is the only multiplicative unit. Nontrivial factorization is the existence of factors $a,b$ both nonzero and non-unit whose product recovers $n$.
Together these give a δ-internal notion of primality that never mentions Nat.Prime at the definition site. Downstream bridges later prove equivalence with primality of the numeric display toNat.
proof idea
Definitional, not a proved theorem. The predicate is the conjunction of three Props: inequality with zero, negation of the unit predicate, and negation of nontrivial factorization. No tactics or upstream lemmas are applied; expansion is pure unfolding of unit and nontrivialFactorization.
why it matters
This is the native prime predicate that the factorization stack hangs on. Downstream, natPrime_toNat_of_primeOrbit and primeOrbit_iff_natPrime_toNat prove that δ-primality is exactly Nat.Prime of the display, so the readout inherits Mathlib factorization structure. Coordinate uniqueness uses it throughout: every coordinate base is a prime orbit dividing $N$; every prime orbit divisor appears as a coordinate base; and dividing $N$ is equivalent to membership in the coordinate-base list. The CoordinateUniquenessCertificate and GoalClosureCertificate both package these facts, making the definition the hinge between orbit arithmetic and unique prime-power coordinates in the Primitive Recognition Calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.