bitBandwidthPerCycle_pos
plain-language theorem explainer
The theorem establishes that the per-cycle BIT bandwidth is strictly positive. Researchers deriving exponential runtime lower bounds for NP certification on recognition substrates cite this result to keep the division by bandwidth well-defined. The proof is a one-line term that substitutes the explicit value via its equality theorem and normalizes the numeral 360.
Claim. $0 < B$, where $B$ is the per-cycle BIT bandwidth fixed at 360 in native units.
background
The module derives structural lower bounds on NP certification time from the bounded BIT bandwidth of any recognition substrate. The per-cycle bandwidth constant equals eight times the consciousness gap value of 45. This rests on the bandwidth definition from the RecognitionBandwidth module, which states that the maximum number of recognition events per unit time is the boundary area divided by four Planck areas, the per-event recognition cost, and the eight-tick cadence. The immediate upstream result is the equality theorem that fixes the constant exactly at 360.
proof idea
The proof rewrites the target inequality using the equality theorem that identifies the bandwidth with 360, then applies norm_num to confirm positivity of the concrete natural number.
why it matters
This positivity statement supplies a required field in the downstream pVsNPFromBITCert structure that assembles the components for the BIT-based exponential lower bound. It supports the module claim that any NP search problem requires time at least two to the power n over the bandwidth on a recognition substrate. The result is consistent with the eight-tick octave and the recognition bandwidth definition, yielding a substrate-dependent bound rather than a classical complexity separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.