Sensitivity separation: labeling constraints

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/LabelingConstraints.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.mem_internalEdges {k : ℕ} (T : Tournament k) {I : Finset (Fin k)} {p : Fin k × Fin k} : p ∈ T.internalEdges I ↔ (p.1 ∈ I ∧ p.2 ∈ I) ∧ T.Adj p.1 p.2

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.labelingConstraint_iff {k : ℕ} (T : Tournament k) {α β : Type} [Nonempty α] (s : Finset α) (v : α → Fin k) (m : α → β) (hv : Function.Injective v) (A : Fin k × Fin k → β) : (∀ i ∈ s, ∀ j ∈ s, T.Adj (v i) (v j) → A (v i, v j) = m j) ↔ ∀ p ∈ T.internalEdges (Finset.image v s), A p = m (Function.invFun v p.2)