def primes_set : Set ℕ

Equations

• primes_set = {n : ℕ | Nat.Prime n}

instance instInfiniteElemNatPrimes_set : Infinite ↑primes_set

Equations

• instInfiniteElemNatPrimes_set = ⋯

instance instDecidablePredNatMemSetPrimes_set : DecidablePred fun (n : ℕ) => n ∈ primes_set

Equations

• instDecidablePredNatMemSetPrimes_set n = n.decidablePrime

def primes (n : ℕ) : ℕ

Equations

• primes n = if n = 0 then 0 else ↑(Nat.Subtype.ofNat primes_set (n - 1))

theorem primes_zero : primes 0 = 0

def primes_inv_exists (n : ℕ) (n_prime : Nat.Prime n) : ∃ (i : ℕ), primes i = n

Equations

• ⋯ = ⋯

def primes_inv (n : ℕ) (n_prime : Nat.Prime n) : ℕ

Equations

• primes_inv n n_prime = Nat.find ⋯

def primes_inv_def (n : ℕ) (n_prime : Nat.Prime n) : primes (primes_inv n n_prime) = n

Equations

• ⋯ = ⋯

theorem primes_inv_pos (n : ℕ) (n_prime : Nat.Prime n) : 0 < primes_inv n n_prime

theorem primes_prime {n : ℕ} (hn : n > 0) : Nat.Prime (primes n)

def cayley_table (row : ℕ) (col : ℕ) : ℤ

Equations

• cayley_table row col = ↑(primes col) - ↑(primes row)

structure Ds : Type

Structure Ds holds the variable data.

• y : ℕ
• y_pos : self.y > 0
• x : ℤ
• width : ℕ
• height : ℕ
• B : ℤ
• L : ℤ

theorem Ds.y_pos (self : Ds) : self.y > 0

structure Beta : Type

Structure Beta holds the variable & static data.

• d : Ds
• P : ℕ
• three_lt_P : 3 < self.P
• prime_P : Nat.Prime self.P
• primeIndex : ℕ
• k : ℕ
• k_pos : self.k > 0
• k_x_y : ↑self.k = self.d.x + ↑self.d.y
• A : ℤ
• h1_A : self.A = ↑self.P - 3
• h2_A : self.A = 6 * self.d.x + 6 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 4 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 2 else 0
• h1_B : self.d.B = cayley_table 2 (self.primeIndex + self.d.width)
• h2_B : self.d.B = 6 * self.d.x + 12 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 8 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 4 else 0
• h1_L : self.d.L = cayley_table (2 + self.d.height) self.primeIndex
• h2_L : self.d.L = 6 * self.d.x
• E : ℤ
• h1_E : self.E = self.A
• h2_E : self.E = 6 * self.d.x + 6 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 4 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 2 else 0

theorem Beta.three_lt_P (self : Beta) : 3 < self.P

theorem Beta.prime_P (self : Beta) : Nat.Prime self.P

theorem Beta.k_pos (self : Beta) : self.k > 0

theorem Beta.k_x_y (self : Beta) : ↑self.k = self.d.x + ↑self.d.y

theorem Beta.h1_A (self : Beta) : self.A = ↑self.P - 3

theorem Beta.h2_A (self : Beta) : self.A = 6 * self.d.x + 6 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 4 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 2 else 0

theorem Beta.h1_B (self : Beta) : self.d.B = cayley_table 2 (self.primeIndex + self.d.width)

theorem Beta.h2_B (self : Beta) : self.d.B = 6 * self.d.x + 12 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 8 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 4 else 0

theorem Beta.h1_L (self : Beta) : self.d.L = cayley_table (2 + self.d.height) self.primeIndex

theorem Beta.h2_L (self : Beta) : self.d.L = 6 * self.d.x

theorem Beta.h1_E (self : Beta) : self.E = self.A

theorem Beta.h2_E (self : Beta) : self.E = 6 * self.d.x + 6 * ↑self.d.y - if ↑self.P = 6 * (self.d.x + ↑self.d.y) - 1 then 4 else if ↑self.P = 6 * (self.d.x + ↑self.d.y) + 1 then 2 else 0

noncomputable def beta_fixed (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (d : Ds) (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : d.L = cayley_table (2 + d.height) primeIndex') (h2L : d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) : Beta

We now define a function beta_fixed that builds a Beta from a Ds instance by fixing P, k, and the corresponding proofs.

Equations

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

noncomputable def beta_fixed' (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ∀ (d : Ds), ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : ∀ (d : Ds), A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : ∀ (d : Ds), d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : ∀ (d : Ds), d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : ∀ (d : Ds), d.L = cayley_table (2 + d.height) primeIndex') (h2L : ∀ (d : Ds), d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : ∀ (d : Ds), E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) : Ds → Beta

Define a wrapper beta_fixed' that fixes all parameters except the variable data d.

Equations

• beta_fixed' P' hP' hp' hk' hkpos' hkxy' primeIndex' A_val h1A h2A h1B h2B h1L h2L E_val h1E h2E d = beta_fixed P' hP' hp' d hk' hkpos' ⋯ primeIndex' A_val h1A ⋯ ⋯ ⋯ ⋯ ⋯ E_val h1E ⋯

theorem beta_fixed'_injective (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ∀ (d : Ds), ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : ∀ (d : Ds), A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : ∀ (d : Ds), d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : ∀ (d : Ds), d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : ∀ (d : Ds), d.L = cayley_table (2 + d.height) primeIndex') (h2L : ∀ (d : Ds), d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : ∀ (d : Ds), E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) : Function.Injective (beta_fixed' P' hP' hp' hk' hkpos' hkxy' primeIndex' A_val h1A h2A h1B h2B h1L h2L E_val h1E h2E)

Prove that beta_fixed' is injective; that is, if two Beta values built by beta_fixed' are equal, then the underlying Ds instances are equal.

noncomputable def beta_sub_inj (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ∀ (d : Ds), ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : ∀ (d : Ds), A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : ∀ (d : Ds), d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : ∀ (d : Ds), d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : ∀ (d : Ds), d.L = cayley_table (2 + d.height) primeIndex') (h2L : ∀ (d : Ds), d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : ∀ (d : Ds), E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (d : Ds) : { b : Beta // b.P = P' }

Define an injection from Ds into the subtype { b : Beta // b.P = P' } by mapping d to ⟨beta_fixed' P' ... d, rfl⟩.

Equations

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

theorem beta_sub_inj_injective (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ∀ (d : Ds), ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : ∀ (d : Ds), A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : ∀ (d : Ds), d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : ∀ (d : Ds), d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : ∀ (d : Ds), d.L = cayley_table (2 + d.height) primeIndex') (h2L : ∀ (d : Ds), d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : ∀ (d : Ds), E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) : Function.Injective (beta_sub_inj P' hP' hp' hk' hkpos' hkxy' primeIndex' A_val h1A h2A h1B h2B h1L h2L E_val h1E h2E)

Prove that beta_sub_inj is injective.

noncomputable def ds_inj (n : ℕ) : Ds

An injection from ℕ into Ds is given by mapping n to the Ds instance with all fields set to n+1 (or n+1 for x, width, height).

Equations

• ds_inj n = { y := n + 1, y_pos := ⋯, x := ↑n + 1, width := n + 1, height := n + 1, B := ↑n + 1, L := ↑n + 1 }

theorem ds_inj_injective : Function.Injective ds_inj

instance instInfiniteDs : Infinite Ds

Equations

• instInfiniteDs = ⋯

theorem Beta_fixed_infinite (P' : ℕ) (hP' : 3 < P') (hp' : Nat.Prime P') (hk' : ℕ) (hkpos' : hk' > 0) (hkxy' : ∀ (d : Ds), ↑hk' = d.x + ↑d.y) (primeIndex' : ℕ) (A_val : ℤ) (h1A : A_val = ↑P' - 3) (h2A : ∀ (d : Ds), A_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) (h1B : ∀ (d : Ds), d.B = cayley_table 2 (primeIndex' + d.width)) (h2B : ∀ (d : Ds), d.B = 6 * d.x + 12 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 8 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 4 else 0) (h1L : ∀ (d : Ds), d.L = cayley_table (2 + d.height) primeIndex') (h2L : ∀ (d : Ds), d.L = 6 * d.x) (E_val : ℤ) (h1E : E_val = A_val) (h2E : ∀ (d : Ds), E_val = 6 * d.x + 6 * ↑d.y - if ↑P' = 6 * (d.x + ↑d.y) - 1 then 4 else if ↑P' = 6 * (d.x + ↑d.y) + 1 then 2 else 0) : Infinite { b : Beta // b.P = P' }

Since Ds is infinite and beta_sub_inj is injective, the subtype { b : Beta // b.P = P' } is infinite.