OAI/NumberTheory/TwoPoint/Circuits/CircuitWalkCode.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of the switching encoding. Earlier incompatible terms stay incompatible, while the first queried term becomes compatible in the image. The first block and its responses can therefore be decoded and removed.

  1. lemma OAI.TwoPointCorrelations.DNFQueryBlock.codes_cons line 17
  2. lemma OAI.TwoPointCorrelations.DNFQueryBlock.codes_eq_nil_iff line 21
  3. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.codes_length_le line 30
  4. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.code_positions_le line 43
  5. theorem OAI.TwoPointCorrelations.CanonicalDNFWalk.image_code_injective line 67