npWorkload_pos
plain-language theorem explainer
npWorkload_pos shows that the NP workload 2^n remains strictly positive for every natural number n. Researchers deriving substrate-dependent complexity bounds in Recognition Science cite it to ensure the search-space size never vanishes when constructing lower bounds from bounded BIT bandwidth. The proof is a direct one-line application of the natural-number power-positivity lemma to base 2.
Claim. For every natural number $n$, $0 < 2^n$, where $2^n$ denotes the minimum number of distinguishable comparisons required to certify an NP-search witness of size $n$.
background
The module derives structural lower bounds on NP certification time from the recognition operator's BIT bandwidth. npWorkload is defined as $2^n$, the size of the canonical NP search space that must be distinguished by comparisons. bandwidthBudget(t) multiplies the per-cycle bandwidth (fixed at 360) by the number of cycles t, so any certification requires bandwidthBudget(t) at least npWorkload(n). Upstream structures calibrate the underlying J-cost and physical tiers that fix the bandwidth constant; the local setting is therefore a substrate-dependent exponential bound, not a classical Turing separation.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the fact that 0 < 2 in the naturals, yielding positivity of 2^n for any n.
why it matters
This positivity fact is required by the PvsNPFromBITCert structure that assembles the doubling separation and master certificate for the BIT-derived lower bound. It completes the workload side of the exponential runtime claim: any finite-bandwidth recognition substrate needs at least 2^n / B cycles. The result remains inside the Recognition framework's phi-rung accounting and does not claim a classical P versus NP separation; the open question it leaves is whether any physical substrate can evade the bound without hypercomputation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.