Rabin certificate data for p = 2130706433

The modulus f has little-endian coefficients [1, 0, 0, 1, 0, 0, 1].

d = 6 is composite, so Rabin's coprimality condition needs one certificate per prime factor of d (2, 3), at exponents p^3, p^2 respectively. Checking only the linear-factor case would admit a product of equal-degree factors.

GENERATED. Do not edit by hand; regenerate with:

python3 scripts/gen_rabin_certificate.py --p 2130706433 \
  --f='1,0,0,1,0,0,1' \
  --lean <this file> --namespace KoalaBear.SexticCert \
  --authors 'Derek Sorensen'

Nothing here is trusted — the kernel re-checks every step through CompPoly.RabinCert.runChain, so incorrect data fails to compile rather than producing a false theorem.

def KoalaBear.SexticCert.traceSteps : List CompPoly.RabinCert.Step

Square-and-multiply chain for X^(p^6) mod f (258 steps).

Coprimality with X^(p^3) - X, for the prime factor 2 of d = 6.

def KoalaBear.SexticCert.cop3Steps : List CompPoly.RabinCert.Step

Square-and-multiply chain for X^(p^3) mod f (121 steps).

def KoalaBear.SexticCert.cop3Rp : List ℕ

The residue X^(p^3) mod f.

def KoalaBear.SexticCert.cop3W : List ℕ

cop3W = (X^(p^3) mod f) - X, the reduced form of X^(p^3) - X.

def KoalaBear.SexticCert.cop3U : List ℕ

Bézout coefficient: cop3U·f + cop3V·cop3W = 1.

def KoalaBear.SexticCert.cop3V : List ℕ

Bézout coefficient: cop3U·f + cop3V·cop3W = 1.

Coprimality with X^(p^2) - X, for the prime factor 3 of d = 6.

def KoalaBear.SexticCert.cop2Steps : List CompPoly.RabinCert.Step

Square-and-multiply chain for X^(p^2) mod f (75 steps).

def KoalaBear.SexticCert.cop2Rp : List ℕ

The residue X^(p^2) mod f.

def KoalaBear.SexticCert.cop2W : List ℕ

cop2W = (X^(p^2) mod f) - X, the reduced form of X^(p^2) - X.

def KoalaBear.SexticCert.cop2U : List ℕ

Bézout coefficient: cop2U·f + cop2V·cop2W = 1.

def KoalaBear.SexticCert.cop2V : List ℕ

Bézout coefficient: cop2U·f + cop2V·cop2W = 1.