npWorkload_succ
plain-language theorem explainer
The workload required to certify an NP-search witness of size n+1 equals twice the workload for size n. Researchers deriving substrate-dependent exponential lower bounds in Recognition Science would cite this doubling relation when bounding runtime by 2^n over bounded BIT bandwidth. The proof is a one-line algebraic reduction that unfolds the power-of-two definition and applies the exponent successor rule.
Claim. Let $W(n)$ denote the minimum number of distinguishable comparisons required to certify an NP-search witness of size $n$. Then $W(n+1) = 2 W(n)$.
background
The module derives a structural lower bound on runtime for NP-search problems on any recognition substrate whose BIT bandwidth is bounded. The npWorkload function is defined as the search-space size 2^n, giving the minimum comparisons needed to certify a witness. The module states that the recognition operator performs at most B · t comparisons in time t, so certification time is at least 2^n / B.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of npWorkload, rewrites the successor case of the power function, and normalizes the arithmetic identity with ring.
why it matters
This doubling step is invoked in doubling_separation to obtain the difference identity and in pvsNP_one_statement to close the master certificate PvsNPFromBITCert. It supplies the recursive step that makes the lower bound exponential in n on every BIT-compatible substrate, consistent with the module's φ-rung bound and the falsifier of a physical polynomial-time solution on a recognition operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.