primePowerCoordinateOfNatPrime
plain-language theorem explainer
Packages a classical prime natural number as one prime-power coordinate with unit exponent in the orbit language. Factorization transport and list-based coordinate builders cite it when lifting Nat primes into DistinctionNat coordinates. The body is a structure instance: embed via ofNat, set exponent to one, and discharge the prime-orbit and nonzero side conditions with named lemmas.
Claim. Given $p \in \mathbb{N}$ with $p$ prime, form the prime-power coordinate whose base is the orbit embedding of $p$ and whose exponent is the unit $1$, certified so that the base is a prime orbit and the exponent is nonzero.
background
In the primitive recognition calculus, integers live as orbit positions DistinctionNat, built from zero and successor. The map from verifier naturals into that type is the standard recursion that sends $0$ to zero and $n+1$ to the successor of the image of $n$.
A prime-power coordinate is a pair (base, exponent) in that language together with two certificates: the base lies on a prime orbit (no nontrivial factorization in the orbit sense), and the exponent is not zero. The orbit value of such a coordinate is the corresponding prime power in the distinction monoid.
This module transports classical factorization data back into that language. The key upstream fact used here is that if $p$ is a classical prime, then its orbit embedding is a prime orbit: the proof rewrites to the toNat characterization and uses that $p$ has no nontrivial Nat factors.
proof idea
Structure-instance definition, not a tactic proof. Base is the orbit embedding of $p$. Exponent is the unit one. The prime-orbit field is filled by the theorem that ofNat of a Nat prime is a prime orbit. The nonzero field is filled by the elementary fact that one is not zero in DistinctionNat.
why it matters
This is the atomic bridge from a single classical prime into the prime-coordinate language used for factorization readout. Downstream, the list mapper walks a list of Nat primes and conses this constructor at each head, building a full list of prime-power coordinates. Separately, the reconstruction theorem shows that the orbit value of this coordinate, read back to Nat, recovers $p$ exactly (via orbitPow and toNat simplification).
In the broader Recognition stack this sits in the classical-factorization transport layer of the primitive recognition calculus: it lets external prime data enter the distinction monoid as certified $p^1$ coordinates before products and nontrivial-factorization arguments run. It does not itself touch the forcing chain (T5–T8) or the J-cost law; it is infrastructure for reading primes in the orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.