IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PrimeCoordinateTransform
Defines the prime-power coordinate layer for recognition factorization: each coordinate is a prime orbit base with a nonzero exponent, and finite lists of such coordinates multiply to a reconstructed natural value. Factorization and uniqueness arguments cite this module for the data type and the product reconstruction lemmas. The content is mostly structure definitions plus elementary list-product and positivity facts.
claimA prime-power coordinate is a pair $(p,k)$ with $p$ a prime orbit base and $k\neq 0$ an exponent. Its value is $p^k$. A finite list of coordinates has product $\prod_i p_i^{k_i}$. Coordinate data packages such a list so that the product reconstructs the underlying natural number; single-prime data and append/cons product rules are included.
background
In the Primitive Recognition Calculus factorization stack, physical periods and orbit readouts (imported from PhysicalPeriodReadout) must be written in a canonical multiplicative form before uniqueness and goal-closure arguments can run. The natural language for that form is prime-power coordinates: each factor is a prime orbit raised to a nonzero integer exponent.
This module introduces that vocabulary. PrimePowerCoordinate is one prime base with a nonzero exponent; primePowerValue evaluates it. Lists of coordinates multiply via primeCoordinateProduct, with the usual nil/cons/append lemmas. PrimeCoordinateData packages a list together with the claim that the product reconstructs the intended natural, and singlePrimeCoordinateData builds the one-factor case. Auxiliary positivity facts (toNat_pos_of_ne_zero, toNat_ne_one_of_not_unit) and a nontrivial-factorization witness for non-prime-orbit values sit alongside the data type.
proof idea
This is primarily a definition and elementary-algebra module, not a deep proof development. Coordinates and their products are defined by structure and list recursion. Reconstruction and append/cons identities are proved by unfolding the product and using standard Nat arithmetic. The nontrivial-factorization lemma is a short case split: if a value is not a pure prime orbit, extract a proper factor and package it as coordinate data. No heavy upstream theorems beyond the imported period-readout layer are required.
why it matters in Recognition Science
Coordinate uniqueness and goal closure both import this module. Uniqueness needs a rigid prime-power presentation of factorization data so that two reconstructions of the same natural can be compared factorwise. Goal closure needs the same presentation to finish the factorization side of the primitive recognition calculus: once every non-unit is written as a product of prime-power coordinates, the remaining bookkeeping reduces to list and Nat lemmas already here.
In the broader Recognition Science foundation, this sits under the forcing and composition layer rather than at T5–T8 themselves. It supplies the discrete multiplicative skeleton on which period readouts and later uniqueness statements rest, so that factorization claims become checkable Lean objects instead of informal prime decompositions.
scope and limits
- Does not prove uniqueness of prime-power coordinates; that lives in CoordinateUniqueness.
- Does not close the full factorization goal; GoalClosure consumes this layer.
- Does not define physical period readout; that is imported upstream.
- Does not address continuous J-cost, phi-ladder masses, or T5–T8 forcing.
- Does not handle zero exponents; coordinates require nonzero exponents by construction.
used by (2)
depends on (1)
declarations in this module (35)
-
structure
PrimePowerCoordinate -
def
primePowerValue -
def
primeCoordinateProduct -
theorem
primeCoordinateProduct_nil -
theorem
primeCoordinateProduct_cons -
structure
PrimeCoordinateData -
theorem
primeCoordinateData_reconstructs -
theorem
primeCoordinateProduct_append -
def
singlePrimeCoordinateData -
theorem
nontrivialFactorization_of_not_primeOrbit -
theorem
toNat_pos_of_ne_zero -
theorem
toNat_ne_one_of_not_unit -
theorem
factor_left_toNat_lt_product -
theorem
factor_right_toNat_lt_product -
def
DeltaPrimeCoordinateTransform -
structure
AssistedPrimeCoordinateTransform -
theorem
primeOrbit_ofNat_of_natPrime -
def
primePowerCoordinateOfNatPrime -
theorem
primePowerValue_of_natPrime_toNat -
def
primeCoordinatesFromNatList -
theorem
primeCoordinateProduct_fromNatList_toNat -
def
natPrimeFactorCoordinates -
theorem
primeCoordinateProduct_natPrimeFactorCoordinates_toNat -
theorem
toNat_ne_zero_of_ne_zero -
def
deltaPrimeCoordinateTransform_classicalTransport -
theorem
deltaPrimeCoordinateTransform_exists -
theorem
nativePrimeCoordinateData_exists -
def
deltaPrimeCoordinateTransform_nativeChoice -
theorem
deltaPrimeCoordinateTransform_nativeChoice_exists -
theorem
primeCoordinateData_nonempty_of_nonunit -
theorem
base_divides_orbitPow_of_exponent_nonzero -
theorem
first_coordinate_prime_divisor -
theorem
deltaPrimeCoordinateTransform_recovers_prime_divisor -
structure
PrimeCoordinateTransformCertificate -
theorem
prime_coordinate_transform_certificate