IsNatural

formal source

  96  implies_lower_bound : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, P n f → True
  97
  98/-- A natural property is constructive + large + useful. -/
  99structure IsNatural (P : ComplexityProperty) where
 100  constructive : IsConstructive P
 101  large : IsLarge P
 102  useful : IsUseful P
 103
 104/-! ## High-Depth Property -/
 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]