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
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
source
def accepts {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Set Q) (w : Fin n β†’ A) (init : Q) (final : Q) (path : Fin (n + 1) β†’ Q) :
Prop

This is an incorrect definition of accepting path.

Equations
source
def accepts' {Q : Type u_1} {A : Type u_2} [Fintype A] {n : β„•} (Ξ΄ : A β†’ Q β†’ Set Q) (w : Fin n β†’ A) (init : Q) (final : Q) (path : Fin (n + 1) β†’ Q) :
Prop
Equations
source
def myΞ΄ :
Fin 2 β†’ Fin 2 β†’ Set (Fin 2)
Equations
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.
source
noncomputable def 𝓑 {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} :
β„• β†’ Q β†’ Finset Q
Equations
source
noncomputable def r {Q : Type u_1} {A : Type u_2} [Fintype A] [Fintype Q] {Ξ΄ : A β†’ Q β†’ Q} :
β„• β†’ Q β†’ β„•
Equations
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, β‹―βŸ©) = Fin.append (Fin.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) :
(Finset.filter (fun (w : Fin M β†’ A) => ast Ξ΄ w c = d) Finset.univ).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 : Q} {d : Q} (hβ‚€ : (Finset.filter (fun (w : Fin n β†’ A) => ast Ξ΄ w c = d) Finset.univ).card β‰₯ 1) (h₁ : (Finset.filter (fun (w : Fin n β†’ A) => ast Ξ΄ w c = d) Finset.univ).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 : Q} {d : Q} (hβ‚€ : (Finset.filter (fun (w : Fin n β†’ A) => ast Ξ΄ w c = d) Finset.univ).card = 1) (hA : Fintype.card A β‰₯ 2) :
Fintype.card Q β‰₯ n + 1

Quas' Theorem.