ComplexityProperty
plain-language theorem explainer
A complexity property is a predicate that assigns to each natural number n and each Boolean function on n inputs a proposition. Researchers formalizing natural proofs in circuit complexity, especially when checking the Razborov-Rudich barrier for J-frustration measures, would cite this definition. The declaration is a direct type abbreviation with no further structure or proof obligations.
Claim. A complexity property is a map sending each natural number $n$ and each function $f : 2^n → 2$ to a proposition $P(n,f)$.
background
The module examines whether J-frustration satisfies the three conditions of a natural proof (constructive, large, useful) from Razborov-Rudich 1997. A natural proof would require a property P of Boolean functions that is computable in poly(2^n) time, holds for a 1/poly(n) fraction of truth tables, and implies no poly-size circuits. This definition supplies the underlying type for all such properties in the J-cost and Laplacian setting. Upstream structures calibrate J via ledger factorization and phi-forcing, supplying the cost function whose frustration is later tested for naturalness.
proof idea
One-line definition that directly encodes the predicate over arities and truth tables.
why it matters
This definition is the common type for IsConstructive, IsLarge, IsUseful, and IsNatural, which in turn feed HighDepthProp. The downstream results use it to show that the high-depth property (false-point fraction ≥ τ) is empty for τ > 1 and therefore fails largeness, so the Razborov-Rudich barrier does not obstruct lower bounds on J-frustration. The construction sits inside the Recognition Science treatment of complexity measures derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.