HighDepthProp
High depth property assigns to each real tau a complexity property on Boolean functions requiring false-point fraction at least tau. Researchers on natural proofs and circuit lower bounds cite it to exhibit an empty property for tau exceeding one. The definition is a direct functional wrapper around the false-point fraction comparison.
claimLet $tau in mathbb{R}$. The high-depth property $mathrm{HighDepthProp}(tau)$ is the complexity property $P$ such that for each arity $n$ and Boolean function $f: (mathrm{Fin} n to mathrm{Bool}) to mathrm{Bool}$, $P(n,f)$ holds precisely when the false-point fraction of $f$ satisfies $mathrm{FalsePointFraction}(f) geq tau$.
background
A complexity property maps each arity $n$ and truth table to a proposition, per the definition of ComplexityProperty. The false-point fraction of a Boolean function is $|f^{-1}(mathrm{false})| / 2^n$, the direct analog of landscape depth without going through CNF. This sits inside the Non-Naturalness module's treatment of Razborov-Rudich natural proofs, which require a property to be constructive, large (fraction at least $1/n^k$ of truth tables), and useful (implying no poly-size circuits).
proof idea
The definition is a one-line wrapper that applies the false-point fraction predicate directly to the input function.
why it matters in Recognition Science
This definition supplies the high-depth property used in high_depth_empty to show emptiness for tau > 1, in high_depth_not_large to prove failure of largeness, and ultimately in jfrust_not_natural and NonNaturalnessCert to establish that J-frustration cannot support a natural proof and thereby bypasses the Razborov-Rudich barrier. It fills the candidate property role in the module's complexity analysis.
scope and limits
- Does not assert that the property is large for any tau.
- Does not claim constructiveness or usefulness of the property.
- Does not apply outside Boolean functions on finite domains.
- Does not provide any bounds or behavior for tau less than or equal to one.
formal statement (Lean)
108def HighDepthProp (tau : ℝ) : ComplexityProperty :=
proof body
Definition body.
109 fun n f => FalsePointFraction f ≥ tau
110
111/-- **THEOREM: For τ > 1, no function satisfies HighDepthProp.**
112 This is immediate from `falsePointFraction_le_one`. -/