bandwidthBudget_succ
plain-language theorem explainer
The successor relation for cumulative BIT bandwidth states that total comparisons after t+1 cycles equal those after t cycles plus the fixed per-cycle allocation of 360 bits. Researchers deriving substrate-dependent lower bounds on NP-search would cite this to establish linear accumulation of recognition capacity. The proof is a one-line term that unfolds the bandwidth definition and normalizes via ring.
Claim. Let $B(t)$ denote total BIT bandwidth after $t$ cycles and let $b$ be the fixed per-cycle bandwidth. Then for every natural number $t$, $B(t+1) = B(t) + b$, where $B(t) := b · t$ and $b = 360$.
background
The module derives complexity lower bounds for the recognition operator on a substrate whose BIT bandwidth is bounded per cycle. Total bandwidth after $t$ cycles is the product of per-cycle bandwidth and $t$. Per-cycle bandwidth equals 8 times the consciousness gap, fixed at 360 bits. This linear accumulation supplies the comparison budget available to certify witnesses in NP-search problems of size $n$, yielding the bound $t ≥ 2^n / B$ stated in the module header.
proof idea
One-line term proof: unfold the definition of bandwidthBudget, then apply ring to normalize the resulting arithmetic equality.
why it matters
Supplies the successor case required by pVsNPFromBITCert to certify the structural lower bound on NP-search runtime. It completes the inductive step in the argument that any recognition substrate with bounded bandwidth requires exponential cycles for $2^n$ comparisons. The result supports the φ-rung lower bound on real physical computation rather than a classical Turing separation, consistent with the module's falsifier of polynomial-time NP solution on a compatible substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.