orbit_divisibility_certificate
plain-language theorem explainer
The native divisibility relation on finite distinction orbits is fully certified: it matches ordinary natural-number divisibility under the cardinality display, and obeys the standard monoid axioms (reflexivity, transitivity, antisymmetry, units, and prime factor laws). Anyone assembling the first-pass kernel certificate cites this bundle. The proof is a field-by-field assembly of already-proved orbit-arithmetic lemmas.
Claim. There is a closed certificate for divisibility on distinction orbits: for all $a,b$ in the distinction naturals, $a$ divides $b$ if and only if the underlying naturals satisfy $a_{\mathrm{nat}} \mid b_{\mathrm{nat}}$; the relation is reflexive, transitive, and antisymmetric; one divides every element and zero divides only zero; units are exactly the divisors of one; divisors of units are units; and prime orbits satisfy the usual prime-factor and prime-divisor properties (a prime dividing a product forces a unit factor, and a divisor of a prime is a unit or equal to that prime).
background
Distinction naturals are the base-neutral finite orbits of repeated distinction (K2.12): an inductive type with zero and successor, equipped with a forgetful map toNat into ordinary $\mathbb{N}$. Multiplication and the unit one are defined so that this display is a monoid homomorphism.
Native divisibility is the existential relation "$a$ divides $b$ when $b = a \cdot k$ for some orbit $k$". The key display lemma states that this is equivalent to ordinary divisibility of the underlying naturals. Units are the orbits whose display is $1$; nontrivial factorizations and prime orbits are likewise defined natively and shown to match their Nat counterparts.
The local module closes the arithmetic surface needed before kernel certificates can mention divisibility, primes, or units without leaving the distinction-orbit language.
proof idea
The proof inhabits the certificate structure by assigning one lemma per field. Display of divisibility is divides_iff_toNat_dvd. Reflexivity and the two multiplication-factor laws are the direct constructors divides_refl, divides_mul_right, divides_mul_left. Transitivity and antisymmetry are short wrappers around divides_trans and divides_antisymm (the latter via toNat injectivity and Nat.dvd_antisymm). Unit display, "divides one iff unit", and "divisor of a unit is a unit" reuse the corresponding unit lemmas. Nontrivial-factorization and prime-orbit displays are the iff lemmas already proved against toNat. The two prime properties are one-line applications of unit_or_unit_of_mul_eq_prime and unit_or_eq_of_divides_prime.
why it matters
This certificate is the single inhabited Prop that says the native orbit divisibility surface is closed. Downstream it is consumed by kernel_first_pass_certificate (K7/A2), which packages strength tags, trace syntax, judgment surface, and trace logic into the first-pass kernel. Without a closed divisibility surface, the kernel cannot talk about prime orbits or unit cancellation inside the distinction calculus.
In the broader Recognition stack this sits in the Foundation layer beneath the forcing chain: it equips the K2.12 distinction orbits with the monoid-divisibility facts needed before later steps reason about periods, octaves, or self-similar fixed points. It does not itself force $\varphi$, eight-tick structure, or $D=3$; it only guarantees that divisibility language is available and faithful to $\mathbb{N}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.