IsLarge
plain-language theorem explainer
IsLarge encodes the largeness condition for a complexity property P by requiring a fixed exponent k together with a decidability witness and a counting lower bound on the fraction of satisfying truth tables. Circuit-complexity researchers working on natural-proof barriers cite it when checking the density requirement in Razborov-Rudich-style arguments. The definition is a direct packaging of the three data fields that make the 1/n^k density statement precise and computable.
Claim. A complexity property $P$ is large when there exists $k$ in the natural numbers such that, for every $n>0$, the predicate $P(n,f)$ is decidable for every Boolean function $f$ on $n$ variables and the number of such $f$ satisfying $P(n,f)$ is at least $2^{2^n}/n^k$.
background
In this module a ComplexityProperty is any map that assigns to each arity $n$ and each truth table a proposition. The surrounding development studies natural proofs in the sense of Razborov-Rudich: a property must be constructive (decidable in polynomial time in the truth-table size), large, and useful (implying no small circuits). IsLarge supplies the middle requirement by turning the informal density statement into a structure that records an explicit exponent and a counting witness.
proof idea
The declaration is a plain structure definition. It packages the integer $k$, the decidability function dec, and the inequality that forces the filtered cardinality to be at least the total number of functions divided by $n^k$. No lemmas or tactics are invoked; the fields are simply the mathematical content of the largeness condition.
why it matters
IsLarge is one of the three conjuncts inside the IsNatural structure. It is invoked by high_depth_not_large to show that the high-depth property (false-point fraction above 1) is empty and therefore fails largeness, which in turn lets jfrust_not_natural conclude that J-frustration lies outside the Razborov-Rudich barrier. The definition therefore closes one link in the chain that separates Recognition-Science constructions from natural-proof obstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.