ComplexityProperty
plain-language theorem explainer
ComplexityProperty is the type of predicates assigning to each arity n and each n-ary Boolean function a proposition. Researchers formalizing natural-proof barriers in circuit complexity would cite it when embedding the Razborov-Rudich theorem into the Recognition Science setting. The declaration is a direct type abbreviation with no computational content or proof obligations.
Claim. A complexity property is a map that, for every natural number $n$, sends each function from a set of size $2^n$ to a proposition: $P : (n : ℕ) → ((Fin n → Bool) → Bool) → Prop$.
background
The module NonNaturalness formalizes the Razborov-Rudich natural-proof barrier for J-frustration. A natural proof requires a property that is constructive (decidable in poly(2^n) time), large (holds for a 1/poly(n) fraction of truth tables), and useful (implies no poly-size circuits). ComplexityProperty supplies the ambient type for all such predicates. Upstream results supply the J-cost structures from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of that later connect frustration metrics to these Boolean predicates.
proof idea
The declaration is a one-line type abbreviation that directly encodes the universal quantification over arities and truth tables.
why it matters
This definition anchors the non-naturalness results. It is instantiated by HighDepthProp (false-point fraction ≥ τ) and then fed into IsNatural, which assembles IsConstructive, IsLarge, and IsUseful. The construction shows that high-depth properties fail largeness for τ > 1, so the Razborov-Rudich barrier does not obstruct J-frustration lower bounds. It therefore closes one link between the phi-ladder forcing chain and circuit-complexity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.