FalsePointFraction
The false-point fraction computes the share of inputs where a Boolean function returns false, expressed as a ratio of cardinalities. Researchers examining natural proof barriers in circuit complexity cite this when linking to landscape depth measures in Recognition Science. It is implemented as a direct division of filtered Finset size by the total number of assignments.
claimFor a Boolean function $f : (Fin n → Bool) → Bool$, the false-point fraction is $|{x : Fin n → Bool | f(x) = false}| / 2^n$.
background
The module develops non-naturalness results for J-frustration by constructing properties of Boolean functions that violate the Razborov-Rudich criteria (constructive, large, useful) for natural proofs. The false-point fraction supplies a direct count of false evaluations, serving as the analog of landscape depth without any CNF encoding step. For CNF-encodable functions it coincides exactly with the depth of the canonical full-width encoding that places one blocking clause at each false point.
proof idea
The definition is a one-line wrapper that filters the universe of all 2^n assignments to retain those where the function returns false, takes the cardinality of that subset, and divides by the cardinality of the full universe.
why it matters in Recognition Science
This definition supplies the core counting measure for HighDepthProp and the NonNaturalnessCert structure. It enables the explicit demonstration that any high-depth property with threshold above one is empty and therefore fails the largeness condition, so the Razborov-Rudich barrier does not obstruct J-frustration arguments. The construction sits inside the Recognition Science treatment of complexity via J-cost and the forcing chain.
scope and limits
- Does not apply to functions whose domain is not exactly the set of all n-bit strings.
- Does not incorporate any CNF or circuit representation of the function.
- Does not compute or bound circuit size or depth.
- Does not depend on J-cost, defect distance, or phi-ladder quantities.
Lean usage
theorem const_false_full_fraction (n : ℕ) : FalsePointFraction (fun _ : Fin n → Bool => false) = 1 := by unfold FalsePointFraction; simpformal statement (Lean)
44def FalsePointFraction {n : ℕ} (f : (Fin n → Bool) → Bool) : ℝ :=
proof body
Definition body.
45 (Finset.univ.filter (fun a : Fin n → Bool => !f a)).card /
46 (Finset.univ.card (α := Fin n → Bool) : ℝ)
47
48/-- False-point fraction is non-negative. -/