PrimeCoordinateData
plain-language theorem explainer
Packages a list of prime-power orbit coordinates whose product equals a fixed orbit number N. Anyone proving uniqueness or completeness of prime factorization in DistinctionNat cites this carrier. It is a pure data structure: a list field plus the reconstruction equality as a field proof.
Claim. For an orbit number $N$, prime-coordinate data is a list of prime-power coordinates $(p_i^{e_i})$ (each $p_i$ a prime orbit, each $e_i \neq 0$) together with a witness that the product of those prime powers equals $N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals built from zero and successor, used as the arithmetic carrier for orbit factorization.
A single prime-power coordinate is a pair (base, exponent) where the base is a prime orbit and the exponent is nonzero. The value of one such coordinate is the corresponding prime power in orbit arithmetic. The product of a list of those coordinates is defined recursively: empty list maps to one; cons multiplies the head value by the product of the tail.
This module sits in the factorization layer that turns orbit numbers into prime-coordinate readouts, feeding the uniqueness theorems that identify that readout with ordinary natural factorization of the display.
proof idea
No proof body: this is a structure definition. It bundles a list of prime-power coordinates with a single equality field asserting that the recursive product of those coordinates reconstructs N. Downstream theorems project the list and rewrite along the reconstruction equality.
why it matters
This is the carrier type for the fundamental theorem of arithmetic in δ coordinates. Downstream, any two such packages for the same N induce the same multiset factorization (primeCoordinateData_factorization_unique), every coordinate base is a prime divisor of N, and every prime orbit dividing N appears as some coordinate base. The headline equivalence is that a prime orbit q divides N if and only if q occurs among the coordinate bases: factor recovery becomes list membership on the readout.
It also feeds the coordinate-uniqueness certificate and the assisted/delta prime-coordinate transform wrappers in the same factorization stack. Within Recognition Science this is infrastructure for reading physical periods and prime structure off orbit numbers, not a forcing-chain step (T5–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.