Documentation

Acmoi.QuasTheorem

Quas' Theorem #

We prove the italicized statement that we "must prove" in Theorem 4.42 from Automatic complexity: a computable measure of irregularity

source
def ast {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Q) (w : Fin n β†’ A) (init : Q) :
Q

ast for "asterisk": ast Ξ΄ is what we in mathematics articles would call Ξ΄^*, the iteration of the transition function Ξ΄ over a word in.

Equations
Instances For
    source
    def astN {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Set Q) (w : Fin n β†’ A) (init : Q) :
    Set Q
    Equations
    Instances For
      source
      def accepts {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Set Q) (w : Fin n β†’ A) (init final : Q) (path : Fin (n + 1) β†’ Q) :
      Prop

      This is an incorrect definition of accepting path.

      Equations
      Instances For
        source
        def accepts' {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Set Q) (w : Fin n β†’ A) (init final : Q) (path : Fin (n + 1) β†’ Q) :
        Prop
        Equations
        Instances For
          source
          def myΞ΄ :
          Fin 2 β†’ Fin 2 β†’ Set (Fin 2)
          Equations
          Instances For
            source
            def kayleighΞ΄ {A : Type u_1} {k : β„•} (hk : k β‰₯ 1) {w : Fin (2 * k + 1) β†’ A} :
            A β†’ Fin (k + 1) β†’ Set (Fin (k + 1))
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def 𝓑 {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} :
              β„• β†’ Q β†’ Finset Q
              Equations
              Instances For
                source
                noncomputable def r {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} :
                β„• β†’ Q β†’ β„•
                Equations
                Instances For
                  source
                  theorem in_particular {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} (c : Q) :
                  𝓑 0 c = {c}
                  source
                  theorem case1 {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} (c : Q) :
                  ↑(𝓑 1 c) = ⋃ (b : A), Ξ΄ b '' ↑(𝓑 0 c)
                  source
                  theorem claimByQuas {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} (c : Q) (m : β„•) :
                  ↑(𝓑 (m + 1) c) = ⋃ (b : A), Ξ΄ b '' ↑(𝓑 m c)
                  source
                  theorem compl_of_card_lt (Ξ± : Type u_1) [Fintype Ξ±] (X : Finset Ξ±) :
                  X βŠ† Finset.univ β†’ X.card < Finset.univ.card β†’ βˆƒ (b' : Ξ±), b' ∈ Finset.univ \ X
                  source
                  theorem ast_append {Q : Type u_1} {A : Type u_2} [Fintype Q] [Fintype A] [Nonempty A] (Ξ΄ : A β†’ Q β†’ Q) {u v : β„•} (U : Fin u β†’ A) (V : Fin v β†’ A) (c : Q) :
                  ast Ξ΄ (Fin.append U V) c = ast Ξ΄ V (ast Ξ΄ U c)
                  source
                  theorem Fin.rtake {A : Sort u_1} {M m : β„•} (hmM : m + 1 ≀ M) (w : Fin M β†’ A) :
                  βˆƒ (v : Fin (M - (m + 1)) β†’ A), (fun (i : Fin (m + 1 + (M - (m + 1)))) => w βŸ¨β†‘i, β‹―βŸ©) = append (take (m + 1) hmM w) v
                  source
                  theorem claim443 {Q : Type u_1} {A : Type u_2} [Fintype Q] [Fintype A] [Nonempty A] {Ξ΄ : A β†’ Q β†’ Q} (hinj : βˆ€ (a : A), Function.Injective (Ξ΄ a)) {c : Q} {m : β„•} (h : r m c = r m.succ c) {M : β„•} (hM : M > m) {d : Q} (hd : d ∈ 𝓑 M c) :
                  {w : Fin M β†’ A | ast Ξ΄ w c = d}.card β‰₯ Fintype.card A

                  Claim 4.43 in Automatic complexity.

                  source
                  theorem arith {n : β„•} (r : β„• β†’ β„•) (hr : βˆ€ j < n, r j < r (j + 1)) :
                  n + r 0 ≀ r n
                  source
                  theorem arith' {n : β„•} (r : β„• β†’ β„•) (h : r 0 β‰₯ 1) (hr : βˆ€ j < n, r j < r (j + 1)) :
                  n + 1 ≀ r n
                  source
                  theorem quas_family {Q : Type u_1} {A : Type u_2} [Fintype Q] [Fintype A] {Ξ΄ : A β†’ Q β†’ Q} (hinj : βˆ€ (a : A), Function.Injective (Ξ΄ a)) {n : β„•} {c d : Q} (hβ‚€ : {w : Fin n β†’ A | ast Ξ΄ w c = d}.card β‰₯ 1) (h₁ : {w : Fin n β†’ A | ast Ξ΄ w c = d}.card < Fintype.card A) :
                  Fintype.card Q β‰₯ n + 1
                  source
                  theorem quas' {Q : Type u_1} {A : Type u_2} [Fintype Q] [Fintype A] {Ξ΄ : A β†’ Q β†’ Q} (hinj : βˆ€ (a : A), Function.Injective (Ξ΄ a)) {n : β„•} {c d : Q} (hβ‚€ : {w : Fin n β†’ A | ast Ξ΄ w c = d}.card = 1) (hA : Fintype.card A β‰₯ 2) :
                  Fintype.card Q β‰₯ n + 1

                  Quas' Theorem.