recognitionBudget
plain-language theorem explainer
The definition introduces the recognition budget as the constant 360, computed directly as eight times forty-five. Complexity theorists examining structural bounds on NP problems within the Recognition Science framework cite this value when comparing exponential search workloads to polynomial cycle allowances. The definition is a straightforward numerical assignment with no additional proof steps required.
Claim. Define the per-cycle recognition budget by $B := 8 × 45$.
background
In the module deriving P versus NP from Recognition Science, the per-cycle bandwidth equals 360 units. This value is the product of the eight-tick octave period and a gap parameter of 45, written as ledgerPeriod times gap45. The local setting treats NP-search workload as scaling with $2^n$ and notes that $2^n ≤ 360 × n$ holds only for small $n$ before exponential growth dominates.
proof idea
The definition is introduced directly as the arithmetic product of 8 and 45, serving as a one-line numerical constant with no lemmas or tactics applied.
why it matters
This definition supplies the per-cycle recognition budget required by the structural certificate PvsNPStructuralCert, which asserts P is contained in NP under the Recognition Science framework. It instantiates the eight-tick octave from the forcing chain at T7, fixing the budget at 360 to bound workloads against 360 times n cycles. The downstream theorem budget_eq_360 confirms the equality by decision procedure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.