unit_of_divides_unit
plain-language theorem explainer
If a unit in the distinction orbit is divisible by another orbit position, that divisor is itself a unit. Algebraists closing the native orbit-divisibility surface cite this when packaging the certificate. The proof rewrites both sides to Nat, then applies Nat.dvd_one.
Claim. Let $a,b$ be positions in the distinction orbit $\mathrm{DistinctionNat}$. If $b$ is a unit (equals the one-step orbit) and $a$ divides $b$ natively (there exists $k$ with $a\cdot k=b$), then $a$ is a unit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying a native multiplicative structure imported from OrbitArithmetic.
Native divisibility says $a$ divides $b$ when there exists an orbit position $k$ with $a\cdot k=b$. The unit predicate asserts equality with the one-step orbit; the module notes that in the finite $\delta$-orbit this is the only multiplicative unit. Both notions display on ordinary naturals: divisibility iff $a.\mathrm{toNat}\mid b.\mathrm{toNat}$, and unit iff $a.\mathrm{toNat}=1$.
The local setting is the Primitive Recognition Calculus layer that builds an orbit-native arithmetic before any continuum or measure structure is introduced.
proof idea
Tactic proof in four steps. Rewrite the unit hypothesis and the goal via unit_iff_toNat_eq_one, so both become statements about toNat equaling 1. Extract the underlying Nat divisibility from divides_iff_toNat_dvd applied to the divides hypothesis. Substitute the rewritten unit fact into that Nat divisibility, obtaining a divisor of 1. Finish with Nat.dvd_one.
why it matters
Feeds orbit_divisibility_certificate, whose doc-comment states that the native orbit divisibility surface is closed. That certificate packages display, reflexivity, and related algebraic facts into a single structure; this lemma supplies the unit-stability under divisibility needed for a coherent multiplicative monoid of orbits.
In the Recognition foundation stack this sits under the primitive calculus that precedes the forcing chain (T0–T8). It does not itself force phi, the eight-tick octave, or D=3, but it keeps the discrete orbit arithmetic self-contained so later rungs can treat divisibility without leaking Nat-only reasoning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.