unit
plain-language theorem explainer
Defines the native unit predicate on finite distinction orbits: an orbit is a unit exactly when it equals the one-step orbit. Orbit-divisibility and prime-factorization arguments cite it to exclude trivial factors. The body is a one-line propositional abbreviation, equality to the multiplicative identity.
Claim. For a finite distinction orbit $a$, the predicate $\mathrm{unit}(a)$ holds if and only if $a$ equals the one-step orbit (the multiplicative identity of the $\delta$-orbit monoid).
background
The ambient type is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals built from zero and successor, standing for closed $\delta$-orbits rather than bare counting numbers. The sibling module supplies the multiplicative arithmetic on these orbits (identity one, multiplication, and the divides relation).
In that monoid the only multiplicative unit is the one-step orbit. The present definition packages that fact as a Prop so later divisibility lemmas can say "non-unit" without repeating the equality. Downstream factorization language (nontrivial factorization, prime orbit) requires both factors nonzero and non-unit; this predicate is the non-unit half of that filter.
Local setting is Primitive Recognition Calculus orbit arithmetic: divisibility of distinction orbits before any continuum or Clifford lift.
proof idea
Definitional abbreviation, not a proved theorem. The body is the propositional equality of the argument with the one-step orbit identity. No tactics, no lemmas: unfolding unit a is definitionally a = one.
why it matters
Gives the monoid-unit side of native orbit divisibility. Sibling notions (divides, nontrivial factorization, prime orbit) use it to bar the identity from counting as a proper factor, so primality and unique-factorization statements on $\delta$-orbits stay meaningful.
In the broader Recognition stack this sits under Primitive Recognition Calculus, upstream of cost-algebra and $\varphi$-ladder work: clean orbit factorization is part of the discrete substrate that later supports J-cost self-similarity (T5) and the eight-tick structure (T7). The definition itself closes no open forcing step; it is scaffolding vocabulary for the arithmetic layer those steps rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.