Main.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.complementation_lower_bound line 11

Source documentation

An n-state source language requires exponentially many states for any 2NFA complement.

theorem complementation_lower_bound (n : ℕ) (hn : 4 ≤ n) :
    ∃ A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n),
      ∀ s : ℕ, ∀ B : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin s),
        B.language = A.languageᶜ → 2 ^ ((n - 4) / 127) ≤ 2 * (s + 1) := by
…

Mentions: OAI.TwoWayComplementation.TwoNFA

theorem OAI.TwoWayComplementation.complementation_lower_bound_finite line 31
Source documentation
The real-valued lower bound for arbitrary finite target state sets.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, OAI.TwoWayComplementation.TwoNFA, SetRel, Fin, HSub.hSub, Fintype, Eq, Set, List, OAI.TwoWayComplementation.TwoNFA.language, Compl.compl, Real, HMul.hMul, HDiv.hDiv, HPow.hPow, Fintype.card
Proof uses: HAdd.hAdd, OAI.TwoWayComplementation.complementation_lower_bound, Exists.intro, OAI.TwoWayComplementation.TwoNFA.reindex, Fintype.equivFin, Eq.mpr, id, congrArg, OAI.TwoWayComplementation.TwoNFA.reindex_language, Eq.refl, cast, Eq.symm, Eq.trans, Nat.cast_one, congr, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance and 75 more
126 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/TwoWayComplementation.lean:36 (same statement text; different proof or body). Qualify references as OAI.TwoWayComplementation.complementation_lower_bound_finite@path.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem complementation_lower_bound_finite (n : ℕ) (hn : 4 ≤ n) :
    ∃ A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n),
      ∀ (Q : Type*) [Fintype Q], ∀ B : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) Q,
        B.language = A.languageᶜ →
          (1 / 2 : ℝ) * 2 ^ ((n - 4) / 127) - 1 ≤ (Fintype.card Q : ℝ) := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA

theorem OAI.TwoWayComplementation.tapeSymbol_map line 46

Source documentation

Letter maps commute with tape lookup and preserve the two endmarkers.

theorem tapeSymbol_map {Sigma Gamma : Type*} (f : Sigma → Gamma) (w : List Sigma)
    (p : Fin (w.length + 2)) :
    tapeSymbol (w.map f) ⟨p.val, by simp⟩ =
      Sum.map id f (tapeSymbol w p) := by
…

Mentions: OAI.TwoWayComplementation.tapeSymbol

def OAI.TwoWayComplementation.TwoNFA.pullAlphabet line 54
Source documentation
Pull an automaton back along a letter map, preserving its state set.
```
def TwoNFA.pullAlphabet {Sigma Gamma Q : Type*} (A : TwoNFA Gamma Q) (f : Sigma → Gamma) :
    TwoNFA Sigma Q where
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
theorem OAI.TwoWayComplementation.TwoNFA.pullAlphabet_language line 61
Source documentation
Letter pullback accepts exactly the words whose images the original machine accepts.
```
theorem TwoNFA.pullAlphabet_language {Sigma Gamma Q : Type*} (A : TwoNFA Gamma Q)
    (f : Sigma → Gamma) (w : List Sigma) :
    w ∈ (A.pullAlphabet f).language ↔ w.map f ∈ A.language := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.TwoNFA.language
theorem OAI.TwoWayComplementation.polynomial_not_bound_two_pow line 85
Source documentation
No real polynomial bounds the powers of two at all natural inputs.
```
theorem polynomial_not_bound_two_pow (p : Polynomial ℝ) :
    ¬ ∀ n : ℕ, (2 : ℝ) ^ n ≤ p.eval (n : ℝ) := by
…
```

theorem OAI.TwoWayComplementation.no_polynomial_complementation line 105

Source documentation

There is no polynomial state bound for complementation over all finite alphabets.

theorem no_polynomial_complementation :
    ¬ ∃ p : Polynomial ℝ, ∀ n k : ℕ, ∀ A : TwoNFA (Fin k) (Fin n),
      ∃ s : ℕ, ∃ B : TwoNFA (Fin k) (Fin s),
        B.language = A.languageᶜ ∧ (s : ℝ) ≤ p.eval (n : ℝ) := by
…

Mentions: OAI.TwoWayComplementation.TwoNFA