OAI/Combinatorics/LowSpaceSubsetSum/Counting/ResidueMatchAccounting.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Every potential Cartesian match is charged to one residue iteration

The calculation counts list occurrences, including repetitions. Summing the full potential over all residues counts every Cartesian pair exactly once. The complementary right-hand residue loop is the same finite sum after an explicit involutive reindexing.

  1. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.direct_match_iff line 21
  2. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.sum_filter_lengths line 27
  3. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.sum_potential line 40
  4. def OAI.LowSpaceSubsetSum.ResidueMatchAccounting.complement line 55
  5. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.complement_val line 58
  6. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.complement_involutive line 63
  7. def OAI.LowSpaceSubsetSum.ResidueMatchAccounting.complementEquiv line 69
  8. theorem OAI.LowSpaceSubsetSum.ResidueMatchAccounting.sum_complementary_potential line 72