bandwidthBudget
plain-language theorem explainer
bandwidthBudget accumulates total BIT bandwidth over t cycles as the product of the fixed per-cycle value 360 and t. Researchers deriving substrate-dependent lower bounds on NP-search certification times within Recognition Science cite this definition when comparing available capacity against exponential workload. It is introduced as a direct one-line product that supplies the left-hand side for all subsequent budget-comparison results.
Claim. The cumulative bandwidth after $t$ cycles equals $360t$, where the per-cycle BIT bandwidth is the constant $8$ times the consciousness gap parameter $45$.
background
The module derives structural lower bounds on recognition time for NP-search problems when the substrate is limited by fixed BIT bandwidth. The upstream constant bitBandwidthPerCycle is defined as $8$ times the consciousness gap of $45$, yielding the per-cycle capacity of $360$ bits. This models the maximum number of useful comparisons the recognition operator can execute in one cycle on a finite-state substrate.
proof idea
The definition is a direct product of the upstream constant bitBandwidthPerCycle with the cycle count $t$. No lemmas or tactics are invoked; the declaration is unfolded verbatim in every downstream comparison theorem.
why it matters
This definition supplies the left-hand side of the inequalities in certify_requires_budget and cycles_lower_bound, which together show that $360t < 2^n$ precludes certification of an NP-search witness of size $n$. It operationalizes the module claim that bounded bandwidth forces exponential time for recognition substrates and sits in track F8 of the Recognition Science plan. The result supports the broader derivation of substrate-dependent complexity bounds without classical Turing separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.