validate row

Proved

ResourceScheduling.Graph.validate_row

by arexychen · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmspolynomial-time

A complete validation row checks the diagonal and all symmetry implications while preserving the numeric state bound.

Preamble

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
import Definitions.Def_ResourceScheduling_Graph_RAMFields
import Definitions.Def_ResourceScheduling_Graph_RAMSafe
open ResourceScheduling.Graph GraphReg GraphProgram

Formal statement

namespace ResourceScheduling.Graph
theorem validate_row (B N : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
    (hi : s.val i ≤ N) (hn : s.val n = N) (hB : N * N + N ≤ B) (hpos : 1 ≤ B) :
    RAMSafe validateRow B s ∧ (validateRow.eval s).val good =
      if s.word.getD (s.val i * N + s.val i) Letter.sep ≠ Letter.one ∧
        ∀ j < N, s.word.getD (s.val i * N + j) Letter.sep = Letter.one →
          s.word.getD (j * N + s.val i) Letter.sep = Letter.one then s.val good else 0 := by sorry
end ResourceScheduling.Graph

Source

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.

View graph