pith. sign in
module module high

IndisputableMonolith.Complexity.NonNaturalness

show as:
view Lean formalization →

This module introduces the false-point fraction |f^{-1}(false)|/2^n as a direct measure of Boolean function complexity that bypasses CNF encodings. Complexity theorists examining non-natural properties in the Recognition Science setting cite it when linking J-frustration to topological obstructions. The module supplies supporting definitions and elementary bounds with no internal proofs.

claimFor a Boolean function $f : 2^n → 2$, the false-point fraction is $|f^{-1}(false)| / 2^n$. For any CNF-encodable $f$ this equals the landscape depth of its canonical full-width encoding.

background

The module sits inside the Complexity domain and imports the J-cost Laplacian on the Boolean hypercube, where vertices are assignments in {0,1}^n and edge weights equal |satJCost(φ,a) - satJCost(φ,a')|. It also draws on J-frustration, defined as the binary topological depth of the J-cost barrier around the satisfying region (0 for SAT, 1 for UNSAT). Constants supplies the RS time quantum τ₀ = 1 tick. The RSatEncoding module supplies the upstream claim that R̂ reaches zero J-cost in O(n) steps for satisfiable instances.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the non-naturalness apparatus that PvsNPAssembly imports to separate J-frustration from natural properties. It thereby supports the conditional Path A in PvsNPAssembly: J-frustration is non-natural, so the RR barrier does not apply, and high frustration implies exponential circuit size. The definitions close the interface between RSatEncoding and the P vs NP resolution structure.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (16)