divides_mul_right
plain-language theorem explainer
Any finite distinction orbit multiplies on the right into a multiple of itself: a always divides a·b. Factorization and coordinate-uniqueness arguments cite this as the basic right-absorption law for native orbit divisibility. The proof is a one-line existential witness: take the cofactor to be b and close by reflexivity.
Claim. For all finite distinction orbits $a$ and $b$, the native divisibility relation holds: $a$ divides $a \cdot b$. Equivalently, there exists an orbit $k$ such that $a \cdot k = a \cdot b$ (namely $k = b$).
background
DistinctionNat is the inductive type of finite orbits of repeated distinction (zero and successor), the base-neutral carrier for primitive recognition arithmetic. Multiplication on these orbits is the native product used throughout the orbit-arithmetic layer.
Native divisibility is defined existentially: $a$ divides $b$ when there is some orbit $k$ with $a \cdot k = b$. This is the orbit-level stand-in for ordinary natural-number divisibility, kept free of a preferred radix.
The local module develops the elementary lattice of this relation (reflexivity, zero, units, primes) so that later factorization and coordinate-readout theorems can quote a closed divisibility surface rather than reopening the definition.
proof idea
One-line wrapper. Unfold the existential definition of divides and supply the witness $k = b$; the required equality $a \cdot b = a \cdot b$ is reflexivity. No auxiliary lemmas are needed beyond the definition of divides and the product on DistinctionNat.
why it matters
This is the right-multiplication absorption law that every nontrivial factorization argument needs: each factor divides any product that contains it. Downstream, mem_coordinate_divides_product uses it to show that every prime-power coordinate divides the reconstructed orbit product (the uniqueness half of the fundamental theorem of arithmetic in δ coordinates). first_coordinate_prime_divisor quotes the same fact to recover a prime divisor by projecting the head of a coordinate list. The module-level orbit_divisibility_certificate packages reflexivity, transitivity, and display lemmas into a closed certificate; this lemma is part of the elementary toolkit that certificate rests on.
In the Recognition forcing chain the finite distinction orbit is the discrete skeleton beneath the eight-tick octave and the φ-ladder; keeping divisibility native (rather than transporting everything to ℕ) preserves that skeleton for later mass and coupling readouts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.