PrimePowerCoordinate
plain-language theorem explainer
A prime-power coordinate is a pair of a prime orbit base and a nonzero exponent in the distinction naturals. Coordinate uniqueness and the δ-coordinate fundamental theorem of arithmetic cite it as the atomic factor unit. It is a structure with two data fields and two well-formedness hypotheses; no proof body.
Claim. A prime-power coordinate is a pair $(b,e)$ where $b$ is a distinction-natural that is a prime orbit (nonzero, non-unit, and free of nontrivial factorization) and $e$ is a nonzero distinction-natural.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, standing in for ordinary naturals without committing to a numeral base. A position $p$ is a prime orbit when it is nonzero, not a unit, and admits no nontrivial factorization.
This module sits in the factorization layer that reads orbit numbers as products of prime powers. The structure packages one such prime-power atom so that lists of coordinates can reconstruct an orbit and recover a unique multiset of factors. Upstream, primeOrbit supplies the primality predicate used as a field hypothesis.
The local setting is coordinate readout: each coordinate contributes a base raised to an exponent, and the product of those values is the reconstructed orbit number.
proof idea
No proof body. The declaration is a structure with fields base and exponent (both distinction-naturals), plus two Prop fields: base_prime asserting that the base is a prime orbit, and exponent_nonzero asserting the exponent is not zero. Inhabitants are built by supplying data and discharging those two obligations.
why it matters
This is the atomic unit for the coordinate-uniqueness layer. Downstream, coordinateFactorization maps a list of these coordinates to a Finsupp of Nat exponents; coordinate_base_is_prime_divisor shows every coordinate base is a prime orbit dividing $N$; and coordinateFactorization_eq_factorization_product equates the readout with the canonical Nat factorization of the reconstructed product.
The parent certificate CoordinateUniquenessCertificate packages the bridge from prime orbits to Nat primes and the uniqueness of factorization in δ coordinates. That uniqueness is the fundamental theorem of arithmetic restated for distinction-natural orbits: any two prime-coordinate reconstructions of the same orbit induce the same multiset of prime powers. The structure therefore underwrites the claim that factorization readout is sound and unique at the recognition-calculus level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.