count cell safe
ProvedResourceScheduling.Graph.count_cell_safealgorithmspolynomial-time
One conditional non-edge count increment preserves the numeric bound with one unit of counter headroom.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram import Definitions.Def_ResourceScheduling_Graph_RAMSafe open ResourceScheduling.Graph GraphReg GraphProgram
Formal statement
namespace ResourceScheduling.Graph
theorem count_cell_safe (B N : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
(hi : s.val i ≤ N) (hj : s.val j ≤ N) (hn : s.val n ≤ N)
(hc : s.val count + 1 ≤ B) (hB : N * N + N ≤ B) (hpos : 1 ≤ B) :
RAMSafe (ifNonEdge (.inc count)) 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.