Sensitivity separation: labeling

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Labeling.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.goodLabeling_exists_of_power_bound {k r : ℕ} (T : Tournament k) (hr : 0 < r) (hN : 120 ≤ k * k) (hkr : k ^ 16 < r ^ 104) : Nonempty (GoodLabeling T r)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.goodLabeling_exists {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) (T : Tournament (2 * M ^ 2 + 1)) : Nonempty (GoodLabeling T r)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.regular_goodLabeling_exists {M : ℕ} (hM : 3 ≤ M) : Nonempty (GoodLabeling (regularCyclicTournament M).toTournament ⌈√↑M⌉₊)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.GoodLabeling.good_on_subset {k r : ℕ} {T : Tournament k} (A : GoodLabeling T r) (I : Finset (Fin k)) (hI : I.card = 16) (m : ↥I → Fin r) : ∃ i ∈ I, ∃ (j : Fin k) (hj : j ∈ I), T.Adj i j ∧ A.label i j ≠ m ⟨j, hj⟩