IsConstructive
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.