Equations
Equations
- primes_inv n n_prime = Nat.find ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- cayley_table row col = ↑(primes col) - ↑(primes row)
Instances For
Instances For
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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 ⋯
Instances For
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)
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
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)
: