Definitions

def Core4027.rFullPart (r m : ℕ) : ℕ

The r-full part of m: the product of p ^ v_p(m) over primes p with v_p(m) ≥ r.

Equations

• Core4027.rFullPart r m = (Finsupp.filter (fun (p : ℕ) => r ≤ m.factorization p) m.factorization).prod fun (p v : ℕ) => p ^ v

def Core4027.N : ℕ

The constant N = 2^14 * 3^4.

Equations

• Core4027.N = 1327104

def Core4027.Cpoly (t : ℕ) : ℕ

C(t) = t^4 + 42 t^2 + 72 t + 333.

Equations

• Core4027.Cpoly t = t ^ 4 + 42 * t ^ 2 + 72 * t + 333

def Core4027.Gpoly (t : ℕ) : ℕ

G(t).

Equations

• Core4027.Gpoly t = t ^ 9 + 108 * t ^ 7 + 216 * t ^ 6 + 4374 * t ^ 5 + 13608 * t ^ 4 + 99468 * t ^ 3 + 215784 * t ^ 2 + 998001 * t + 1474200

def Core4027.Hpoly (t : ℕ) : ℕ

H(t).

Equations

• One or more equations did not get rendered due to their size.

def Core4027.nn (t : ℕ) : ℕ

n = (G(t)/N)^3.

Equations

• Core4027.nn t = (Core4027.Gpoly t / Core4027.N) ^ 3

The rFullPart factorization theory

theorem Core4027.rFullPart_ne_zero (r M : ℕ) : rFullPart r M ≠ 0

theorem Core4027.rFullPart_cube_eq (a : ℕ) (ha : 1 ≤ a) : rFullPart 3 (a ^ 3) = a ^ 3

A perfect cube of a positive number is 3-full: its rFullPart 3 is itself.

theorem Core4027.rFullPart_factorization (r M q : ℕ) : (rFullPart r M).factorization q = if r ≤ M.factorization q then M.factorization q else 0

theorem Core4027.pow_dvd_rFullPart (M d : ℕ) (hM : 0 < M) (hd : d ^ 3 ∣ M) : d ^ 3 ∣ rFullPart 3 M

The key algebraic identity

theorem Core4027.IDENT (t : ℕ) : Gpoly t ^ 3 + N ^ 3 = Hpoly t * Cpoly t ^ 3

Polynomial congruence transfer

theorem Core4027.Cpoly_modEq {a b M : ℕ} (h : a ≡ b [MOD M]) : Cpoly a ≡ Cpoly b [MOD M]

theorem Core4027.Gpoly_modEq {a b M : ℕ} (h : a ≡ b [MOD M]) : Gpoly a ≡ Gpoly b [MOD M]

theorem Core4027.Hpoly_modEq {a b M : ℕ} (h : a ≡ b [MOD M]) : Hpoly a ≡ Hpoly b [MOD M]

Concrete constant facts

theorem Core4027.Gpoly_const_modN : Gpoly 23016 ≡ 0 [MOD N]

theorem Core4027.Cpoly_const_mod2 : Cpoly 23016 % 2 = 1

theorem Core4027.Cpoly_const_mod27 : Cpoly 23016 % 27 = 9

Pure polynomial bounds

theorem Core4027.Cpoly_gt (t : ℕ) : t ^ 4 < Cpoly t

theorem Core4027.Cpoly_cube_gt (t : ℕ) : t ^ 12 < Cpoly t ^ 3

theorem Core4027.Gpoly_ge_const (t : ℕ) : 1474200 ≤ Gpoly t

theorem Core4027.Gpoly_div_pos (t : ℕ) : 1 ≤ Gpoly t / N

theorem Core4027.Gpoly_upper (t : ℕ) (ht : 1676 ≤ t) : Gpoly t ≤ 2 * t ^ 9

theorem Core4027.Gpoly_cube_le (t : ℕ) (ht : 1676 ≤ t) : Gpoly t ^ 3 ≤ 8 * t ^ 27

T1 : n is 3-full

theorem Core4027.T1 (t : ℕ) : rFullPart 3 (nn t) = nn t

Main section: the prime-supply hypotheses

theorem Core4027.t_mod_N (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : t ≡ 23016 [MOD N]

theorem Core4027.t_mod_s3 (s t₀ t : ℕ) (ht : t = t₀ + N * s ^ 3) : t ≡ t₀ [MOD s ^ 3]

theorem Core4027.t_mod_s (s t₀ t : ℕ) (ht : t = t₀ + N * s ^ 3) : t ≡ t₀ [MOD s]

theorem Core4027.hHt (s t₀ t : ℕ) (hH : s ^ 3 ∣ Hpoly t₀) (ht : t = t₀ + N * s ^ 3) : s ^ 3 ∣ Hpoly t

theorem Core4027.hCt (s t₀ t : ℕ) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : ¬s ∣ Cpoly t

theorem Core4027.L1 (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : N ∣ Gpoly t

theorem Core4027.L2 (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : Cpoly t % 2 = 1

theorem Core4027.L3mod (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : Cpoly t % 27 = 9

theorem Core4027.L3a (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : 9 ∣ Cpoly t

theorem Core4027.L3b (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : ¬27 ∣ Cpoly t

theorem Core4027.hs_ge5 (s : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) : 5 ≤ s

theorem Core4027.Ns3_le_t (s t₀ t : ℕ) (ht : t = t₀ + N * s ^ 3) : N * s ^ 3 ≤ t

theorem Core4027.t_le_2Ns3 (s t₀ t : ℕ) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ N * s ^ 3) (ht : t = t₀ + N * s ^ 3) : t ≤ 2 * (N * s ^ 3)

theorem Core4027.t_big (s t₀ t : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) (ht : t = t₀ + N * s ^ 3) : 1676 ≤ t

theorem Core4027.N3_mul_nn (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : N ^ 3 * nn t = Gpoly t ^ 3

theorem Core4027.T0 (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : N ^ 3 * (nn t + 1) = Hpoly t * Cpoly t ^ 3

theorem Core4027.T0_div (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : nn t + 1 = Hpoly t * Cpoly t ^ 3 / N ^ 3

theorem Core4027.Ctil_eq (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : Cpoly t = 9 * (Cpoly t / 9)

theorem Core4027.Ctil_coprime6 (s t₀ t : ℕ) (hcong : t₀ % N = 23016 % N) (ht : t = t₀ + N * s ^ 3) : (Cpoly t / 9).Coprime 6

theorem Core4027.Ctil_coprime_s (s t₀ t : ℕ) (hs : Nat.Prime s) (hcong : t₀ % N = 23016 % N) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : (Cpoly t / 9).Coprime s

theorem Core4027.T2_dvd (s t₀ t : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) (hcong : t₀ % N = 23016 % N) (hH : s ^ 3 ∣ Hpoly t₀) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : (Cpoly t / 9 * s) ^ 3 ∣ nn t + 1

theorem Core4027.T2 (s t₀ t : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) (hcong : t₀ % N = 23016 % N) (hH : s ^ 3 ∣ Hpoly t₀) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : (Cpoly t / 9 * s) ^ 3 ∣ rFullPart 3 (nn t + 1)

theorem Core4027.B1_ge (s t₀ t : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) (hcong : t₀ % N = 23016 % N) (hH : s ^ 3 ∣ Hpoly t₀) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : (Cpoly t / 9 * s) ^ 3 ≤ rFullPart 3 (nn t + 1)

theorem Core4027.T3 (s t₀ t : ℕ) (hs : Nat.Prime s) (hs6 : ¬s ∣ 6) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ N * s ^ 3) (hcong : t₀ % N = 23016 % N) (hH : s ^ 3 ∣ Hpoly t₀) (hC : ¬s ∣ Cpoly t₀) (ht : t = t₀ + N * s ^ 3) : 8 ^ 13 * (1458 * N * (rFullPart 3 (nn t) * rFullPart 3 (nn t + 1))) ^ 27 > N ^ 39 * nn t ^ 40