No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
69theorem npWorkload_pos (n : ℕ) : 0 < npWorkload n :=
proof body
Term-mode proof.
70 pow_pos (by norm_num : (0:ℕ) < 2) n
71
72/-! ## §3. Lower-bound theorem -/
73
74/-- **STRUCTURAL LOWER BOUND.** If a recognition substrate of bandwidth
75`bitBandwidthPerCycle` certifies an NP-search witness in `t` cycles,
76then `bandwidthBudget t ≥ npWorkload n`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
bandwidthBudget
in IndisputableMonolith.Complexity.PvsNPFromBIT
decl_use
-
bitBandwidthPerCycle
in IndisputableMonolith.Complexity.PvsNPFromBIT
decl_use
-
npWorkload
in IndisputableMonolith.Complexity.PvsNPFromBIT
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
bandwidth
in IndisputableMonolith.Unification.RecognitionBandwidth
decl_use