IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PrimeCoordinateTransform

declarations in this module (35)

• structure PrimePowerCoordinate L20
• def primePowerValue L27
• def primeCoordinateProduct L31
• theorem primeCoordinateProduct_nil L35
• theorem primeCoordinateProduct_cons L38
• structure PrimeCoordinateData L44
• theorem primeCoordinateData_reconstructs L48
• theorem primeCoordinateProduct_append L53
• def singlePrimeCoordinateData L64
• theorem nontrivialFactorization_of_not_primeOrbit L77
• theorem toNat_pos_of_ne_zero L85
• theorem toNat_ne_one_of_not_unit L94
• theorem factor_left_toNat_lt_product L102
• theorem factor_right_toNat_lt_product L115
• def DeltaPrimeCoordinateTransform L123
• structure AssistedPrimeCoordinateTransform L127
• theorem primeOrbit_ofNat_of_natPrime L134
• def primePowerCoordinateOfNatPrime L147
• theorem primePowerValue_of_natPrime_toNat L154
• def primeCoordinatesFromNatList L159
• theorem primeCoordinateProduct_fromNatList_toNat L168
• def natPrimeFactorCoordinates L179
• theorem primeCoordinateProduct_natPrimeFactorCoordinates_toNat L184
• theorem toNat_ne_zero_of_ne_zero L192
• def deltaPrimeCoordinateTransform_classicalTransport L203
• theorem deltaPrimeCoordinateTransform_exists L214
• theorem nativePrimeCoordinateData_exists L220
• def deltaPrimeCoordinateTransform_nativeChoice L255
• theorem deltaPrimeCoordinateTransform_nativeChoice_exists L260
• theorem primeCoordinateData_nonempty_of_nonunit L264
• theorem base_divides_orbitPow_of_exponent_nonzero L274
• theorem first_coordinate_prime_divisor L287
• theorem deltaPrimeCoordinateTransform_recovers_prime_divisor L312
• structure PrimeCoordinateTransformCertificate L326
• theorem prime_coordinate_transform_certificate L342