Sensitivity separation: recursive joint zero

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveJointZero.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_joint_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 q' : Fin h) (hqq : q < q') (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T A.label F q x = false) (hx' : recursiveFamily T A.label F q' x = false) : jointSensitivityAt (recursiveFamily T A.label F q) (recursiveFamily T A.label F q') x ≤ 16 * sideSensitivity F false + 3 * jointSensitivity F true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_joint_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) : jointSensitivity (recursiveFamily T A.label F) false ≤ 16 * sideSensitivity F false + 3 * jointSensitivity F true