one_divides
plain-language theorem explainer
The one-step distinction orbit divides every finite orbit position under native multiplication. Anyone assembling the orbit-divisibility certificate or building multiplicative arithmetic on DistinctionNat cites this left-unit law. The proof is a one-line existential wrapper: the cofactor is the target itself, discharged by one_mul_eq.
Claim. For every finite distinction-orbit position $a$, the one-step orbit $1$ divides $a$: there exists an orbit position $k$ such that $1 \cdot k = a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, standing in for discrete orbit positions rather than ordinary naturals. Multiplication on this type is the native orbit product imported from OrbitArithmetic.
Native divisibility is defined existentially: $a$ divides $b$ when there is some orbit position $k$ with $a \cdot k = b$. The constant one is the multiplicative unit of the orbit (the one-step position). The sibling lemma one_mul_eq states that one times any $a$ recovers $a$, which is exactly the witness equation needed here.
This module develops the divisibility surface on DistinctionNat: reflexive and zero cases, units, primes, and nontrivial factorizations, all before packaging them into a single certificate.
proof idea
One-line wrapper. Unfold divides to an existential and supply the pair $\langle a,, \mathrm{one_mul_eq}, a \rangle$: the cofactor is $a$ itself, and one_mul_eq proves $\mathrm{one} \cdot a = a$. No further case analysis or induction.
why it matters
Feeds orbit_divisibility_certificate, whose doc-comment states that "the native orbit divisibility surface is closed." That certificate packages divides_refl, divides_trans, and the bridge to ordinary Nat divisibility; the unit law one_divides is the missing left-identity half of the monoid picture (paired with mul_one_eq / one_mul_eq).
In the Primitive Recognition Calculus, orbit arithmetic is the discrete substrate under the forcing chain. Closing unit divisibility keeps the native multiplicative structure coherent before later layers attach cost, phi-ladder rungs, or eight-tick periodicity. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.