Sensitivity separation: recursive zero

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveZero.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_sensitivity_zero_at {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (hr : 0 < r) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T A.label F q x = false) : sensitivityAt (recursiveFamily T A.label F q) x ≤ 16 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_side_zero {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (hr : 0 < r) : sideSensitivity (recursiveFamily T A.label F) false ≤ 16 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true