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.MaxCutGames.MachineUniformCopyOrder.occurrenceMajor line 17
def OAI.MaxCutGames.MachineUniformCopyOrder.copyMajor line 20
theorem OAI.MaxCutGames.MachineUniformCopyOrder.occurrenceMajor_perm_copyMajor line 23
theorem OAI.MaxCutGames.MachineUniformCopyOrder.selected_count_eq line 35
theorem OAI.MaxCutGames.MachineUniformCopyOrder.mem_iff line 41
theorem OAI.MaxCutGames.MachineUniformCopyOrder.copyMajor_selected_count line 45
theorem OAI.MaxCutGames.MachineUniformCopyOrder.occurrenceMajor_selected_count line 56
theorem OAI.MaxCutGames.MachineUniformCopyOrder.encoded_rows_perm line 63
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.MaxCutGames.MachineUniformCopyOrder.occurrenceMajor, OAI.MaxCutGames.MachineUniformCopyOrder.copyMajor
theorem OAI.MaxCutGames.MachineUniformCopyOrder.countSatisfied_eq line 71
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.MaxCutGames.MachineUniformCopyOrder.occurrenceMajor, OAI.MaxCutGames.MachineUniformCopyOrder.copyMajor