ComplexityProperty
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not impose decidability or computability on the predicate.
- Does not reference circuit size, depth, or J-cost directly.
- Does not fix any probability measure beyond the uniform counting used in IsLarge.
- Does not encode any concrete property such as false-point fraction.
formal statement (Lean)
78def ComplexityProperty := ∀ n : ℕ, ((Fin n → Bool) → Bool) → Prop
proof body
Definition body.
79
80/-- A property is **large** if the fraction of n-ary truth tables satisfying it
81 is at least 1/n^k for some fixed k. -/