OAI/Combinatorics/ParityLifts/SparseCertificate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.bitSat_literal_map line 7
2. lemma OAI.ParityWL.Complexity.literal_assignment_extend line 22
3. lemma OAI.ParityWL.Complexity.holds_minimizeList line 29
4. def OAI.ParityWL.Complexity.literalSizeBound line 34
5. def OAI.ParityWL.Complexity.sparseDensity line 36
6. theorem OAI.ParityWL.Complexity.bit_sparse_certificate line 40

   Source documentation

   Bit-string certificates are for the very same deterministic sparse program, not an oracle for a mathematically chosen family.

   theorem bit_sparse_certificate {N : ℕ} (F : Formula N) (j : ℕ) (hj : 0<j) :
       ∃ T : SparseTree BitLiteral,
         T.root=minimizeList F.bitList ∧ T.Valid (12*j) ∧
         T.All (fun H => (treeEncode H).size≤literalSizeBound N) ∧
         (T.leaves.length : ℝ)≤(2 : ℝ)^((N : ℝ)/j) ∧
         (∀ H∈T.leaves, H.length ≤ sparseDensity (12*j) N ∧ ∀ C∈H, C.length≤3) ∧
         ((∃ H∈T.leaves, ∃ a, bitSat a H) ↔ F.Satisfiable) := by
   …

   Mentions: OAI.ParityWL.Complexity.Formula, OAI.ParityWL.Complexity.SparseTree, OAI.ParityWL.Complexity.BitLiteral, OAI.ParityWL.Complexity.minimizeList, OAI.ParityWL.Complexity.treeEncode, OAI.ParityWL.Complexity.literalSizeBound, OAI.ParityWL.Complexity.sparseDensity, OAI.ParityWL.Complexity.bitSat