IsLarge
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert that any concrete property satisfies the counting bound.
- Does not supply the constructive or useful halves of naturalness.
- Does not quantify over circuit-size parameters or lower-bound statements.
- Does not address asymptotic density for infinite families of functions.
formal statement (Lean)
82structure IsLarge (P : ComplexityProperty) where
83 k : ℕ
84 dec : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, Decidable (P n f)
85 count_bound : ∀ n : ℕ, 0 < n →
86 (Finset.univ.filter (fun f : (Fin n → Bool) → Bool =>
87 @decide (P n f) (dec n f))).card * n ^ k ≥
88 Finset.univ.card (α := (Fin n → Bool) → Bool)
proof body
Definition body.
89
90/-- A property is constructive if decidable. -/