divides_iff_toNat_dvd
plain-language theorem explainer
Native divisibility on distinction orbits is equivalent to ordinary Nat divisibility of their verifier counts. Anyone proving factorization, units, or Euclidean lemmas on DistinctionNat cites this bridge. The proof is a two-sided transport: multiply witnesses under toNat, and rebuild witnesses via ofNat with injectivity.
Claim. For finite distinction orbits $a,b$, the native relation "$a$ divides $b$" holds if and only if the verifier natural numbers satisfy $a^{\mathrm{toNat}} \mid b^{\mathrm{toNat}}$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the δ-orbit of K2.12. Its verifier map toNat reads the iteration count into Lean Nat; ofNat builds the orbit back, and toNat_ofNat says the round-trip is identity.
Multiplication on orbits is defined so that it recovers ordinary Nat multiplication under toNat (the recovery theorem toNat_mul). Native divisibility divides a b means there exists an orbit witness $k$ with $b = a \cdot k$. The module sits in Primitive Recognition Calculus orbit arithmetic: native structure first, Nat only as a display.
Upstream injectivity toNat_inj lets equal verifier counts force equal orbits, which is the return path of the equivalence.
proof idea
Iff by constructor.
Forward: from $b = a \cdot k$, apply toNat, rewrite with toNat_mul, and take the witness $k^{\mathrm{toNat}}$.
Backward: from $b^{\mathrm{toNat}} = a^{\mathrm{toNat}} \cdot k$ in Nat, rebuild the witness as ofNat k. Apply toNat_inj after rewriting toNat_mul and toNat_ofNat so the Nat equation lifts to an orbit equation.
why it matters
This is the display bridge for the whole orbit divisibility surface. The certificate orbit_divisibility_certificate records it as divides_display, closing native divisibility against Nat.
Downstream it feeds antisymmetry of divides, the unit characterizations (divides_one_iff_unit, unit_of_divides_unit), Euclidean lemmas (coprime cancellation, gcd divisibility), and factorization: prime_divisor_is_coordinate_base converts a native prime divisor into a Nat prime divisor to match coordinate bases, and period-gap factorization routes through the same display.
In the Recognition stack this is arithmetic infrastructure under the forcing chain, not a physics constant claim: it lets prime-orbit and period-factor arguments stay native while borrowing Nat number theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.