NaturalProperty
plain-language theorem explainer
NaturalProperty encodes the Razborov-Rudich criteria of constructivity and largeness for properties on Boolean functions. Researchers bridging recognition operators on Z³ lattices to circuit complexity lower bounds cite it when showing that global J-cost minimization evades polynomial-size truth tables. The structure is introduced as a direct definition of the two Prop fields with no derivation steps.
Claim. A predicate on Boolean functions is natural when it is constructive (computable in polynomial time from the truth table) and large (satisfied by a random function with probability at least $1/mathrm{poly}(n)$).
background
The TuringBridge module connects the RS recognition operator R-hat acting on the full Z³ ledger to classical P versus NP. It encodes SAT instances as J-cost landscapes where R-hat reaches zero defect precisely when satisfiable. Natural properties must act on polynomial-size truth tables rather than the complete lattice topology. The module imports JcostCore and Constants to ground the landscape construction. Upstream results supply collision-free properties from OptionAEmpiricalProgram.is and algebraic tautologies from SimplicialLedger.EdgeLengthFromPsi.is that support the ledger encoding.
proof idea
This is a definition that directly declares the two Prop fields matching the Razborov-Rudich conditions. No lemmas or tactics are applied; the structure serves as the interface type for the subsequent non-naturality claim.
why it matters
The definition supports the non-naturality of the R-hat certificate, which is step 3 in the module strategy for the P versus NP bridge. It places the global Z³ J-cost minimization outside the class of natural properties, advancing the argument that recognition time T_R cannot be polynomial. The module documentation ties this to the open Turing simulation question in PvsNP_SelfContained_Final.tex §XIII Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.