OAI/Combinatorics/LowSpaceSubsetSum/Counting/MixerParameterCount.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact integer mixer parameters from small stored half lists

The count streams all pair occurrences, removing adjacent equal sum keys with constant extra state. Neither the distinct-sum set nor the full mixer powerset is stored. The count therefore feeds the integer ordering and prime-width formulas without a real-valued oracle.

  1. def OAI.LowSpaceSubsetSum.MixerParameterCount.sortedWeights line 19
  2. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.sortedWeights_sorted line 22
  3. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.sortedWeights_mem line 31
  4. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.sortedWeights_size line 37
  5. def OAI.LowSpaceSubsetSum.MixerParameterCount.count line 42
  6. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.count_value line 45
  7. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.count_queries line 63
  8. def OAI.LowSpaceSubsetSum.MixerParameterCount.firstHalf line 68
  9. def OAI.LowSpaceSubsetSum.MixerParameterCount.secondHalf line 71
  10. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.firstHalf_subset line 73
  11. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.firstHalf_card line 78
  12. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.halves_union line 83
  13. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.halves_disjoint line 86
  14. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.secondHalf_card line 89
  15. def OAI.LowSpaceSubsetSum.MixerParameterCount.mixerCount line 95

    Source documentation

    This function is determined entirely by the input and the permuted mixer domain; a designated solution is not an argument.

    def mixerCount (a : Fin n → ℤ) (V : Finset (Fin n)) : ℕ × ℕ :=
…
  16. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.mixerCount_value line 98
  17. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.mixerCount_queries line 102
  18. theorem OAI.LowSpaceSubsetSum.MixerParameterCount.mixerCount_footprint line 110

    Source documentation

    Every possible live state of the count uses only half-mixer arrays and a tournament of half-mixer rows.

    theorem mixerCount_footprint (a : Fin n → ℤ) (V : Finset (Fin n))
    (hc : V.card = mixerSize n)
    (s : SumReader.State (sortedWeights a (firstHalf V)) (sortedWeights a (secondHalf V))) :
    SumReader.footprint _ _ s ≤ 42 * 2 ^ (mixerSize n / 2) + 43 := by
…

    Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.SumReader.State, OAI.LowSpaceSubsetSum.MixerParameterCount.sortedWeights, OAI.LowSpaceSubsetSum.MixerParameterCount.firstHalf, OAI.LowSpaceSubsetSum.MixerParameterCount.secondHalf, OAI.LowSpaceSubsetSum.SumReader.footprint