pith. sign in
module module high

IndisputableMonolith.Complexity.NonNaturalness

show as:
view Lean formalization →

The NonNaturalness module defines the false-point fraction for Boolean functions as an analog to landscape depth in the J-cost setting, along with properties classifying naturalness and depth. It equips the Recognition Science treatment of complexity to separate natural from non-natural behaviors without CNF mediation. Researchers resolving P vs NP via topological obstructions would cite these objects. The module consists of definitions and elementary fraction bounds with no deep proofs.

claimFor a Boolean function $f : (Fin n) → Bool$, the false-point fraction is $|f^{-1}(false)| / 2^n$. This quantity equals the landscape depth of the canonical full-width CNF encoding of $f$. Related predicates include IsNatural, IsConstructive, IsUseful, IsLarge, and HighDepthProp on such functions.

background

The module operates inside the Recognition Science complexity framework. It imports the J-cost Laplacian on the Boolean hypercube, whose edges carry weights |satJCost(φ, a) − satJCost(φ, a′)| for Hamming-distance-1 assignments. It further relies on J-frustration, which quantifies the topological depth of the J-cost barrier around a formula’s satisfying region, and on the R̂ SAT encoding that supplies a non-natural polytime certifier for satisfiable k-CNF instances. Constants are taken from the RS-native time quantum τ₀ = 1 tick.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the non-naturalness vocabulary that feeds the P vs NP Assembly. In particular it supports the step that J-frustration is non-natural (Phase 2 of the conditional P ≠ NP path), allowing the RR barrier to be bypassed and linking to the topological obstruction results in RSatEncoding. It also populates the Core.Complexity interface.

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)