NonNaturalnessCert
plain-language theorem explainer
The NonNaturalnessCert structure certifies that the high-depth property (false-point fraction at least tau) for any tau greater than 1 cannot qualify as natural in the Razborov-Rudich sense. Complexity theorists working on circuit lower bounds or the Recognition Science dissolution of P versus NP would cite it to confirm that J-frustration evades the natural-proofs barrier. It is assembled directly from three field definitions: zero fraction on the constant-true function, the universal bound of one on all fractions, and an implication that high
Claim. Let $F(f)$ be the false-point fraction of a Boolean function $f$. A NonNaturalnessCert consists of: $F$ of the constant-true function equals 0; $F(f) ≤ 1$ for every $f$; and for every real $τ > 1$, the property $P_τ(f) ≡ F(f) ≥ τ$ cannot be constructive, useful, and large simultaneously.
background
The module treats non-naturalness of J-frustration via the Razborov-Rudich framework: a natural property must be constructive (decidable), large (holds for a 1/poly fraction of truth tables), and useful (implies circuit hardness). FalsePointFraction is defined as the direct count |f^{-1}(false)| / 2^n, serving as the analog of landscape depth without CNF encoding. HighDepthProp(tau) is the predicate that this fraction is at least tau; the upstream doc states that for tau > 1 the property is empty because fractions cannot exceed 1. IsConstructive, IsUseful, and IsNatural are the standard structures packaging decidability, hardness implication, and the conjunction with largeness.
proof idea
The structure is a plain definition that supplies its three fields. The first two fields are witnessed by the sibling lemmas const_true_zero_fraction and falsePointFraction_le_one. The barrier_bypass field is filled by the theorem jfrust_not_natural, which assumes IsNatural, extracts the largeness component, and obtains an immediate contradiction with high_depth_not_large once tau exceeds 1.
why it matters
NonNaturalnessCert populates the non_natural field of both PneqNPConditional and PvsNPMasterCert, completing the phase-2 frustration component of the RS dissolution argument. It directly implements the module claim that high depth fails naturalness, so the Razborov-Rudich barrier does not obstruct J-frustration lower bounds. In the broader framework this step ensures the complexity phase remains compatible with the eight-tick octave and phi-ladder mass formulas without invoking natural proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.