high_depth_not_large
For real tau greater than 1, the property that a Boolean function has false-point fraction at least tau cannot be large. Complexity theorists studying natural-proof barriers would cite this to exclude high-depth properties from arguments that rely on largeness. The proof is a direct counting argument that specializes the IsLarge bound to n=1, invokes emptiness of the property, and derives 0 greater than or equal to 4.
claimLet $tau > 1$. Let $P$ be the property on Boolean functions defined by $P(n,f)$ holding precisely when the false-point fraction of $f$ is at least $tau$. If $P$ is large, i.e., there exists a natural number $k$ such that for every $n>0$ the number of $n$-ary truth tables satisfying $P$ is at least $2^{2^n}/n^k$, then a contradiction follows.
background
Natural proofs require a property that is constructive, large, and useful; largeness means the property holds for at least a $1/n^k$ fraction of all $n$-ary truth tables. HighDepthProp(tau) is the property that the false-point fraction of a Boolean function is at least tau. IsLarge(P) packages an explicit counting bound together with a decidability witness for P.
proof idea
Assume IsLarge(HighDepthProp tau). Specialize the count_bound clause to n=1 to obtain that the filtered count times 1^k is at least 4. Apply high_depth_empty to show that the filter over all four functions is empty, so the count is zero. Rewrite with zero_mul and obtain the numerical contradiction 0 greater than or equal to 4, which omega discharges.
why it matters in Recognition Science
The result is invoked inside jfrust_not_natural to conclude that HighDepthProp cannot be natural when tau exceeds 1, thereby showing that the Razborov-Rudich barrier does not apply to J-frustration. It supplies the concrete step that high depth fails the largeness requirement inside the natural-proof definition. In the Recognition Science setting this supports the broader claim that J-frustration lies outside the natural-proof regime.
scope and limits
- Does not address the case tau less than or equal to 1.
- Does not speak to constructiveness or usefulness of the property.
- Applies only to HighDepthProp and not to other candidate properties.
- Does not refute the Razborov-Rudich theorem itself.
- Uses only the explicit counting definition of largeness given in the module.
formal statement (Lean)
121theorem high_depth_not_large (tau : ℝ) (htau : 1 < tau) :
122 IsLarge (HighDepthProp tau) → False := by
proof body
Tactic-mode proof.
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
139/-- **THEOREM (Barrier Bypass).**
140 High depth (τ > 1) cannot be the basis of a natural proof. -/