falsePointFraction_le_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish any lower bound on the false-point fraction.
- Does not apply outside finite Boolean domains of size 2^n.
- Does not reference J-cost, Laplacian, or frustration measures.
- Does not address circuit size or computability of the function.
formal statement (Lean)
55theorem falsePointFraction_le_one {n : ℕ} (f : (Fin n → Bool) → Bool) :
56 FalsePointFraction f ≤ 1 := by
proof body
Tactic-mode proof.
57 unfold FalsePointFraction
58 have hcard_pos : (0 : ℝ) < (Finset.univ.card (α := Fin n → Bool) : ℝ) := by
59 exact_mod_cast Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
60 rw [div_le_one hcard_pos]
61 exact_mod_cast Finset.card_filter_le _ _
62
63/-- The constant-true function has zero false-point fraction. -/