primePowerValue
plain-language theorem explainer
Maps a prime-power coordinate (prime orbit base with nonzero exponent) to its orbit value base^exponent in DistinctionNat. Factorization and uniqueness proofs cite it as the atomic prime-power contribution. The body is a one-line alias of orbitPow on the coordinate fields.
Claim. Given a prime-power coordinate $c=(b,e)$ with $b$ a prime orbit and $e\neq 0$, the orbit value of $c$ is $b^{e}$ in the distinction monoid (via $\delta$-native exponentiation).
background
DistinctionNat is the base-neutral inductive type of finite orbits of repeated distinction (zero and succ), the native carrier for factorization in the Primitive Recognition Calculus.
A PrimePowerCoordinate packages one prime orbit base $b$ together with a nonzero exponent $e$, with proofs that $b$ is prime as an orbit and $e\neq 0$. The local module builds the prime-coordinate transform: reading numbers as lists of such coordinates and reconstructing products.
orbitPow is $\delta$-native exponentiation on DistinctionNat: $\mathrm{orbitPow}(a,0)=1$ and $\mathrm{orbitPow}(a,k+1)=\mathrm{orbitPow}(a,k)\cdot a$. This definition simply evaluates that power on the coordinate's fields.
proof idea
Definitional one-liner: return orbitPow applied to the coordinate's base and exponent. No tactics or lemmas; the meaning is entirely that of orbitPow on a certified prime-power pair.
why it matters
Atomic readout of one prime-power factor in $\delta$ coordinates. Downstream, primeCoordinateProduct multiplies these values over a list; uniqueness and divisor theorems (coordinate_base_is_prime_divisor, mem_coordinate_divides_product, first_coordinate_prime_divisor, coordinateFactorization_eq_factorization_product) reduce to divides and factorization facts about primePowerValue.
In the Recognition foundation this is the bridge from abstract prime-orbit data to concrete orbit numbers, so the fundamental theorem of arithmetic in $\delta$ coordinates can be stated as uniqueness of multisets of such values. It sits under the Primitive Recognition Calculus factorization stack rather than the T0–T8 forcing chain directly, but supplies the arithmetic substrate those later physical readouts assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.