ExplicitFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.explicit_complementation_family line 8

Source documentation

An explicit liveness witness and its complementation lower bound.

theorem explicit_complementation_family (n : ℕ) (hn : 4 ≤ n) :
    ∃ A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n),
      A.language = sourceLanguage (Fin (n - 2)) ∧
      (∀ (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, OAI.TwoWayComplementation.sourceLanguage

theorem OAI.TwoWayComplementation.explicit_family_main line 36
Source documentation
Both lower bounds hold for the same n-state liveness witness.
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, And, Eq, Set, List, OAI.TwoWayComplementation.TwoNFA.language, OAI.TwoWayComplementation.sourceLanguage, Fintype, Compl.compl, Real, HMul.hMul, HDiv.hDiv, HPow.hPow and 2 more
Proof uses: OAI.TwoWayComplementation.explicit_complementation_family, Exists.intro, And.intro, OAI.TwoWayComplementation.deterministic_liveness_lower_bound, Eq.trans
50 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/TwoWayDeterminization.lean:58 (same statement text; different proof or body). Qualify references as OAI.TwoWayComplementation.explicit_family_main@path.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem explicit_family_main (n : ℕ) (hn : 4 ≤ n) :
    ∃ A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n),
      A.language = sourceLanguage (Fin (n - 2)) ∧
      (∀ (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 : ℝ)) ∧
      (131 ≤ n → ∀ (Q : Type*) [Fintype Q],
        ∀ D : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) Q,
        D.Deterministic → D.language = A.language →
          (1 / 2 : ℝ) * 2 ^ ((n - 4) / 127) ≤ (Fintype.card Q : ℝ)) := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.sourceLanguage