OrbitDivisibilityCertificate
plain-language theorem explainer
A Prop-valued bundling certificate that packages the full native divisibility surface on finite distinction orbits: divides matches ordinary Nat divisibility under toNat, with reflexivity, transitivity, units, antisymmetry, and prime-factor laws. Anyone citing the closed orbit-arithmetic layer or the first-pass PRC kernel would use it. The structure itself is pure interface; the companion theorem fills every field from prior lemmas.
Claim. There is a closed certificate for divisibility on distinction orbits $D$: $a\mid b$ in $D$ if and only if $\mathrm{toNat}(a)\mid\mathrm{toNat}(b)$; $\mid$ is reflexive and transitive; $a\mid a\cdot b$ and $b\mid a\cdot b$; the unit orbit divides every orbit; zero divides only zero; units are exactly the orbits with $\mathrm{toNat}=1$; divisors of one are units; divisors of units are units; mutual divisibility implies equality; nontrivial factorization and primality match the usual Nat statements under $\mathrm{toNat}$; and if a prime orbit factors or is divided, one factor (resp. the divisor) is a unit or the prime itself.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the K2.12 carrier for primitive recognition calculus. Its verifier map toNat sends each orbit position to an ordinary natural number by counting steps.
Native divisibility is defined without leaving the orbit: $a$ divides $b$ when there exists an orbit $k$ with $a\cdot k=b$. A unit is a multiplicative unit in this monoid (only the one-step orbit). Nontrivial factorization means a product of two nonzero non-units; a prime orbit is nonzero, non-unit, and free of nontrivial factorization.
This module sits in the Primitive Recognition Calculus foundation layer, importing orbit arithmetic. The certificate is the single Prop that asserts the native surface is faithful to Nat divisibility and carries the standard monoid-divisibility and primality laws.
proof idea
No proof body: this is a structure declaration (a Prop bundling many fields), not a theorem. Each field is a named hypothesis stating one law of the native divisibility surface. The companion theorem orbit_divisibility_certificate inhabits the structure by assigning prior lemmas fieldwise (e.g. divides_iff_toNat_dvd for display, divides_refl, divides_trans, and the remaining orbit-arithmetic facts). Treat the structure as the interface contract those lemmas discharge.
why it matters
Closes the native orbit divisibility surface as a single citeable object. Downstream, orbit_divisibility_certificate proves the surface is inhabited, and KernelFirstPassCertificate (K7/A2) consumes the first-pass PRC kernel stages: analytic specification with concrete Lean objects along the first theorem chain. That kernel certificate is explicitly a bundling certificate, not yet the final inevitability theorem.
In the Recognition stack this is arithmetic-from-logic scaffolding under Primitive Recognition Calculus: finite distinction orbits must support a faithful divisibility and primality theory before mass ladders, forcing (T0–T8), or continuum physics attach. It does not itself force phi, eight-tick structure, or $D=3$; it locks the discrete monoid layer those later steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.