program cost
ProvedResourceScheduling.Graph.program_costalgorithmspolynomial-time
The actual fixed graph program and the final reversal transfer fit one polynomial source-step deadline on every word, including empty and malformed inputs.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram open ResourceScheduling.Graph GraphReg GraphProgram
Formal statement
namespace ResourceScheduling.Graph
theorem program_cost : ∃ k, ∀ w : List Letter,
program.cost ⟨fun _ => 0, w, []⟩ + 3 * (wordProgram w).length + 2 ≤ w.length ^ k + k := by sorry
end ResourceScheduling.GraphSource
New auxiliary formalization for the ResourceScheduling Q2 reduction. The target is the unchanged CookPvsNP one-tape machine model, following Cook, The P versus NP problem, Clay Mathematics Institute (2000), Appendix. This explicit finite-column stack compiler and its simulation lemmas are new contributions, not numbered claims from Cook or the scheduling source paper.