high_depth_empty
No Boolean function on n variables has false-point fraction at least tau when tau exceeds 1. Complexity theorists working on natural proofs cite this to show the high-depth property is empty and therefore fails the largeness condition in the Razborov-Rudich framework. The term-mode proof unfolds the property definition and applies the false-point fraction upper bound together with lt_of_le_of_lt.
claimFor every natural number $n$, every real number $tau > 1$, and every Boolean function $f : (Fin n → Bool) → Bool$, the false-point fraction of $f$ satisfies FalsePointFraction($f$) < $tau$.
background
The module develops non-naturalness results for J-frustration properties in the sense of Razborov-Rudich 1997. A natural proof requires a property that is constructive (poly-time decidable), large (holds for at least a 1/poly(n) fraction of all 2^{2^n} functions), and useful (implies no poly-size circuits). HighDepthProp tau is the ComplexityProperty that selects those functions whose false-point fraction (the measure of inputs where f evaluates to false) meets or exceeds the threshold tau. The upstream lemma falsePointFraction_le_one proves that this fraction is at most 1 for any f.
proof idea
The proof is a one-line term wrapper. It unfolds HighDepthProp to obtain the negated goal FalsePointFraction f < tau, invokes falsePointFraction_le_one to recover the bound ≤ 1, and closes with lt_of_le_of_lt using the hypothesis 1 < tau.
why it matters in Recognition Science
The declaration is invoked by high_depth_not_large, which shows that HighDepthProp tau fails IsLarge when tau > 1. This step completes the module argument that high-depth J-frustration properties are not natural, so the Razborov-Rudich barrier does not obstruct circuit lower bounds derived from the J-cost framework. It directly supports the claim that certain Recognition Science complexity properties evade the natural-proof obstruction.
scope and limits
- Does not establish emptiness or non-emptiness for tau ≤ 1.
- Does not address constructiveness or usefulness of the property.
- Does not apply to infinite domains or non-Boolean functions.
- Does not yield any quantitative bound stricter than the trivial fraction ≤ 1.
formal statement (Lean)
113theorem high_depth_empty {n : ℕ} (tau : ℝ) (htau : 1 < tau)
114 (f : (Fin n → Bool) → Bool) : ¬ HighDepthProp tau n f := by
proof body
Term-mode proof.
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. -/