HighDepthProp

formal source

 105
 106/-- The **high depth property**: f has false-point fraction ≥ τ.
 107    For τ > 1 this is impossible (fraction ≤ 1), so the property is empty. -/
 108def HighDepthProp (tau : ℝ) : ComplexityProperty :=
 109  fun n f => FalsePointFraction f ≥ tau
 110
 111/-- **THEOREM: For τ > 1, no function satisfies HighDepthProp.**
 112    This is immediate from `falsePointFraction_le_one`. -/
 113theorem high_depth_empty {n : ℕ} (tau : ℝ) (htau : 1 < tau)
 114    (f : (Fin n → Bool) → Bool) : ¬ HighDepthProp tau n f := by
 115  unfold HighDepthProp
 116  push_neg
 117  exact lt_of_le_of_lt (falsePointFraction_le_one f) htau
 118
 119/-- **THEOREM: For τ > 1, high depth is not large.**
 120    An empty property trivially fails the largeness count. -/
 121theorem high_depth_not_large (tau : ℝ) (htau : 1 < tau) :
 122    IsLarge (HighDepthProp tau) → False := by
 123  intro ⟨k, dec, hcount⟩
 124  -- For n = 1: the filter is empty (no function satisfies the property)
 125  have h1 := hcount 1 (by norm_num)
 126  -- Every function fails HighDepthProp tau when tau > 1
 127  have hempty : (Finset.univ.filter (fun f : (Fin 1 → Bool) → Bool =>
 128      @decide (HighDepthProp tau 1 f) (dec 1 f))).card = 0 := by
 129    rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
 130    intro f _
 131    simp only [decide_eq_true_eq]
 132    exact high_depth_empty tau htau f
 133  -- So 0 * 1^k ≥ |all truth tables| = 2^2 = 4
 134  rw [hempty, zero_mul] at h1
 135  have hpos : 0 < Finset.univ.card (α := (Fin 1 → Bool) → Bool) := by
 136    exact Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
 137  omega
 138