const_true_zero_fraction
plain-language theorem explainer
The constant-true Boolean function on n variables has false-point fraction exactly zero. Complexity theorists studying natural proofs and Razborov-Rudich barriers cite this base case when verifying that depth-based properties fail largeness. The proof is a one-line wrapper that unfolds the false-point fraction definition and simplifies the empty filter cardinality.
Claim. Let $f$ be the constant-true function from $(Fin n → Bool)$ to $Bool$. Then the false-point fraction of $f$ satisfies $FalsePointFraction(f) = 0$.
background
FalsePointFraction of a Boolean function $f$ on $n$ variables is the proportion of inputs where $f$ returns false, given by the cardinality of the preimage of false divided by $2^n$. This quantity acts as the direct analog of landscape depth for J-frustration without CNF encoding, as stated in its definition: the fraction equals the landscape depth of the canonical full-width encoding with one blocking clause per false point.
proof idea
The proof is a one-line wrapper that unfolds FalsePointFraction and applies simp to reduce the cardinality of the empty set of false points to zero.
why it matters
This theorem supplies the const_true_zero component of nonNaturalnessCert, which assembles the certificate that J-frustration fails naturalness. It supports the claim that high false-point fraction properties are not large, bypassing the Razborov-Rudich barrier for circuit lower bounds. The module's zero-sorry status confirms the framework's complexity claims rest on fully formalized base cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.