OAI/Computability/UniqueGames/Machines/MachineUniformRounding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual largest-remainder routine on a uniform occurrence distribution.

For h > 0 occurrences, each weight has numerator one and denominator h. Choosing tolerance 1 / C gives Q = C * h. Every quota is the integer C, so the sorting order is immaterial: there is no deficit to allocate. The exact output list contains C copies of each original occurrence, in original order.

This is a conditional specialization of the rounding algorithm. It does not assert that a particular preceding matrix reduction produces uniform weights, nor does it assert a runtime certificate for a general sorting algorithm.

  1. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.denominator_uniform line 25
  2. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.denominator_uniform_eq_ceil line 29
  3. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.uniform_mass line 34
  4. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.scaled_quota_uniform line 36
  5. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.floorCount_uniform line 43
  6. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.remainder_uniform line 47
  7. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.deficit_uniform line 51
  8. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.incremented_uniform line 56
  9. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.count_uniform line 61

    Source documentation

    The concrete largest-remainder multiplicity is precisely C.

    theorem count_uniform (h C : Nat) (hh : 0 < h) (i : Fin h) :
    count (denominator h 1 C) h (fun _ => 1) i = C := by
…
  10. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.copies_uniform line 66
  11. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.copies_uniform_length line 71
  12. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.normalized_count_uniform line 76

    Source documentation

    Each normalized rounded weight equals its original uniform weight exactly.

    theorem normalized_count_uniform (h C : Nat) (hh : 0 < h) (hC : 0 < C)
    (i : Fin h) :
    (count (denominator h 1 C) h (fun _ => 1) i : ℚ) /
      denominator h 1 C = 1 / (h : ℚ) := by
…
  13. theorem OAI.UniqueGamesTheorem.MachineUniformRounding.selected_weights_exact line 87

    Source documentation

    Therefore every satisfaction predicate has zero rounding error.

    theorem selected_weights_exact (h C : Nat) (hh : 0 < h) (hC : 0 < C)
    (keep : Fin h → Bool) :
    (∑ i, if keep i then
      (count (denominator h 1 C) h (fun _ => 1) i : ℚ) / denominator h 1 C else 0) =
      ∑ i, if keep i then 1 / (h : ℚ) else 0 := by
…