OAI/Combinatorics/ParityLifts/SATChoice.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.Complexity.encodeGraphs line 9

   Source documentation

   This is a full row-major adjacency matrix, not an adjacency oracle or a colored-graph promise. Both matrices and their common order appear on the tape.

   noncomputable def encodeGraphs {n : ℕ} (G H : SimpleGraph (Fin n)) : List Bool := by
   …

2. inductive OAI.ParityWL.Complexity.Implementation line 15
3. def OAI.ParityWL.Complexity.Equivalent line 18
4. def OAI.ParityWL.Complexity.SATTimeBound line 25

   Source documentation

   An actual execution bound; no computation is hidden in its interpretation.

   def SATTimeBound (M : Machine) (B : ℕ → ℕ → ℝ) : Prop :=
   …

   Mentions: OAI.ParityWL.Complexity.Machine

5. def OAI.ParityWL.Complexity.PositiveRateETH line 32

   Source documentation

   Positive-rate ETH: one positive forbidden rate, with arbitrary fixed polynomial input factor. This is not the weaker uniform premise below.

   def PositiveRateETH : Prop :=
   …

6. def OAI.ParityWL.Complexity.UniformSubexponentialETH line 38

   Source documentation

   The same single machine must meet every positive exponential rate, with one fixed polynomial input factor. Constants may depend on the chosen rate.

   def UniformSubexponentialETH : Prop :=
   …

7. def OAI.ParityWL.Complexity.FixedWLBound line 44

   Source documentation

   Using n+1 includes the zero-order input and is exactly O(n^r) on positive orders. The finite exceptional small orders can be absorbed in the constant.

   noncomputable def FixedWLBound (M : Machine) (c : Convention) (i : Implementation)
       (k : ℕ) (r : ℝ) : Prop :=
   …

   Mentions: OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation

8. def OAI.ParityWL.Complexity.UniformWLBound line 50
9. def OAI.ParityWL.Complexity.FixedDimensionETHStatement line 57
10. def OAI.ParityWL.Complexity.UniformETHStatement line 62
11. def OAI.ParityWL.Complexity.groupWidth line 72
12. lemma OAI.ParityWL.Complexity.le_groupWidth_mul line 74
13. def OAI.ParityWL.Complexity.groupAt line 81
14. def OAI.ParityWL.Complexity.groupIndices line 84
15. lemma OAI.ParityWL.Complexity.group_indices_card line 87
16. def OAI.ParityWL.Complexity.clauseScope line 106
17. def OAI.ParityWL.Complexity.groupScope line 109
18. lemma OAI.ParityWL.Complexity.clauseScope_card line 112
19. lemma OAI.ParityWL.Complexity.groupScope_card line 115
20. def OAI.ParityWL.Complexity.extendScope line 123
21. lemma OAI.ParityWL.Complexity.extendScope_apply line 126
22. def OAI.ParityWL.Complexity.groupedChoice line 130
23. lemma OAI.ParityWL.Complexity.groupedChoice_size line 141
24. lemma OAI.ParityWL.Complexity.literal_mem_groupScope line 157
25. lemma OAI.ParityWL.Complexity.groupedChoice_successful_of_sat line 162
26. lemma OAI.ParityWL.Complexity.groupedChoice_agreement line 175
27. lemma OAI.ParityWL.Complexity.sat_of_groupedChoice_successful line 186
28. theorem OAI.ParityWL.Complexity.sat_grouping line 210

    Source documentation

    The grouping reduction, including empty groups, empty overlaps, and empty domains.

    theorem sat_grouping {N t : ℕ} (F : Formula N) (ht : 0 < t) :
        (groupedChoice F ht).SizeAtMost (2 ^ (3 * groupWidth F.length t)) ∧
        ((groupedChoice F ht).Successful ↔ F.Satisfiable) :=
    …

    Mentions: OAI.ParityWL.Complexity.Formula, OAI.ParityWL.Complexity.groupedChoice, OAI.ParityWL.Complexity.groupWidth

29. lemma OAI.ParityWL.Complexity.bagParameter_pos line 220
30. def OAI.ParityWL.Complexity.satChoice line 223
31. theorem OAI.ParityWL.Complexity.sat_parity_reduction line 228

    Source documentation

    The mathematical SAT-to-uncolored-graph reduction.

    theorem sat_parity_reduction (c : Convention) (k : ℕ) (hk : 4 ≤ k)
        {N : ℕ} (F : Formula N) :
        let C := satChoice c k hk F
    …

    Mentions: OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Formula, OAI.ParityWL.Complexity.satChoice

32. def OAI.ParityWL.Complexity.Formula.toCNF line 260
33. lemma OAI.ParityWL.Complexity.Formula.toCNF_width line 263
34. lemma OAI.ParityWL.Complexity.Formula.toCNF_holds line 269
35. def OAI.ParityWL.Complexity.CNF.toFormula line 279
36. lemma OAI.ParityWL.Complexity.CNF.toFormula_length line 283
37. lemma OAI.ParityWL.Complexity.CNF.toFormula_holds line 287
38. theorem OAI.ParityWL.Complexity.sat_sparsification line 300

    Source documentation

    The combinatorial IPZ producer at computably chosen thresholds 12j.

    theorem sat_sparsification {N : ℕ} (F : Formula N) (j : ℕ) (hj : 0 < j) :
        ∃ L : List (Formula N),
          (∀ H ∈ L, H.length ≤ 1 + 2 * N * (1 + (12 * j) ^ 2 + 2 * (12 * j) ^ 8)) ∧
          (∀ a : Fin N → Bool, F.Satisfied a ↔ ∃ H ∈ L, H.Satisfied a) ∧
          (L.length : ℝ) ≤ (2 : ℝ) ^ ((N : ℝ) / j) := by
    …

    Mentions: OAI.ParityWL.Complexity.Formula

39. lemma OAI.ParityWL.Complexity.sat_sparsification_or line 327