high_depth_not_large
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.