pVsNPFromBITCert
plain-language theorem explainer
The pVsNPFromBITCert structure bundles the BIT bandwidth fixed at 360, recursive budget and workload definitions, positivity conditions, doubling property, and exponential lower-bound inequality into a single certificate. Researchers deriving substrate-dependent runtime bounds for NP-search problems in Recognition Science would cite it as the master certificate for the structural exponential requirement. It is assembled as a direct structure definition that references the supporting lemmas for each field without further proof steps.
Claim. Let $B=360$ be the per-cycle BIT bandwidth. Define the bandwidth budget after $t$ cycles by budget$(0)=0$ and budget$(t+1)=$budget$(t)+B$. Let the NP workload satisfy workload$(n)>0$ for all $n$ and workload$(n+1)=2·$workload$(n)$. Then for all $n,t$, if $360t<2^n$ it follows that budget$(t)<$workload$(n)$, and each additional input bit doubles the required budget.
background
The module derives a structural lower bound on NP-search certification from the bounded BIT bandwidth of any recognition substrate. The recognition operator performs at most $B$ useful comparisons per cycle; any problem requiring distinction among $2^n$ possibilities is therefore bounded below by $t≥2^n/B$. Key definitions are bitBandwidthPerCycle (fixed at 360), bandwidthBudget (the cumulative sum over cycles), npWorkload (the exponential $2^n$ size), and the cycles_lower_bound theorem that enforces the strict inequality when budget is insufficient.
proof idea
The definition is a one-line structure constructor that directly assigns each field of PvsNPFromBITCert to the corresponding pre-established lemma: bitBandwidthPerCycle_eq supplies the equality, bandwidthBudget_zero and bandwidthBudget_succ supply the recursion, npWorkload_pos and npWorkload_succ supply workload properties, cycles_lower_bound supplies the main inequality via insufficient_budget_no_certify, and doubling_separation supplies the doubling step.
why it matters
This certificate completes the master bundle for the structural lower bound in Track F8, establishing that NP-search certification on any BIT-bounded recognition substrate requires time exponential in $n$. It supplies the concrete claim that runtime is at least $⌈2^n/360⌉$ cycles and is explicitly a φ-rung bound rather than a classical Turing separation. The module doc identifies the falsifier as a physical demonstration of polynomial-time NP solution on a compatible substrate; the result sits downstream of the bandwidth recursion lemmas and upstream of any application of the exponential bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.