singlePrimeCoordinateData
plain-language theorem explainer
For a prime orbit number N, packages N as prime-coordinate data with the singleton list N^1. Anyone assembling the native prime-coordinate transform cites this as the base case when N is already prime. Reconstruction is discharged by injecting through the Nat display and simplifying the one-factor product.
Claim. If $N$ is a prime orbit number, then the singleton list of prime-power coordinates with base $N$ and exponent $1$ is prime-coordinate data for $N$: the product of that list equals $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as the native arithmetic carrier in the Primitive Recognition Calculus. Orbit powers and multiplication on this carrier are displayed into ordinary Nat via toNat, with recovery theorems such as toNat_mul and orbitPow_toNat guaranteeing that the display is a ring homomorphism on the relevant operations.
Prime-coordinate data for an orbit number N is a list of prime-power coordinates together with a proof that their product reconstructs N. Each coordinate carries a prime base, a nonzero exponent, and the orbit value of one coordinate is orbitPow base exponent. The list product is defined recursively: empty list maps to one; cons multiplies the head value by the product of the tail.
This definition lives in the factorization layer that turns orbit numbers into prime-power coordinates, preparatory to transporting Mathlib's classical prime-factor lists across the δ/Nat equivalence.
proof idea
Build the structure by hand: coordinates is the singleton list whose unique entry has base N, exponent one, base_prime from the hypothesis that N is a prime orbit, and exponent_nonzero from one_ne_zero.
The reconstructs field is a short tactic proof. Apply toNat_inj to reduce equality of DistinctionNat values to equality after toNat. Then simp unfolds primeCoordinateProduct and primePowerValue on a singleton, rewrites orbitPow_toNat and one_toNat, and uses toNat_mul so the displayed product collapses to N.toNat * 1, matching the goal.
why it matters
This is the prime base case for native prime-coordinate data. Downstream, nativePrimeCoordinateData_exists asserts that every non-zero non-unit orbit number admits some PrimeCoordinateData; its proof routes through classical Nat factorization and must handle primes by packaging them exactly as this definition does.
The parent theorem's doc-comment frames the whole transform as classical transport of Mathlib's Nat.primeFactorsList across the established δ/Nat display, not a new factoring algorithm. Closing that existence statement needs a concrete constructor when N is already prime; this definition supplies it.
In the broader Recognition foundation, prime-coordinate factorization is scaffolding for reading physical periods and spectra off orbit arithmetic. It does not itself touch the forcing chain (T5–T8) or the J-cost law, but it keeps the arithmetic layer native to DistinctionNat rather than working only after forgetting to Nat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.