Sensitivity separation: construction

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Construction.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.BooleanAnalysis.Sensitivity.Internal.constructionBase (d M h : ℕ) (q : Fin h) (x : Fin M × Fin (d + 2) → Bool) : Bool

Extend the initial Hamming-ball predicates to all index counts.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.Sensitivity.Internal.ConstructionCoordinates (d M r n : ℕ) : Type

Coordinates for the regular-tournament construction at a given level.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.ConstructionCoordinates d M r n = Complexity.BooleanAnalysis.Sensitivity.Internal.TowerCoordinates (2 * M ^ 2 + 1) r (Fin M × Fin (d + 2)) n

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.terminalPredicate {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (ConstructionCoordinates d M r d → Bool) → Bool

The single remaining predicate after all recursive levels.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.construction_base_nested (d M : ℕ) : NestedFamily (constructionBase d M (d + 1))

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.construction_base_zero (d M : ℕ) (q : Fin (1 + d)) : (constructionBase d M (1 + d) q fun (x : Fin M × Fin (d + 2)) => false) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.construction_base_blocks (d M : ℕ) (b : Fin M) (q : Fin (1 + d)) : constructionBase d M (1 + d) q (flip (fun (x : Fin M × Fin (d + 2)) => false) (baseBlock b)) = true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.terminalPredicate_zero {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : (terminalPredicate d T A fun (x : ConstructionCoordinates d M r d) => false) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.terminalPredicate_blocks {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) (b : TowerBlockIndex (2 * M ^ 2 + 1) (Fin M) d) : terminalPredicate d T A (flip (fun (x : ConstructionCoordinates d M r d) => false) (towerBlocks baseBlock d b)) = true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.terminalPredicate_blockSensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : M * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt (terminalPredicate d T A) fun (x : ConstructionCoordinates d M r d) => false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.construction_profiles {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) (n : ℕ) : n ≤ d → towerSide T.toTournament A.label (constructionBase d M) (d + 1) n false ≤ 2 * (d + 2) * M ^ n ∧ towerSide T.toTournament A.label (constructionBase d M) (d + 1) n true ≤ 2 * (d + 2) * M ^ (n + 1)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.terminalPredicate_sensitivityAt {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) : (∀ (x : ConstructionCoordinates d M r d → Bool), terminalPredicate d T A x = false → sensitivityAt (terminalPredicate d T A) x ≤ 2 * (d + 2) * M ^ d) ∧ ∀ (x : ConstructionCoordinates d M r d → Bool), terminalPredicate d T A x = true → sensitivityAt (terminalPredicate d T A) x ≤ 2 * (d + 2) * M ^ (d + 1)

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.finalBoolean {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (Fin M × ConstructionCoordinates d M r d → Bool) → Bool

Disjoin M independent copies of the terminal predicate.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalBoolean_zero {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : (finalBoolean d T A fun (x : Fin M × ConstructionCoordinates d M r d) => false) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalBoolean_sensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) : sensitivity (finalBoolean d T A) ≤ 2 * (d + 2) * M ^ (d + 1)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalBoolean_blockSensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt (finalBoolean d T A) fun (x : Fin M × ConstructionCoordinates d M r d) => false

def Complexity.BooleanAnalysis.Sensitivity.Internal.constructionDimension (d M r : ℕ) : ℕ

Number of coordinates of the final Boolean function.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.constructionDimension d M r = (d + 2) * M ^ 2 * ((2 * M ^ 2 + 1) * r) ^ d

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.final_coordinates_card (d M r : ℕ) : Fintype.card (Fin M × ConstructionCoordinates d M r d) = constructionDimension d M r

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.finalWitness {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (Fin (constructionDimension d M r) → Bool) → Bool

Reindex the final Boolean function onto an ordinary finite Boolean cube.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalWitness_zero {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : (finalWitness d T A fun (x : Fin (constructionDimension d M r)) => false) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalWitness_sensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) : sensitivity (finalWitness d T A) ≤ 2 * (d + 2) * M ^ (d + 1)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.finalWitness_blockSensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt (finalWitness d T A) fun (x : Fin (constructionDimension d M r)) => false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.constructionDimension_pos {d M r : ℕ} (hM : 0 < M) (hr : 0 < r) : 0 < constructionDimension d M r