doubling_separation
The minimum comparisons needed to certify an NP-search witness of size n+1 exceeds the requirement for size n by exactly that same amount. Researchers deriving substrate-dependent complexity bounds from recognition operators would cite this doubling property. The proof reduces directly to the successor lemma for the workload function followed by arithmetic normalization.
claimLet $W(n) := 2^n$ denote the minimum number of distinguishable comparisons required to certify a witness for an NP-search problem of size $n$. Then $W(n+1) - W(n) = W(n)$.
background
In the module deriving computational complexity lower bounds from BIT bandwidth, the recognition operator on a substrate with bounded bandwidth B performs at most B · t comparisons in time t. The npWorkload function is defined as the minimum comparisons for an NP-search witness of size n, which equals 2^n. The upstream npWorkload_succ theorem states that adding one bit doubles the workload: npWorkload (n+1) = 2 * npWorkload n.
proof idea
The proof is a one-line wrapper that rewrites using the successor lemma npWorkload_succ and then applies the omega tactic for arithmetic.
why it matters in Recognition Science
This result establishes the structural doubling property that feeds into the master certificate PvsNPFromBITCert, which collects the bandwidth and workload axioms for the lower-bound derivation. It fills the chain step showing that each additional input bit doubles the required bandwidth budget, yielding the exponential lower bound on recognition time for NP witnesses. The module notes that a physical demonstration of polynomial-time NP-hard solution on a compatible substrate would falsify the bound.
scope and limits
- Does not establish a classical separation between P and NP in the Turing model.
- Does not apply to hypercomputational or oracle-assisted substrates.
- Does not quantify the constant factors in the bandwidth bound.
- Does not address average-case complexity.
formal statement (Lean)
110theorem doubling_separation (n : ℕ) :
111 npWorkload (n + 1) - npWorkload n = npWorkload n := by
proof body
Term-mode proof.
112 rw [npWorkload_succ]
113 omega
114
115/-! ## §5. Master certificate -/
116