IsUseful
plain-language theorem explainer
IsUseful marks a complexity property P as useful when P(n,f) implies circuit hardness for the satisfying Boolean functions f. Researchers analyzing natural proofs barriers cite it to check whether J-frustration properties can establish lower bounds without triggering Razborov-Rudich. The structure is a direct one-field definition encoding the implication, with no lemmas or tactics required.
Claim. A complexity property $P$ is useful when, for every arity $n$ and every Boolean function $f$ of arity $n$, satisfaction of $P(n,f)$ implies that $f$ has no polynomial-size circuits.
background
The Non-Naturalness module formalizes the Razborov-Rudich 1997 natural proofs barrier for circuit lower bounds. A ComplexityProperty is a predicate assigning to each arity $n$ and truth table a proposition; it serves as the base type for the three conditions of a natural proof. The module states that a natural property must be constructive (poly-time computable), large (holds for a $1/n^k$ fraction of functions), and useful (implies no poly-size circuits). IsUseful supplies the usefulness component of this triple.
proof idea
The declaration is a structure definition whose single field directly encodes the usefulness implication. No upstream lemmas are invoked and no tactics are used; it functions as a type-level marker for the hardness condition.
why it matters
IsUseful completes the IsNatural structure, which is invoked by jfrust_not_natural to obtain a contradiction for high-depth properties with false-point fraction exceeding 1. This shows that J-frustration (derived from the J-cost Laplacian) evades the natural-proofs barrier, allowing RS-derived measures to target circuit lower bounds. The result aligns with the module's goal of demonstrating that high-depth J-frustration properties are non-natural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.