IsLarge
plain-language theorem explainer
IsLarge encodes the largeness condition from natural proofs: a complexity property P of Boolean functions is large when the satisfying fraction is at least 1/n^k for fixed k. Circuit complexity researchers studying Razborov-Rudich barriers cite this when checking whether a property like high-depth frustration can yield natural proofs. The structure directly packages the integer k, a decidability witness, and the counting inequality over all n.
Claim. Let $P$ be a complexity property. Then $P$ is large if there exists $k$ such that $P(n,f)$ is decidable for every arity $n$ and every truth table $f$, and for every $n>0$ the number of $n$-ary Boolean functions satisfying $P$ is at least $2^{2^n}/n^k$.
background
ComplexityProperty is the type of maps sending arity $n$ and a truth table $(Fin n → Bool) → Bool$ to a proposition. The module sets this inside the Razborov-Rudich framework: a natural proof requires a property that is constructive (poly-time decidable), large (fraction at least 1/poly(n)), and useful (implies no poly-size circuits). IsLarge supplies the middle clause via an explicit counting lower bound.
proof idea
This is a structure definition that directly encodes the three components of largeness: the exponent k, the decidability predicate, and the counting lower bound. No lemmas are applied.
why it matters
IsLarge supplies the largeness component for IsNatural, which in turn is used to show that high-depth properties fail naturalness via high_depth_not_large. It implements the second requirement in the Razborov-Rudich natural proof definition within the J-frustration analysis, showing the RS barrier evades that obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.