high_depth_empty
plain-language theorem explainer
For τ > 1 the high-depth property (false-point fraction at least τ) holds for no Boolean function on any number of variables. Researchers studying natural proofs against circuit lower bounds cite this to establish that the property is empty and thus fails the largeness requirement of Razborov-Rudich. The proof is a direct application of the upper bound false-point fraction ≤ 1 combined with the strict inequality τ > 1.
Claim. Let $F(f)$ denote the false-point fraction of a Boolean function $f$. Then for every natural number $n$, every real number $τ > 1$, and every function $f : (Fin n → Bool) → Bool$, it holds that $F(f) < τ$.
background
The module examines non-naturalness of J-frustration in the sense of Razborov-Rudich 1997: a natural proof needs a property that is constructive, large (fraction at least 1/poly(n)), and useful for circuit lower bounds. HighDepthProp tau is the ComplexityProperty that selects functions whose false-point fraction meets or exceeds tau. The upstream result falsePointFraction_le_one states that this fraction is at most 1 for any f. MODULE_DOC records that the module contains zero sorry and zero axiom.
proof idea
The term proof unfolds HighDepthProp to the inequality FalsePointFraction f ≥ tau, pushes the negation, and invokes lt_of_le_of_lt on the lemma falsePointFraction_le_one together with the hypothesis 1 < tau.
why it matters
high_depth_not_large applies this result to conclude that HighDepthProp tau fails the largeness count when tau > 1. The declaration therefore supplies the emptiness step needed to show that high depth is not a natural property, so the Razborov-Rudich barrier does not block lower bounds obtained from J-frustration. The downstream doc-comment notes that an empty property trivially fails the largeness count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.