const_false_full_fraction
plain-language theorem explainer
The constant-false Boolean function on n inputs has false-point fraction exactly 1. Researchers analyzing natural-proof barriers in circuit complexity cite this when showing that high false-point-fraction properties fail the largeness condition required by Razborov-Rudich. The proof is a direct unfolding of the fraction definition followed by simplification that counts all 2^n inputs as false points.
Claim. For every natural number $n$, the false-point fraction of the constant-false function $f: (Fin n → Bool) → Bool$ equals 1.
background
The module examines non-naturalness of J-frustration inside the Razborov-Rudich framework. A natural proof needs a property that is constructive, large (probability at least 1/poly(n) over random truth tables), and useful for proving circuit lower bounds. The false-point fraction of a Boolean function is the proportion of inputs on which the function returns false, defined directly as |f^{-1}(false)| / 2^n without CNF encoding; it serves as the direct analog of landscape depth for the canonical full-width encoding.
proof idea
The proof is a one-line wrapper that unfolds the false-point fraction definition and applies simplification. The simplification recognizes that the filter over all 2^n inputs retains every element when the function is constantly false, so the ratio equals 1.
why it matters
This calculation supplies the base case for showing that any property requiring false-point fraction greater than 1 is empty and therefore not large. It therefore supports the claim that high-depth properties fail naturalness and that the Razborov-Rudich barrier does not apply to J-frustration. The result sits inside the module's demonstration that zero-sorry formalization of the non-naturalness argument is possible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.