Sensitivity separation: constructed seed

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/ConstructedSeed.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.construction_label_count_pos {M : ℕ} (hM : 0 < M) : 0 < ⌈√↑M⌉₊

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.exists_constructed_seed (d M : ℕ) (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ∃ (f : (Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool) → Bool), 0 < constructionDimension d M ⌈√↑M⌉₊ ∧ (f fun (x : Fin (constructionDimension d M ⌈√↑M⌉₊)) => false) = false ∧ (∃ (x : Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool) (y : Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool), f x ≠ f y) ∧ sensitivity f ≤ 2 * (d + 2) * M ^ (d + 1) ∧ M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt f fun (x : Fin (constructionDimension d M ⌈√↑M⌉₊)) => false