Sensitivity separation: seed amplification

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/SeedAmplification.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.constructed_power_family : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → (Fin (n m) → Bool) → Bool), (∀ (m : ℕ), 0 < n m ∧ (F m fun (x : Fin (n m)) => false) = false ∧ (∃ (x : Fin (n m) → Bool) (y : Fin (n m) → Bool), F m x ≠ F m y) ∧ ↑(sensitivity (F m)) ^ α ≤ ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false) ∧ (128 / 121) ^ m ≤ ↑(blockSensitivity (F m)) / ↑(sensitivity (F m)) ^ 2) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) Filter.atTop Filter.atTop