Spin Trace: A Time-Based Invariant for Irreducible Determination in SAT

We introduce a time-based lower-bound principle for computation, formalized as Spin Trace, an invariant that counts irreducible closure events transforming undefined time into determined time. Spin Trace is defined via Minimal Closure, the minimum number of closure events required to determine the outcome of a computation, and is formulated to be independent of the underlying computational model. We show that closure events are non-commutative with local Gate actions and cannot be eliminated by reordering, parallelization, or circuit-level optimizations. Focusing on SAT, we analyze unsatisfiable instances through minimal unsatisfiable subformulas (MUS) and introduce Peeling Length, a measure of how many local closures can be performed before unresolved structure necessarily re-emerges. For Tseitintype MUS constructed on expanding graphs, we establish a boundary re-emergence phenomenon: any local closure induces new unresolved regions at the boundary, forcing additional closure events. This yields families of instances for which Spin Trace grows with the input size. We further show that boundary re-emergence enforces a lower bound on the number of concurrently unresolved variables, implying lower bounds on Resolution width and, via standard size–width trade-offs, on proof length. These results establish Spin Trace as a robust invariant for irreducible determination in SAT and proof complexity, capturinglower-bound phenomena independent of specific proof systems.