SelectorCommonWitness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

One witness for an entire selector profile group

A nonempty group contains an actual selected move, hence an actual feasible family member. Its admissibility tests depend on the original coloring only through the full profile. Maximizing each cutoff for this one member therefore produces common heavy sets for the entire group. Selected-move minimality puts every moved row inside its corresponding common heavy set.

structure OAI.TalagrandThreshold.Selector.CommonWitness line 26
Source documentation
The same actual family member and cutoffs work for every original coloring in a fixed final-coloring/profile group.
```
structure CommonWitness {F : Family α} (mu : MassFamily F) {s : ℕ}
    (z : Coloring α s) (n : Profile s) where
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile
theorem OAI.TalagrandThreshold.Selector.card_le_profile_of_truncation line 42
theorem OAI.TalagrandThreshold.Selector.exists_common_witness line 58
Source documentation
The common witness is constructed from the actual nonempty group; no additional feasibility, reconstruction, or cardinality certificate is assumed.
```
theorem exists_common_witness {F : Family α} (mu : MassFamily F) {s : ℕ}
    (z : Coloring α s) (n : Profile s)
    (hne : (groupOriginals mu z n).Nonempty) : Nonempty (CommonWitness mu z n) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.groupOriginals, OAI.TalagrandThreshold.Selector.CommonWitness
theorem OAI.TalagrandThreshold.Selector.exists_common_heavy_sets line 109
Source documentation
The finite sets needed for counting are common to the whole actual group.
```
theorem exists_common_heavy_sets {F : Family α} (mu : MassFamily F) {s : ℕ}
    (z : Coloring α s) (n : Profile s)
    (hne : (groupOriginals mu z n).Nonempty) :
    ∃ R : Fin s → Finset α,
      (∀ i, (R i).card ≤ 2 ^ (i.val + 1) * profileSize n) ∧
      ∀ a ∈ groupOriginals mu z n, ∀ i, movedRow a z i ⊆ R i := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.groupOriginals, OAI.TalagrandThreshold.Selector.profileSize, OAI.TalagrandThreshold.Selector.movedRow