divides_refl
plain-language theorem explainer
Every finite distinction orbit divides itself under native orbit multiplication. Orbit-arithmetic and divisibility-certificate proofs cite this reflexivity fact. The argument is a one-line existential witness: the unit (one-step) orbit multiplies any orbit back to itself via the unit law.
Claim. For every finite distinction orbit $a$, $a$ divides $a$: there exists an orbit $k$ such that $a \cdot k = a$.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction (K2.12): constructors zero and successor. It carries a native multiplicative monoid structure imported from OrbitArithmetic.
Native orbit divisibility is the existential relation: $a$ divides $b$ when some orbit $k$ satisfies $a \cdot k = b$. The one-step orbit is the multiplicative unit, and the upstream unit law states that $a \cdot 1 = a$ for every $a$.
The local module builds the divisibility surface on these orbits (reflexivity, zero cases, primes, factorization) before packaging a closed certificate.
proof idea
One-line wrapper. The definition of divides is an existential; supply the unit orbit as witness and discharge the equation by the upstream unit law $a \cdot 1 = a$. No further case analysis or induction is required.
why it matters
Supplies the reflexive field of the orbit divisibility certificate, whose doc-comment states that the native orbit divisibility surface is closed. That certificate also records transitivity and the bridge from orbit divides to ordinary natural-number divisibility. In the Recognition foundation this is monoid bookkeeping on distinction orbits (Primitive Recognition Calculus), not yet a forcing-chain step (T5 J-uniqueness through T8 dimension), but it underwrites later arithmetic used by the calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.