primeOrbit_divides_iff_mem_coordinate_bases
plain-language theorem explainer
For a nonzero distinction number N equipped with prime-coordinate data, a prime orbit q divides N if and only if q appears as some coordinate base in the readout. Anyone recovering factors from the classical-transport coordinate list cites this biconditional. The proof is a two-line constructor gluing the soundness and completeness lemmas already proved in the same module.
Claim. Let $N$ be a nonzero distinction natural with prime-coordinate data $D$, and let $q$ be a prime orbit. Then $q$ divides $N$ if and only if there exists a coordinate $c$ in $D$'s coordinate list with base equal to $q$.
background
In the Primitive Recognition Calculus, distinction naturals carry an orbit structure; a prime orbit is the recognition-side avatar of an ordinary prime. Prime-coordinate data for $N$ is a finite list of prime-power coordinates produced by the classical-transport transform: each entry has a prime-orbit base and an exponent, and the product of the corresponding prime powers recovers $N$.
The module builds a uniqueness package around that readout. Two sibling results already settle one direction each: every coordinate base is a prime orbit dividing $N$ (sound factor projection), and every prime orbit dividing $N$ appears as some coordinate base (complete factor oracle). The present statement packages those into a single membership criterion.
Locally this sits inside factorization uniqueness for the computable $\delta$ transport: factor recovery becomes list membership on the coordinate bases rather than a search over primes.
proof idea
Bidirectional constructor. Forward direction: if $q$ divides $N$, apply prime_divisor_is_coordinate_base (with the nonzero hypothesis and the prime-orbit assumption) to obtain a coordinate whose base equals $q$. Reverse direction: from a witness coordinate $c$ in the list with base $q$, rewrite along that equality and apply the second conjunct of coordinate_base_is_prime_divisor, which already records that every coordinate base divides $N$. No new arithmetic is done; the proof only glues the two one-sided lemmas.
why it matters
This is the headline readout equivalence for coordinate uniqueness: dividing by a prime orbit is exactly membership of that orbit among the coordinate bases. Downstream it feeds coordinate_uniqueness_certificate, which assembles the full certificate that the computable classical-transport transform induces the canonical Nat.factorization on every nonzero nonunit orbit number.
In the Recognition stack this closes the factor-oracle step of the primitive recognition calculus factorization layer: once bases are known to be exactly the prime divisors, uniqueness of the coordinate list follows from uniqueness of ordinary prime factorization, and the transport readout becomes a canonical prime decomposition without search. It is pure foundation arithmetic supporting later forcing and measure constructions, not itself a T0–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.