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