Sensitivity separation: quantitative profiles

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/QuantitativeProfiles.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.quantitative_profile_bounds (d L M r : ℕ) (hM : 0 < M) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) (S J : ℕ → Bool → ℕ) (hS₀ : S 0 false ≤ L) (hS₁ : S 0 true ≤ L * M) (hJ₀ : J 0 false = 0) (hJ₁ : J 0 true = 0) (hstepS₀ : ∀ n < d, S (n + 1) false ≤ 16 * S n false + S n true + 3 * J n true) (hstepS₁ : ∀ n < d, S (n + 1) true ≤ M ^ 2 * S n false + r * S n true) (hstepJ₀ : ∀ n < d, J (n + 1) false ≤ 16 * S n false + 3 * J n true) (hstepJ₁ : ∀ n < d, J (n + 1) true ≤ M ^ 2 * J n false + r * S n true) (n : ℕ) : n ≤ d → S n false ≤ 2 * L * M ^ n ∧ S n true ≤ 2 * L * M ^ (n + 1)