DeterministicBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.CompanionBridge.deterministic_bound line 13
Source documentation
A state lower bound for every deterministic recognizer of relation liveness.
```
theorem deterministic_bound (h s : ℕ) (hh : 2 ≤ h)
    (D : TwoNFA (SetRel (Fin h) (Fin h)) (Fin s))
    (hdet : D.Deterministic) (hD : D.language = sourceLanguage (Fin h)) :
    2 ^ ((h - 2) / 31) ≤ 4 * (s + 1) ^ 2 := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.sourceLanguage

theorem OAI.TwoWayComplementation.deterministic_rate line 29

Source documentation

Arithmetic specialization for the relation alphabet on n - 2 vertices.

theorem deterministic_rate (n s : ℕ) (hn : 131 ≤ n)
    (hb : 2 ^ ((n - 4) / 31) ≤ 4 * (s + 1) ^ 2) :
    (1 / 2 : ℝ) * 2 ^ ((n - 4) / 127) ≤ (s : ℝ) := by
…

theorem OAI.TwoWayComplementation.deterministic_liveness_lower_bound line 54

Source documentation

Deterministic lower bound with arbitrary finite state types.

theorem deterministic_liveness_lower_bound (n : ℕ) (hn : 131 ≤ n)
    (Q : Type*) [Fintype Q]
    (D : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) Q)
    (hdet : D.Deterministic) (hD : D.language = sourceLanguage (Fin (n - 2))) :
    (1 / 2 : ℝ) * 2 ^ ((n - 4) / 127) ≤ (Fintype.card Q : ℝ) := by
…

Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.sourceLanguage