primeOrbit_of_unit_or_unit
plain-language theorem explainer
Converse native factor criterion: a nonzero non-unit position on the finite distinction orbit whose every product split has a unit factor is a prime orbit. Orbit-arithmetic workers cite it to promote the unit-factor condition to primality. The proof is a short refine that unpacks a nontrivial factorization and feeds it to the hypothesis for contradiction.
Claim. Let $p$ be a nonzero position on the finite distinction orbit that is not a unit. If every factorization $a\cdot b=p$ has $a$ or $b$ a unit, then $p$ is a prime orbit: nonzero, non-unit, and free of nontrivial factorization.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the native carrier for orbit arithmetic in the Primitive Recognition Calculus.
Multiplication on that carrier supports a native unit predicate: the only multiplicative unit is the one-step orbit. A nontrivial factorization is a product split into two factors that are both nonzero and non-unit. A prime orbit is then defined as a nonzero non-unit position with no nontrivial factorization.
This lemma sits in OrbitDivisibility, the module that develops divides, units, and prime orbits over that native arithmetic, importing the orbit carrier and OrbitArithmetic.
proof idea
Build the prime-orbit triple by refine, reusing the given nonzero and non-unit hypotheses. The remaining goal is absence of nontrivial factorization. Assume such a factorization exists, unpack the two factors with their nonzero and non-unit witnesses and the product equation, apply the unit-factor hypothesis to that product, and discharge each branch by the corresponding non-unit witness. Pure case analysis; no external lemmas beyond the local definitions.
why it matters
Closes the converse direction of the native factor characterization of prime orbits: unit-only factors imply primality on the finite distinction orbit. That characterization is the arithmetic backbone for later recognition-calculus arguments that treat prime orbit positions as indecomposable distinction steps.
No downstream users are wired yet in the graph, so the lemma is presently a self-contained foundation brick inside OrbitDivisibility rather than a cited step in a forcing-chain theorem. It supports the broader program of rebuilding number-theoretic structure on DistinctionNat before lifting to J-cost, phi-ladder, and the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.