def cayley_table (n : ℕ) : List (List ℤ)

Equations

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

def sub_array (n : ℕ) (start_c : ℕ) (end_c : ℕ) (end_r : ℕ) : Option (List (List ℤ))

Equations

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

structure Beta : Type

• A : ℤ
• B : ℤ
• L : ℤ
• E : ℤ
• isValid : self.A < self.B ∧ self.A > self.L ∧ self.B > self.L ∧ self.B > self.E ∧ self.L < self.E ∧ self.A = self.E

theorem Beta.isValid (self : Beta) : self.A < self.B ∧ self.A > self.L ∧ self.B > self.L ∧ self.B > self.E ∧ self.L < self.E ∧ self.A = self.E

instance instReprBeta : Repr Beta

Equations

• instReprBeta = { reprPrec := reprBeta✝ }

def beta_from_sub_array (sub : Option (List (List ℤ))) : Option Beta

Equations

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

theorem beta_field_sum_from_cayley (β : Beta) (m : ℤ) (n : ℤ) (c : ℤ) (k : ℤ) (hA : β.A = m + n) (hB : β.B = m + (n + k)) (hL : β.L = m + c + n) (hE : β.E = m + c + (n + k)) : β.B + β.L = β.A + β.E

theorem prime_form_6n_plus_1_or_6n_minus_1 (p : ℕ) (hprime : Nat.Prime p) (hp : 3 < p) : ∃ (n : ℕ), p = 6 * n + 1 ∨ p = 6 * n - 1

theorem infinitely_many_betas_with_prime_properties (p : ℕ) (hprime : Nat.Prime p) (hmin : 3 < p) : {β : Beta | ∃ (x : ℤ) (y : ℤ), x < x + y ∧ y > 0 ∧ (↑p = 6 * (x + y) - 1 ∧ β.A = 6 * x + 6 * y - 4 ∧ β.B = 6 * x + 12 * y - 8 ∧ β.L = 6 * x ∧ β.E = 6 * x + 6 * y - 4 ∧ Nat.Prime (β.B + 3).toNat ∧ Nat.Prime (β.B + 3 - β.E).toNat ∨ ↑p = 6 * (x + y) + 1 ∧ β.A = 6 * x + 6 * y - 2 ∧ β.B = 6 * x + 12 * y - 4 ∧ β.L = 6 * x ∧ β.E = 6 * x + 6 * y - 2 ∧ Nat.Prime (β.B + 3).toNat ∧ Nat.Prime (β.B + 3 - β.E).toNat)}.Infinite