prime_divisor_is_coordinate_base
plain-language theorem explainer
Any prime orbit that divides a nonzero distinction integer N must appear as the base of some coordinate in any prime-coordinate readout of N. Factor-oracle completeness follows: the coordinate list is not missing prime factors. The proof bridges δ-native primes and divisibility to Nat.factorization support, then pulls the matching coordinate back via the reconstruction identity.
Claim. Let $N$ be a nonzero distinction natural with prime-coordinate reconstruction data $D$. If $q$ is a prime orbit and $q$ divides $N$, then some coordinate $c$ in $D$'s coordinate list has base $c.\mathrm{base}=q$.
background
Distinction naturals are the δ-native integers of the Primitive Recognition Calculus; toNat reads each as an ordinary Nat by counting iteration steps from the identity. A prime orbit is the δ-side primality predicate; natPrime_toNat_of_primeOrbit shows it forces the display to be a genuine Nat.Prime.
PrimeCoordinateData N packages a list of prime-power coordinates whose product reconstructs $N$. The associated coordinateFactorization is a Nat →₀ ℕ multiset of bases and exponents. Upstream, coordinateFactorization_eq_factorization_of_data identifies that multiset with the canonical Nat.factorization of $N$'s display: "the readout of $N$ is exactly the canonical factorization of $N$'s display."
This module develops uniqueness and soundness of that readout. The converse direction (every listed base is a prime divisor) is already available; the present theorem is the completeness half.
proof idea
Translate hypotheses to Nat: natPrime_toNat_of_primeOrbit gives Nat.Prime q.toNat, and divides_iff_toNat_dvd gives ordinary divisibility. Nonzeroness of $N$ becomes N.toNat ≠ 0 via toNat_inj and toNat_zero.
Those three facts place q.toNat in N.toNat.primeFactors, hence in the support of Nat.factorization N.toNat. Rewrite that support along coordinateFactorization_eq_factorization_of_data, then apply mem_support_coordinateFactorization to extract a list member whose base displays as q.toNat. Finish by toNat injectivity.
why it matters
This is the completeness half of the factor-oracle story for δ coordinates. Downstream it is the forward direction of primeOrbit_divides_iff_mem_coordinate_bases, the headline equivalence: "deciding whether $q$ divides $N$ is exactly checking whether $q$ is one of the coordinate bases. Factor recovery is list membership on the readout, not a search."
Together with the converse coordinate_base_is_prime_divisor, the coordinate list becomes a faithful, complete prime-factor certificate for nonzero $N$. In the Recognition foundation this is arithmetic structure lifted from the logic-native orbit calculus rather than assumed on Nat, feeding the factorization uniqueness chain that underwrites later ladder and mass bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.