primeCoordinateData_reconstructs
plain-language theorem explainer
Any prime-coordinate packing of an orbit number N multiplies back to N. Factorization and period-readout arguments cite this as the reconstruction guarantee for prime-power lists. The proof is a one-line projection of the structure field that already stores the equality.
Claim. For every orbit number $N$ and every prime-coordinate datum for $N$ (a list of prime-power coordinates together with a reconstruction witness), the product of those prime-power values equals $N$.
background
In the Primitive Recognition Calculus, orbit numbers are the base-neutral finite orbits of repeated distinction (DistinctionNat): an inductive copy of the naturals used as the carrier for factorization and period readout, not as a preferred radix.
A prime-power coordinate packages a single prime raised to a multiplicity. The list product primeCoordinateProduct folds those values with the orbit monoid multiplication, sending the empty list to the unit orbit. PrimeCoordinateData N is the structure that pairs such a list with an equality asserting that the product recovers $N$.
This module sits under factorization and physical period readout: once an orbit is written in prime coordinates, downstream certificates can transport classical factorization facts into the recognition setting without re-proving reconstruction at each use site.
proof idea
One-line wrapper. The structure PrimeCoordinateData N already carries a field reconstructs : primeCoordinateProduct coordinates = N. The theorem simply projects that field: given data, return data.reconstructs. No extra algebra or induction is performed here.
why it matters
Feeds the certificate prime_coordinate_transform_certificate, whose first field is exactly this reconstruction law (data_reconstructs := fun N data => primeCoordinateData_reconstructs data). That certificate packages the prime-coordinate transform as a single reusable object for the factorization layer of the Primitive Recognition Calculus.
In the broader Recognition stack, orbit factorization is the discrete backbone under period readout and later forcing steps that need unique prime decompositions of distinction counts. This lemma is the trivial but mandatory interface: every packed coordinate list is faithful to its orbit number, so later uniqueness and transport results can treat reconstruction as given rather than re-derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.