PvsNPFromBITCert
plain-language theorem explainer
The PvsNPFromBITCert structure packages the BIT bandwidth axioms and derived properties that underpin the exponential lower bound on NP-witness certification. Complexity researchers studying recognition substrates cite it to invoke the full set of assumptions for the t >= 2^n / 360 bound. It is assembled by direct reference to the per-cycle bandwidth definition, workload doubling, and the cycles lower bound theorem.
Claim. A structure asserting that the per-cycle bandwidth equals 360, is positive, the total budget satisfies budget(0) = 0 and budget(t+1) = budget(t) + 360, the workload W(n) = 2^n is positive and doubles with each increment, 360 t < 2^n implies budget(t) < W(n), and W(n+1) - W(n) = W(n).
background
The module derives complexity lower bounds for the recognition operator on a substrate whose BIT bandwidth is capped at 8 times the consciousness gap, yielding 360 units per cycle. Bandwidth budget after t cycles is defined as the product of this per-cycle value and t. NP workload is the search-space size 2^n, the minimum number of distinguishable comparisons required to certify a witness.
proof idea
This is a structure definition that directly bundles the referenced definitions and lemmas: bitBandwidthPerCycle equality and positivity, the recursive bandwidthBudget rules, npWorkload positivity and doubling, the cycles lower bound theorem, and the doubling separation theorem. No tactics or reductions are performed.
why it matters
It supplies the complete certificate for the BIT lower-bound derivation and is instantiated by the downstream pVsNPFromBITCert definition. The structure closes the master-certificate section of the module, connecting the bounded-bandwidth recognition operator to the exponential workload and the phi-rung substrate constraints. It leaves open whether any physical recognition system can evade the bound without hypercomputation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.