unit_iff_toNat_eq_one
plain-language theorem explainer
On the finite distinction orbit, the native unit predicate holds exactly when the verifier Nat display equals 1. Anyone working native divisibility, prime-orbit characterizations, or period-gap factorization cites this bridge. The proof is a two-direction constructor: unfold unit to equality with one, then use one_toNat and injectivity of toNat.
Claim. For every finite distinction-orbit position $a$, $a$ is a multiplicative unit if and only if its verifier natural number equals $1$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the native carrier for orbit arithmetic. Its verifier display toNat reads the iteration count as an ordinary Lean Nat (zero maps to 0, successor to succ).
In OrbitDivisibility, the multiplicative unit of the orbit is defined natively: unit a means $a$ equals the one-step orbit one. The simp fact one_toNat records that this one-step position displays as $1$. Upstream, OrbitArithmetic supplies toNat_inj: equal Nat displays come from equal orbit positions.
The local setting is the native divisibility surface on DistinctionNat (divides, unit, nontrivial factorization, prime orbit), before those predicates are certified against ordinary Nat arithmetic.
proof idea
Term-mode constructor on the biconditional.
Forward: assume unit a, unfold to $a = \mathrm{one}$, rewrite by that equality and one_toNat to get $a.\mathrm{toNat} = 1$.
Reverse: assume $a.\mathrm{toNat} = 1$, unfold the goal unit a to $a = \mathrm{one}$, apply toNat_inj, and rewrite the display equality together with one_toNat to finish.
why it matters
This is the unit half of the display bridge between native orbit predicates and ordinary Nat arithmetic. Downstream it is used heavily: divides_one_iff_unit rewrites divisors of one as units; nontrivialFactorization_iff_toNat and not_unit_ofNat_of_ne_one exclude the unit case when matching Nat factorizations; primeOrbit_iff_toNat_no_nontrivial_factor and orbit_divisibility_certificate close the native divisibility surface; Factorization modules use it for toNat_ne_one_of_not_unit and even-period-gap nontrivial factorizations.
In the Recognition foundation stack this sits under PrimitiveRecognitionCalculus orbit arithmetic, the discrete substrate that later feeds forcing-chain structure (eight-tick octave, D = 3). It does not itself invoke J-cost or phi; it keeps unit-hood synchronized with the verifier so later prime and period arguments stay native.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.