OAI/NumberTheory/TwoPoint/Bounds/IntegerPathProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Separate the copy, block, and endpoint gates from the signed arithmetic edge product along an actual forced matrix path.

  1. def OAI.TwoPointCorrelations.integerStepMask line 14
  2. def OAI.TwoPointCorrelations.integerPathMask line 20
  3. lemma OAI.TwoPointCorrelations.integerPathMask_zero_or_one line 28
  4. lemma OAI.TwoPointCorrelations.retained_integerShiftWeight_eq_mask line 43
  5. theorem OAI.TwoPointCorrelations.integerShiftWord_eq_mask_product line 61
  6. theorem OAI.TwoPointCorrelations.integerShiftWord_pair_product line 80