OAI/NumberTheory/TwoPoint/Circuits/CircuitQueryWalk.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Complete query blocks along a canonical DNF path. A prefix of a path is enough for the switching encoding; the final Boolean answer is irrelevant.

  1. structure OAI.TwoPointCorrelations.DNFQueryBlock line 13
  2. def OAI.TwoPointCorrelations.DNFQueryBlock.support line 20
  3. def OAI.TwoPointCorrelations.DNFQueryBlock.length line 24
  4. def OAI.TwoPointCorrelations.DNFQueryBlock.image line 28
  5. inductive OAI.TwoPointCorrelations.CanonicalDNFWalk line 34
  6. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.support_subset_free line 45
  7. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.head_disjoint_tail line 59
  8. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.length_eq_card_support line 69
  9. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.length_le_dimension line 80