Sensitivity separation: recursive

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Recursive.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.recursive_four_recurrences {M r h : ℕ} {I : Type} [Fintype I] (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (hr : 0 < r) : have P := recursiveFamily T.toTournament A.label F; sideSensitivity P true ≤ M ^ 2 * sideSensitivity F false + r * sideSensitivity F true ∧ jointSensitivity P true ≤ M ^ 2 * jointSensitivity F false + r * sideSensitivity F true ∧ sideSensitivity P false ≤ 16 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true ∧ jointSensitivity P false ≤ 16 * sideSensitivity F false + 3 * jointSensitivity F true