falsePointFraction_nonneg
plain-language theorem explainer
The false-point fraction of any Boolean function on n variables is non-negative as a ratio of cardinalities. Researchers analyzing natural proof barriers in circuit complexity cite this to ground definitions of high-depth predicates. The proof is a one-line term that unfolds the definition and applies non-negativity of division after casting naturals to reals.
Claim. For any natural number $n$ and Boolean function $f: (Fin n → Bool) → Bool$, the false-point fraction satisfies $0 ≤ |{a : Fin n → Bool | ¬f(a)}| / 2^n$.
background
The Non-Naturalness module examines why J-frustration properties fail to qualify as natural proofs in the Razborov-Rudich sense: a property must be constructive, large (fraction at least 1/poly(n) of truth tables), and useful for establishing circuit lower bounds. The false-point fraction is defined directly as the proportion of inputs where f evaluates to false, serving as the analog of landscape depth for CNF-encodable functions without explicit encoding. This supplies the basic non-negativity needed before introducing predicates such as HighDepthProp that threshold the fraction at some τ.
proof idea
The term proof unfolds FalsePointFraction to a ratio of two Nat.card values cast to ℝ, then invokes div_nonneg on the pair of non-negative reals obtained from Nat.cast_nonneg. No further lemmas or case analysis are required.
why it matters
This supplies the lower bound for FalsePointFraction, enabling the module's later results on HighDepthProp and the demonstration that high-depth predicates are not large when τ > 1. It thereby supports the claim that J-frustration based properties evade the Razborov-Rudich barrier, consistent with the Recognition Science emphasis on non-natural constructions. The companion upper-bound lemma falsePointFraction_le_one completes the [0,1] interval for the fraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.