prepare safe
ProvedResourceScheduling.Graph.prepare_safealgorithmspolynomial-time
The parser and matrix-length preparation execute within a quadratic numeric register bound, for every input word.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram import Definitions.Def_ResourceScheduling_Graph_RAMSafe open ResourceScheduling.Graph GraphReg GraphProgram
Formal statement
namespace ResourceScheduling.Graph
theorem prepare_safe (B L : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
(hL : s.word.length ≤ L) (hB : 9 * L * L + 3 * L + 1 ≤ B) : RAMSafe prepare B s := 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.