divides
plain-language theorem explainer
Native divisibility on the finite δ-orbit: orbit position a divides b when some orbit k satisfies a·k = b. Factorization and coordinate-uniqueness layers cite it as the ambient order relation on DistinctionNat. The body is the standard existential definition of monoid divisibility.
Claim. For orbit positions $a,b$ in the finite $\delta$-orbit $\mathrm{DistinctionNat}$, $a$ divides $b$ if and only if there exists an orbit position $k$ such that $a \cdot k = b$.
background
The ambient carrier is DistinctionNat: the base-neutral finite orbit of repeated distinction (K2.12), an inductive type with zero and successor, standing for positions along the δ-step orbit rather than ordinary naturals. Multiplication is the monoid operation inherited from orbit arithmetic (imported via OrbitArithmetic).
This module builds the native divisibility layer on that monoid. Sibling predicates include the unit predicate (only the one-step orbit is a unit) and nontrivial factorization (both factors nonzero and non-unit). The definition is the usual monoid divisibility relation: existence of a multiplier taking a to b.
Upstream, DistinctionNat and the one-step extension (step) fix the orbit language; the unit predicate is defined immediately after and uses the same monoid structure.
proof idea
Definitional: no proof. The predicate is the Prop ∃ k : DistinctionNat, a * k = b, i.e. monoid divisibility under orbit multiplication. Downstream lemmas (reflexivity, zero cases, factorization endpoints) unfold or apply this existential directly.
why it matters
This is the ambient order relation for the entire δ-orbit factorization stack. Downstream, nontrivialFactorization_of_proper_divisor turns a proper nonunit divisor into a native nontrivial factorization ("the reusable endpoint for period-readout factoring"). Coordinate uniqueness uses it to assert that every coordinate base is a prime orbit dividing N, that membership in a coordinate list implies the prime-power value divides the product, and that prime-orbit divisibility matches coordinate-base membership. ChartTransitionCertificate and CoordinateUniquenessCertificate both quantify over this relation when stating product-display and factorization uniqueness.
In the Recognition framework it is scaffolding for reading prime structure off finite δ-orbits, feeding the factorization path that supports period readout and coordinate uniqueness on the orbit monoid. It is not itself a forcing-chain step (T0–T8); it is arithmetic infrastructure those later layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.