OAI/NumberTheory/TwoPoint/Circuits/CircuitBlockCode.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A query block is encoded by positions within its term, the path answers, and one separator. Term indices are recovered from the modified restriction, so the code alphabet is independent of the number of terms.

  1. def OAI.TwoPointCorrelations.CubeTerm.slot line 14
  2. lemma OAI.TwoPointCorrelations.CubeTerm.slot_le line 18
  3. lemma OAI.TwoPointCorrelations.CubeTerm.slot_injective line 25
  4. def OAI.TwoPointCorrelations.DNFQueryBlock.literalCode line 34
  5. def OAI.TwoPointCorrelations.DNFQueryBlock.code line 37
  6. def OAI.TwoPointCorrelations.DNFQueryBlock.codes line 40
  7. lemma OAI.TwoPointCorrelations.DNFQueryBlock.code_length line 43
  8. lemma OAI.TwoPointCorrelations.DNFQueryBlock.literalCode_injective line 46
  9. lemma OAI.TwoPointCorrelations.separated_option_lists_injective line 74