coordinate_base_is_prime_divisor
plain-language theorem explainer
Every base appearing in a prime-coordinate factorization of an orbit number N is a prime orbit that divides N. Consumers of δ-coordinate factorizations cite this to treat list readout as a sound factor projection. The proof is a short divisibility chain: base divides its prime power, that power divides the coordinate product, and the product reconstructs N.
Claim. Let $N$ be an orbit number with prime-coordinate data: a list of prime-power coordinates whose product equals $N$. If $c$ is any coordinate on that list, then the base of $c$ is a prime orbit and divides $N$.
background
In the primitive recognition calculus, orbit numbers live in DistinctionNat. A prime-power coordinate packages a prime orbit base with a nonzero exponent; its value is the corresponding orbit power. Prime-coordinate data for $N$ is a list of such coordinates together with a reconstruction equality: the product of their values equals $N$.
Divisibility on orbit numbers is the native divides relation. Upstream, any nonzero exponent forces the base to divide its own orbit power, and membership in a coordinate list forces the coordinate value to divide the list product. The present lemma closes the remaining step from list membership to "base divides $N$".
Local setting is the CoordinateUniqueness module: soundness and uniqueness of the prime-coordinate readout of an orbit number, as a multiset of prime powers.
proof idea
Term-mode proof. Split the conjunction: the base is already marked prime by the coordinate structure field.
For divisibility, form two facts. First, the base divides the coordinate value by the nonzero-exponent orbit-power lemma. Second, that value divides the product of the full coordinate list by the membership-divides-product lemma. Rewrite the product via the reconstruction equality in the data, then transitively compose the two divisibility steps.
why it matters
This is the soundness half of factor recovery from coordinate lists. Downstream, the headline equivalence primeOrbit_divides_iff_mem_coordinate_bases uses it so that "$q$ divides $N$" becomes exactly "$q$ appears as a coordinate base": factor recovery is list membership, not a search. It also feeds the uniqueness certificate that packages the full readout story.
In the Recognition foundation stack this sits under PrimitiveRecognitionCalculus factorization: δ-coordinate arithmetic that underwrites unique prime factorization of orbit numbers. It does not itself invoke the forcing chain (T5–T8) or the J-cost law; it is pure arithmetic infrastructure those layers rely on when they read primes off reconstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.