cycles_lower_bound
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not prove a classical separation of P and NP in the Turing model.
- Does not apply to systems with unbounded or oracle-assisted bandwidth.
- Does not supply an upper bound or constructive certification algorithm.
formal statement (Lean)
94theorem cycles_lower_bound {n t : ℕ}
95 (h : 360 * t < 2 ^ n) :
96 bandwidthBudget t < npWorkload n := by
proof body
Term-mode proof.
97 apply insufficient_budget_no_certify
98 rw [bitBandwidthPerCycle_eq]
99 exact h
100
101/-! ## §4. Doubling separation -/
102
103/-- Adding one bit to the search space doubles the workload. -/