arithmoi-0.2.0.5: Efficient basic number-theoretic functions. Primes, powers, integer logarithms.

Portability Non-portable (GHC extensions) Provisional Daniel Fischer Safe-Infered

Math.NumberTheory.Primes.Testing.Certificates

Description

Certificates for primality or compositeness.

Synopsis

# Certificates

A certificate of either compositeness or primality of an `Integer`. Only numbers `> 1` can be certified, trying to create a certificate for other numbers raises an error.

Constructors

 Composite !CompositenessProof Prime !PrimalityProof

Instances

 Show Certificate

A proof of compositeness of a positive number. The type is abstract to ensure the validity of proofs.

Instances

 Show CompositenessProof

The number whose compositeness is proved.

The number whose compositeness is proved.

The number whose compositeness is proved.

A proof of primality of a positive number. The type is abstract to ensure the validity of proofs.

Instances

 Show PrimalityProof

The number whose primality is proved.

The number whose primality is proved.

The number whose primality is proved.

# Arguments

An argument for compositeness of a number (which must be `> 1`). `CompositenessProof`s translate directly to `CompositenessArguments`, correct arguments can be transformed into proofs. This type allows the manipulation of proofs while maintaining their correctness. The only way to access components of a `CompositenessProof` except the composite is through this type.

Constructors

 Divisors `compo == firstDiv*secondDiv`, where all are `> 1` Fieldscompo :: Integer firstDivisor :: Integer secondDivisor :: Integer Fermat `compo` fails the strong Fermat test for `fermatBase` Fieldscompo :: Integer fermatBase :: Integer Lucas `compo` fails the Lucas-Selfridge test Fieldscompo :: Integer Belief No particular reason given Fieldscompo :: Integer

An argument for primality of a number (which must be `> 1`). `PrimalityProof`s translate directly to `PrimalityArguments`, correct arguments can be transformed into proofs. This type allows the manipulation of proofs while maintaining their correctness. The only way to access components of a `PrimalityProof` except the prime is through this type.

Constructors

 Pock A suggested Pocklington certificate Fieldsaprime :: Integer largeFactor :: Integer smallFactor :: Integer factorList :: [(Integer, Int, Integer, PrimalityArgument)] Division Primality should be provable by trial division to `alimit` Fieldsaprime :: Integer alimit :: Integer Obvious `aprime` is said to be obviously prime, that holds for primes `< 30` Fieldsaprime :: Integer Assumption Primality assumed Fieldsaprime :: Integer

## Weaken proofs to arguments

`arguePrimality` transforms a proof of primality into an argument for primality.

`argueCompositeness` transforms a proof of compositeness into an argument for compositeness.

## Prove valid arguments

`verifyPrimalityArgument` checks the given argument and constructs a proof from it, if it is valid. For the explicit arguments, this is simple and resonably fast, for an `Assumption`, the verification uses `certify` and hence may take a long time.

`verifyCompositenessArgument` checks the given argument and constructs a proof from it, if it is valid. For the explicit arguments, this is simple and resonably fast, for a `Belief`, the verification uses `certify` and hence may take a long time.

# Determine and prove whether a number is prime or composite

`certify n` constructs, for `n > 1`, a proof of either primality or compositeness of `n`. This may take a very long time if the number has no small(ish) prime divisors

## Checks for the paranoid

Check the validity of a `Certificate`. Since it should be impossible to construct invalid certificates by the public interface, this should never return `False`.

Check the validity of a `CompositenessProof`. Since it should be impossible to create invalid proofs by the public interface, this should never return `False`.

Check the validity of a `PrimalityProof`. Since it should be impossible to create invalid proofs by the public interface, this should never return `False`.