falsePointFraction_le_one
plain-language theorem explainer
False-point fraction is bounded above by one for every Boolean function on a finite domain. Workers on natural proofs cite the result to show that high-depth properties become empty once the threshold exceeds one. The argument unfolds the definition, confirms the denominator is positive, and reduces the claim to a standard Finset cardinality inequality.
Claim. For every natural number $n$ and every Boolean function $f: (Fin n → Bool) → Bool$, the false-point fraction satisfies $ |{a : Fin n → Bool | ¬f(a)}| / 2^n ≤ 1 $.
background
The module studies whether J-frustration properties can serve as natural proofs in the Razborov-Rudich sense. A natural proof must be constructive (poly-time computable), large (fraction at least 1/poly(n) of all functions), and useful (implies no small circuits). FalsePointFraction is defined directly as the proportion of truth-table entries where f evaluates to false, without CNF encoding; it equals landscape depth for the canonical full-width encoding.
proof idea
The proof unfolds FalsePointFraction to expose the ratio of cardinalities. It establishes positivity of the denominator by exhibiting the constant-false function and applying Finset.card_pos. It then rewrites the target via div_le_one and invokes the library fact Finset.card_filter_le to conclude that the filtered set of false points cannot exceed the full domain.
why it matters
The bound is invoked directly in high_depth_empty to prove that HighDepthProp tau n f is impossible for tau > 1, and it is packaged inside nonNaturalnessCert as fraction_le_one. This step shows that high-depth J-frustration properties are empty and therefore fail the largeness requirement of natural proofs, allowing the module to conclude that jfrust_not_natural holds and the Razborov-Rudich barrier does not apply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.