Documentation

Project

Equations
Instances For
    def primes (n : ) :
    Equations
    Instances For
      def primes_inv_exists (n : ) (n_prime : Nat.Prime n) :
      ∃ (i : ), primes i = n
      Equations
      • =
      Instances For
        def primes_inv (n : ) (n_prime : Nat.Prime n) :
        Equations
        Instances For
          def primes_inv_def (n : ) (n_prime : Nat.Prime n) :
          primes (primes_inv n n_prime) = n
          Equations
          • =
          Instances For
            theorem primes_inv_pos (n : ) (n_prime : Nat.Prime n) :
            0 < primes_inv n n_prime
            theorem primes_prime {n : } (hn : n > 0) :
            def cayley_table (row col : ) :
            Equations
            Instances For
              structure Ds :
              Instances For
                structure Beta :
                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) :
                    DsBeta
                    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) :
                      { b : Beta // b.P = P' }
                      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)
                        noncomputable def ds_inj (n : ) :
                        Equations
                        • ds_inj n = { y := n + 1, y_pos := , x := n + 1, width := n + 1, height := n + 1, B := n + 1, L := n + 1 }
                        Instances For
                          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' }