Sensitivity separation: labeling bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/LabelingBounds.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.le_ceil_sqrt_sq (M : ℕ) : M ≤ ⌈√↑M⌉₊ ^ 2

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_space_large {M : ℕ} (hM : 3 ≤ M) : 120 ≤ (2 * M ^ 2 + 1) * (2 * M ^ 2 + 1)