MachineUniformCopyOrder.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

An exact ordering bridge for uniform copies.

Largest-remainder output groups copies of each occurrence together. A fixed whole-word copying machine instead repeats the entire occurrence list. These lists are permutations, not equal serializations. The permutation preserves every selected occurrence count and the target's actual countSatisfied.

def OAI.UniqueGamesTheorem.MachineUniformCopyOrder.occurrenceMajor line 19
def OAI.UniqueGamesTheorem.MachineUniformCopyOrder.copyMajor line 22
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.occurrenceMajor_perm_copyMajor line 25
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.selected_count_eq line 37
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.mem_iff line 43
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.copyMajor_selected_count line 47
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.occurrenceMajor_selected_count line 58
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.encoded_rows_perm line 65
Source documentation
Encoded rows retain their multiplicities; this does not identify concatenated bitstreams in two different occurrence orders.
```
theorem encoded_rows_perm {α β : Type*} (C : Nat) (edges : List α)
    (encode : α → List β) :
    ((occurrenceMajor C edges).map encode).Perm ((copyMajor C edges).map encode) :=
…
```
Mentions: OAI.UniqueGamesTheorem.MachineUniformCopyOrder.occurrenceMajor, OAI.UniqueGamesTheorem.MachineUniformCopyOrder.copyMajor
theorem OAI.UniqueGamesTheorem.MachineUniformCopyOrder.countSatisfied_eq line 73
Source documentation
The actual finite-target satisfaction counter is unaffected by the reorder.
```
theorem countSatisfied_eq {n q : Nat} (C : Nat)
    (edges : List (Constraint n q)) (labeling : Fin n → Fin q) :
    countSatisfied labeling (occurrenceMajor C edges) =
      countSatisfied labeling (copyMajor C edges) :=
…
```
Mentions: OAI.UniqueGamesTheorem.MachineUniformCopyOrder.occurrenceMajor, OAI.UniqueGamesTheorem.MachineUniformCopyOrder.copyMajor