OAI/Combinatorics/ParityLifts/BitTables.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.BitFormula line 7
  2. abbrev OAI.ParityWL.Complexity.Name line 8
  3. def OAI.ParityWL.Complexity.bitClauseSat line 10
  4. def OAI.ParityWL.Complexity.bitSat line 11
  5. def OAI.ParityWL.Complexity.names line 13
  6. lemma OAI.ParityWL.Complexity.mem_names line 15
  7. lemma OAI.ParityWL.Complexity.idxOf_inj_on line 18
  8. lemma OAI.ParityWL.Complexity.findIndex_idxOf line 23
  9. def OAI.ParityWL.Complexity.lookupBits line 34
  10. lemma OAI.ParityWL.Complexity.lookupBits_map line 37
  11. lemma OAI.ParityWL.Complexity.bitSat_congr line 44
  12. def OAI.ParityWL.Complexity.satisfyingWords line 52
  13. lemma OAI.ParityWL.Complexity.mem_satisfyingWords line 55
  14. def OAI.ParityWL.Complexity.pairKey line 61

    Source documentation

    The canonical smaller group's variable list fixes the order in a pair key. The shared-variable mask is identical on the two sides.

    def pairKey {t : ℕ} (Q : Fin t → BitFormula) (d : ℕ) (i j : Fin t) (bs : List Bool) : List Bool :=
…

    Mentions: OAI.ParityWL.Complexity.BitFormula

  15. lemma OAI.ParityWL.Complexity.pairKey_length line 67
  16. lemma OAI.ParityWL.Complexity.pairKey_symm_iff line 73
  17. def OAI.ParityWL.Complexity.rowKey line 99
  18. def OAI.ParityWL.Complexity.bitChoiceData line 102
  19. lemma OAI.ParityWL.Complexity.ChoiceData.success_rows line 105
  20. lemma OAI.ParityWL.Complexity.bitChoiceData_success_iff line 128
  21. theorem OAI.ParityWL.Complexity.bitChoiceData_correct line 161

    Source documentation

    The finite unary tables implement SAT gluing, including empty clauses and empty groups; no promise of nonempty domains is introduced.

    theorem bitChoiceData_correct {t : ℕ} (Q : Fin t → BitFormula) (d : ℕ)
    (hd : ∀ i, (names (Q i)).length≤d) :
    (bitChoiceData Q d).system.Successful ↔ ∃ a : Name → Bool, ∀ i, bitSat a (Q i) := by
…

    Mentions: OAI.ParityWL.Complexity.BitFormula, OAI.ParityWL.Complexity.names, OAI.ParityWL.Complexity.bitChoiceData, OAI.ParityWL.Complexity.Name, OAI.ParityWL.Complexity.bitSat