cycles_lower_bound
plain-language theorem explainer
The theorem shows that for natural numbers n and t, if 360 t is less than 2 to the power n then the bandwidth budget after t cycles is strictly smaller than the workload needed to certify an NP-search witness of size n. Complexity researchers studying recognition-based computation would cite it when establishing exponential lower bounds on witness certification. The proof is a direct one-line application of the insufficient budget lemma after equating the per-cycle bandwidth to 360.
Claim. If $360 t < 2^n$ for natural numbers $n,t$, then the total bandwidth budget in $t$ cycles is strictly less than the minimum number of comparisons required to certify an NP-search witness of size $n$.
background
The module derives computational complexity lower bounds from the bounded bandwidth of the BIT recognition operator on a finite-state substrate. Bandwidth budget after t cycles is defined as the product of per-cycle bandwidth and t, where per-cycle bandwidth equals 360. The NP workload for input size n is defined as 2 to the power n, representing the size of the search space that must be distinguished. An upstream lemma states that if per-cycle bandwidth times t is less than 2 to the power n then the budget is insufficient for certification. This places the result in the setting of substrate-dependent exponential bounds on recognition time.
proof idea
The term proof applies the insufficient-budget theorem, rewrites the per-cycle bandwidth using its equality to 360, and discharges the goal with the supplied hypothesis.
why it matters
It contributes to the PvsNPFromBITCert structure and the pvsNP one-statement theorem, which packages the bandwidth equality, the lower bound, and the doubling property of the workload. The module documentation positions this as the structural lower bound for Track F8, where any recognition substrate with bounded BIT bandwidth requires at least the ceiling of 2 to the power n over 360 cycles to certify an NP witness. It touches the open question of whether real physical systems can evade this bound without hypercomputation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.