IsConstructive
plain-language theorem explainer
A complexity property is constructive when the predicate it assigns to each arity and truth table is decidable. Researchers working on natural proofs in circuit complexity cite the definition to verify the first Razborov-Rudich condition before checking largeness or usefulness. The structure consists of a single field that directly encodes the decidability requirement.
Claim. Let $P$ be a complexity property. Then $P$ is constructive if for every natural number $n$ and every function $f: (Fin n → Bool) → Bool the proposition $P(n,f)$ is decidable.
background
The module studies whether J-frustration can serve as the basis of a natural proof in the sense of Razborov-Rudich 1997. Such a proof requires a property that is constructive (decidable in poly time), large (holds for a 1/poly fraction of truth tables), and useful (implies no small circuits). ComplexityProperty is the interface type that maps each arity n and each Boolean function on n bits to a proposition; the present definition isolates the constructive leg of that interface.
proof idea
This is a structure definition whose single field requires decidability of the property predicate for all arities and all functions. No lemmas or tactics are invoked; the definition itself supplies the required decidability assertion.
why it matters
IsConstructive supplies the first conjunct of IsNatural, which combines constructiveness, largeness, and usefulness to capture a natural proof. It is invoked in jfrust_not_natural to derive a contradiction from the assumption that a high-depth property is natural, thereby showing that the Razborov-Rudich barrier does not apply to J-frustration. The definition therefore supports the module claim that J-frustration lies outside the natural-proof regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.