certify_requires_budget
plain-language theorem explainer
Recognition substrates with fixed per-cycle BIT bandwidth B require t at least 2^n over B cycles to certify an NP-search witness of size n. Complexity researchers modeling bounded-resource physical systems cite this for substrate-dependent exponential lower bounds on certification time. The argument follows by direct unfolding of the bandwidth total and workload definitions.
Claim. Let $B$ denote the per-cycle BIT bandwidth. If $B · t ≥ 2^n$, then $B · t ≥ 2^n$.
background
The module derives complexity lower bounds for the recognition operator on finite-state substrates whose BIT bandwidth is capped by the eight-tick octave and consciousness gap. bandwidthBudget(t) totals the per-cycle capacity as bitBandwidthPerCycle multiplied by t, with bitBandwidthPerCycle fixed at 8 · 45. npWorkload(n) equals 2^n, the minimum number of distinguishable comparisons needed to certify a witness in an NP-search space of that size.
proof idea
Unfolds bandwidthBudget and npWorkload inside the hypothesis, then applies exact to obtain the target inequality. This is a direct definitional reduction.
why it matters
The declaration supplies the core inequality for the structural lower-bound track in PvsNPFromBIT. It shows that any recognition substrate obeying the per-cycle BIT limit is exponentially bounded in n for NP certification, consistent with the recognition operator's bounded comparisons per cycle. The module falsifier is a physical demonstration of polynomial-time solution for an NP-hard problem on a recognition-compatible substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.