FalsePointFraction
plain-language theorem explainer
The false-point fraction of a Boolean function f on n bits equals the share of assignments where f evaluates to false. Complexity theorists analyzing natural proofs and the Razborov-Rudich barrier cite this quantity as the direct counting measure of landscape depth. The definition implements the ratio by filtering the full truth table for negated outputs and dividing the resulting cardinality by 2^n.
Claim. For a Boolean function $f : (Fin n → Bool) → Bool$, the false-point fraction is $|f^{-1}(false)| / 2^n$.
background
The module develops non-naturalness results for J-frustration by importing the Razborov-Rudich criteria for natural proofs: a property must be constructive (poly-time computable), large (probability at least 1/poly(n)), and useful (implies no poly-size circuits). FalsePointFraction supplies the raw counting measure that avoids CNF encodings entirely. HighDepthProp later wraps this fraction at a threshold τ to test the naturalness conditions.
proof idea
One-line definition that counts the filtered preimage of false via Finset.univ.filter and divides by the explicit cardinality of the full space Fin n → Bool.
why it matters
FalsePointFraction supplies the counting primitive for HighDepthProp and NonNaturalnessCert. The latter shows that any τ > 1 yields an empty property, violating the largeness requirement and thereby bypassing the Razborov-Rudich barrier for J-frustration. This step closes the direct analog to landscape depth inside the Recognition Science treatment of complexity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.