divides_trans
plain-language theorem explainer
Transitivity of native orbit divisibility: if a divides b and b divides c among finite distinction-orbit positions, then a divides c. Factorization and prime-coordinate uniqueness proofs cite it when chaining divisor relations along coordinate lists. The argument multiplies the two existential witnesses and reassociates with the orbit product law.
Claim. Let $a,b,c$ be positions in the finite distinction orbit. If $a$ divides $b$ and $b$ divides $c$ in the native sense (there exist orbit positions $m,n$ with $a\cdot m=b$ and $b\cdot n=c$), then $a$ divides $c$ (there exists an orbit position $k$ with $a\cdot k=c$).
background
DistinctionNat is the inductive type of base-neutral finite orbit positions under repeated distinction (K2.12): zero and successor. Multiplication on these positions is the native orbit product, transported from ordinary natural-number multiplication via the toNat embedding.
Native orbit divisibility is the monoid divisibility relation: $a$ divides $b$ when some orbit position $k$ satisfies $a\cdot k=b$. The surrounding module builds the full divisibility surface (units, primes, nontrivial factorizations, reflexivity) on that monoid.
Upstream, orbit multiplication is associative, $(a\cdot b)\cdot c=a\cdot(b\cdot c)$, proved by injecting to Nat and invoking Nat.mul_assoc. That single algebraic fact is the only nontrivial input to transitivity of divides.
proof idea
Unpack both existential hypotheses to witnesses $m$ and $n$ with $a\cdot m=b$ and $b\cdot n=c$. Offer the composite witness $m\cdot n$. Rewrite the goal with left-associated multiplication via mul_assoc, then substitute the two equalities to obtain $a\cdot(m\cdot n)=c$. Short tactic proof: rcases, refine the product pair, rewrite.
why it matters
Closes the transitive clause of the orbit divisibility certificate, which packages reflexivity, transitivity, and the display that native divides matches Nat.dvd under toNat. Downstream, coordinate uniqueness uses it so every coordinate base is a prime divisor of $N$, membership in a coordinate list implies the prime-power value divides the reconstructed product, and the first coordinate projects to a prime divisor of the reconstructed number. That is the monoid glue for unique factorization in $\delta$-coordinates (fundamental theorem of arithmetic in the primitive recognition calculus). It sits in Foundation arithmetic substrate, before the forcing chain (T0–T8) and physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.