divides_mul_left
plain-language theorem explainer
Any finite orbit position divides every left multiple of itself under native orbit multiplication. Factorization and coordinate-uniqueness arguments cite this as the elementary left-absorption law for orbit divisibility. The proof is a one-line existential: the cofactor is the left factor, after commuting the product.
Claim. For all finite orbit positions $a,b$ in the base-neutral distinction orbit, $b$ divides $a\cdot b$: there exists an orbit position $k$ such that $b\cdot k=a\cdot b$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying the native arithmetic of the primitive recognition calculus. Multiplication on this type is commutative; the module imports the orbit-arithmetic commutativity law proved by induction on the left factor.
Native orbit divisibility is the existential monoid relation: $a$ divides $b$ when there is some orbit position $k$ with $a\cdot k=b$. This is the δ-orbit stand-in for ordinary natural-number divisibility, kept internal to the orbit type rather than routed through a toNat embedding at every step.
The local setting is the OrbitDivisibility layer: reflexive and zero cases, units, nontrivial factorizations, and prime-orbit predicates sit as siblings. The present fact is the left-multiple absorption rule needed before building certificates and unique factorization in δ coordinates.
proof idea
Unfold the existential definition of divides and supply the left factor $a$ as witness. The goal reduces to $b\cdot a=a\cdot b$, which is exactly the orbit-arithmetic commutativity lemma. A single rw [mul_comm] closes the equality. Term shape is refine ⟨a, ?_⟩ followed by that rewrite; no induction or case split.
why it matters
The fact is consumed by the orbit-divisibility certificate, which packages reflexive, transitive, and display laws to assert that the native divisibility surface is closed. It is also used in the coordinate-uniqueness layer: membership of a prime-power coordinate in a list implies that coordinate's value divides the product of the list, a step toward the fundamental theorem of arithmetic in δ coordinates (unique multiset of prime powers for any two prime-coordinate reconstructions of the same orbit number).
Within Recognition Science this sits in the Primitive Recognition Calculus foundation, beneath the forcing chain and the J-cost calculus. It does not itself force φ, the eight-tick octave, or $D=3$; it supplies the monoid bookkeeping those later layers assume when they treat orbit positions as multiplicative data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.