IsNatural
IsNatural packages a complexity property as natural when it is simultaneously constructive, large, and useful. Circuit complexity researchers cite the definition when classifying candidate properties for natural proofs against the Razborov-Rudich barrier. The declaration is a structure definition that directly bundles the three component structures.
claimA complexity property $P$ is natural if it is constructive (decidable for every arity $n$ and truth table), large (at least a $1/n^k$ fraction of $n$-ary truth tables satisfy $P$ for some fixed $k$), and useful (satisfying $P$ implies a circuit lower bound).
background
The module formalizes the Razborov-Rudich natural proof barrier for J-frustration. ComplexityProperty is the type of predicates that take an arity $n$ and a Boolean function on $n$ variables to a proposition. IsConstructive requires that the predicate is decidable for each $n$ and function. IsLarge requires a counting bound: the number of satisfying truth tables is at least $1/n^k$ of the total $2^{2^n}$ tables for some fixed $k$. IsUseful requires that the predicate implies hardness, encoded here as an implication to the trivial proposition True.
proof idea
This is a structure definition. It introduces three fields that directly reference the structures IsConstructive, IsLarge, and IsUseful; no lemmas or tactics are invoked.
why it matters in Recognition Science
IsNatural serves as the target type in jfrust_not_natural, which shows that HighDepthProp with threshold greater than 1 cannot be natural because it fails largeness. The result establishes that J-frustration bypasses the natural-proof barrier, so the Razborov-Rudich theorem does not obstruct circuit lower bounds derived from it. The definition therefore closes one step in the non-naturalness argument for the complexity properties arising in Recognition Science.
scope and limits
- Does not assert existence of any natural property for a concrete complexity class.
- Does not supply a non-trivial circuit lower bound inside the useful component.
- Does not treat properties of functions outside finite-arity Boolean functions.
- Does not constrain the exponent $k$ appearing in the largeness count bound.
formal statement (Lean)
99structure IsNatural (P : ComplexityProperty) where
100 constructive : IsConstructive P
101 large : IsLarge P
102 useful : IsUseful P
103
104/-! ## High-Depth Property -/
105
106/-- The **high depth property**: f has false-point fraction ≥ τ.
107 For τ > 1 this is impossible (fraction ≤ 1), so the property is empty. -/