OAI/Combinatorics/ParityLifts/FixedBridge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.Complexity.reductionRate line 7
2. def OAI.ParityWL.Complexity.fixedSATCode line 10
3. theorem OAI.ParityWL.Complexity.fixed_reduction_rate line 15

   Source documentation

   A fully specified finite-alphabet SAT machine, with a parser degree independent of all fixed parameters. Every matrix and sparse leaf is actually written.

   theorem fixed_reduction_rate : ∃ P : ℕ, 0<P ∧ ∀ (j : ℕ), 0<j →
       ∀ (k : ℕ), 4 ≤ k → ∀ (c : Convention), ∀ [NeZero (bagParameter c k)],
       ∀ (i : Implementation) (M : Machine) (r : ℝ), 0 ≤ r → FixedWLBound M c i k r →
         ∀ ε : ℝ, 0<ε → ∃ C : ℝ, 0<C ∧
           SATTimeBound (fixedSATCode j (bagParameter c k) M).decision (fun N L =>
             C*(L+1 : ℝ)^(2*normalizeProgram.degree+2)*
               2^((reductionRate P j (bagParameter c k) r+ε)*N)) := by
   …

   Mentions: OAI.ParityWL.Convention, OAI.ParityWL.bagParameter, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.FixedWLBound, OAI.ParityWL.Complexity.SATTimeBound, OAI.ParityWL.Complexity.fixedSATCode, OAI.ParityWL.Complexity.reductionRate

4. lemma OAI.ParityWL.Complexity.SATTimeBound.mono line 44
5. lemma OAI.ParityWL.Complexity.SATTimeBound.rate_mono line 50