IsConstructive
IsConstructive packages the requirement that a complexity property P must be decidable on every finite truth table. Researchers examining natural proofs for circuit lower bounds cite it to verify the first Razborov-Rudich criterion before checking largeness and usefulness. The declaration is a structure that directly records the decidability predicate without further reduction.
claimA complexity property $P$ is constructive when, for every natural number $n$ and every Boolean function $f$ on $n$ inputs, the statement $P(n,f)$ is decidable.
background
The module examines whether J-frustration satisfies the three conditions for a natural proof in the sense of Razborov-Rudich: constructiveness, largeness, and usefulness. A complexity property is defined as a map sending each arity $n$ and each truth table of size $2^n$ to a proposition. The local setting isolates J-frustration as a candidate property whose depth exceeds one, rendering it non-natural once the three conditions are checked.
proof idea
This is a structure definition that directly encodes the decidability requirement. No lemmas or tactics are invoked; the single field records the universal quantifier over $n$ and $f$ together with the Decidable instance.
why it matters in Recognition Science
It supplies the constructive component of IsNatural, which is then used in jfrust_not_natural to derive a contradiction from the assumption that a high-depth property is natural. The result supports the module claim that J-frustration evades the Razborov-Rudich barrier and therefore does not obstruct circuit lower bounds in the Recognition Science setting.
scope and limits
- Does not assert that any concrete property satisfies the decidability condition.
- Does not address the largeness or usefulness criteria.
- Does not quantify over infinite families of functions.
- Does not connect to the phi-ladder or forcing chain.
formal statement (Lean)
91structure IsConstructive (P : ComplexityProperty) where
92 dec : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, Decidable (P n f)
93
94/-- A property is useful if it implies hardness. -/