comparison_sort_decision_tree_height_ge
theoremverified
If a binary decision tree has at least n! leaves, then 2^(height) >= n!, establishing the comparison sorting lower bound.
Statement
theorem comparison_sort_decision_tree_height_ge {α : Type*} (t : BinaryTree α) (n : ℕ) (h : n.factorial ≤ t.numLeaves) : n.factorial ≤ 2 ^ t.height
- Verified
- 06 Sep 2026
- Axioms
Quot.soundpropext- Built on 1
- binary_tree_num_leaves_le_pow_heightThe number of leaves of any binary tree is at most 2 raised to its height.
- Used by 1
- comparison_sort_height_ge_half_n_logb_half_nFor every type α, every binary tree t over α, and every natural number n, if n! ≤ t.numLeaves and 2 ≤ n, then (n/2)·log₂(n/2) ≤ t.height.…
Lean source view module on GitHub
/-- Any decision tree capable of distinguishing n! permutations has height at least log_2(n!). -/ theorem comparison_sort_decision_tree_height_ge {α : Type*} (t : BinaryTree α) (n : ℕ) (h : n.factorial ≤ t.numLeaves) : n.factorial ≤ 2 ^ t.height := h.trans (binary_tree_num_leaves_le_pow_height t)