HighDepthProp
plain-language theorem explainer
HighDepthProp(τ) is the complexity property asserting that a Boolean function has false-point fraction at least τ. Researchers on natural proofs and circuit lower bounds cite it to demonstrate that depth-based properties fail the largeness condition of Razborov-Rudich when τ exceeds 1. The definition is a one-line wrapper that applies the FalsePointFraction predicate directly.
Claim. Let $P_τ$ be the complexity property such that for each arity $n$ and Boolean function $f: (Fin n → Bool) → Bool$, $P_τ(n,f)$ holds precisely when the false-point fraction of $f$ satisfies $|f^{-1}(false)| / 2^n ≥ τ$.
background
A ComplexityProperty is any map sending arity n and a truth table to a proposition. FalsePointFraction of f is the direct proportion |f^{-1}(false)| / 2^n, the landscape-depth analog without CNF encoding. The module studies non-naturalness of J-frustration against the Razborov-Rudich criteria (constructive, large, useful) for natural proofs that would separate NP from P/poly.
proof idea
The definition is a one-line wrapper that applies FalsePointFraction and compares the result to tau.
why it matters
HighDepthProp supplies the predicate used by high_depth_empty, high_depth_not_large, and jfrust_not_natural. Those results show that for τ > 1 the property is empty and therefore cannot be large, yielding the barrier-bypass claim inside NonNaturalnessCert. This places the definition inside the Recognition Science treatment of J-frustration as a non-natural property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.