IsConstructive

formal source

  88    Finset.univ.card (α := (Fin n → Bool) → Bool)
  89
  90/-- A property is constructive if decidable. -/
  91structure IsConstructive (P : ComplexityProperty) where
  92  dec : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, Decidable (P n f)
  93
  94/-- A property is useful if it implies hardness. -/
  95structure IsUseful (P : ComplexityProperty) where
  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) :