jfrust_not_natural
plain-language theorem explainer
High depth properties requiring false-point fraction at least tau greater than 1 cannot satisfy the largeness condition for natural proofs. Complexity researchers studying Razborov-Rudich barriers cite this to show that J-frustration arguments evade the natural proofs obstruction. The proof is a term-mode one-liner that unpacks the IsNatural structure and applies the high_depth_not_large lemma to the extracted largeness component.
Claim. Let $tau > 1$ be real. Suppose the property $P$ that a Boolean function has false-point fraction at least $tau$ is constructive (decidable) and useful (implies hardness). Then $P$ cannot be natural.
background
The Non-Naturalness module formalizes natural proofs in the sense of Razborov-Rudich: a property must be constructive (decidable), large (holds for a positive fraction of functions), and useful (implies no small circuits). HighDepthProp tau is defined as the property that false-point fraction is at least tau; for tau > 1 this property is empty because fractions are bounded by 1. Upstream, high_depth_not_large states: THEOREM: For τ > 1, high depth is not large. An empty property trivially fails the largeness count. The module setting uses this to establish that J-frustration based properties bypass the natural proofs barrier.
proof idea
The proof is a term-mode one-liner. It introduces the IsNatural structure, extracts its large component, and applies high_depth_not_large tau htau to that component.
why it matters
This theorem supplies the barrier_bypass field in the downstream nonNaturalnessCert definition. It shows high-depth J-frustration fails naturalness, so the Razborov-Rudich barrier does not apply to such arguments. Within Recognition Science this supports non-naturalness certificates for complexity properties without invoking one-way functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.