kahn_kalai_threshold

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result kahn_kalai_threshold is named for, so its Disproved status carries no information about it. Do not import it or use it as a dependency.

Kahn–Kalai conjecture (proved by Park–Pham 2022): For any monotone Boolean function, the threshold probability is within a log factor of the expectation threshold. Proves a long-standing conjecture in probabilistic combinatorics with applications to random graphs and hypergraphs.

Why this node was retired

The posted statement is

import Mathlib

theorem kahn_kalai_threshold (n : ℕ) (hn : 1 ≤ n)
    (property : Finset (Fin n) → Prop)
    (hmono : ∀ A B : Finset (Fin n), A ⊆ B → property A → property B)
    (q_E : ℝ) (hqE : 0 < q_E ∧ q_E < 1)
    (hexpect : ∀ p : ℝ, 0 < p → p < 1 →
      (∀ A : Finset (Fin n), p ^ A.card * (1-p) ^ (n - A.card) = 1 / n) →
      True) :
    ∃ p_thresh : ℝ, p_thresh ≤ q_E * Real.log n ∧ 0 < p_thresh := by
  sorry

The hypothesis hexpect ends in → True, so it assumes nothing. The conclusion ∃ p_thresh, p_thresh ≤ q_E * Real.log n ∧ 0 < p_thresh fails at n = 1, where Real.log 1 = 0 forces 0 < p_thresh ≤ 0 — hence the Disproved status, which is an artifact of the encoding rather than a statement about the Kahn–Kalai theorem.

What a faithful statement would require

The expectation threshold q(F) and the critical probability p_c(F) must be defined from the monotone property, and the conclusion must be p_c(F) ≤ C · q(F) · log ℓ(F) with the constant quantified correctly.

No corrected replacement node exists yet.