Register bounds for the streaming Tseitin transformation

This proof-only module bounds every natural number retained by the streaming transducer. A successful token step raises the largest retained value by at most one, so a run is bounded by its initial state plus the number of tokens consumed. The concrete reduction machine uses this invariant to select one uniform register-operation budget for its entire input scan.

def Complexity.SAT.ThreeSAT.Streaming.Pending.maxValue : Pending → ℕ

Largest variable index retained by a pending-clause window.

Equations

• Complexity.SAT.ThreeSAT.Streaming.Pending.zero.maxValue = 0
• (Complexity.SAT.ThreeSAT.Streaming.Pending.one a).maxValue = a.var
• (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b).maxValue = max a.var b.var
• (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c).maxValue = max a.var (max b.var c.var)

def Complexity.SAT.ThreeSAT.Streaming.Scan.maxValue : Scan → ℕ

Variable counter retained by the raw-literal scanner.

Equations

• Complexity.SAT.ThreeSAT.Streaming.Scan.boundary.maxValue = 0
• (Complexity.SAT.ThreeSAT.Streaming.Scan.literal sign var).maxValue = var

def Complexity.SAT.ThreeSAT.Streaming.State.maxValue (st : State) : ℕ

Largest natural number retained anywhere in a streaming state.

Equations

• st.maxValue = max st.next (max st.pending.maxValue st.scan.maxValue)

theorem Complexity.SAT.ThreeSAT.Streaming.maxValue_step_le_internal {st st' : State} {tok : EncToken} (hstep : step st tok = some st') : st'.maxValue ≤ st.maxValue + 1

One successful token step raises the largest retained value by at most one. Output growth is deliberately absent: emitted bits are not work-register contents.

theorem Complexity.SAT.ThreeSAT.Streaming.maxValue_run_le_internal {st st' : State} {toks : List EncToken} (hrun : run st toks = some st') : st'.maxValue ≤ st.maxValue + toks.length

A successful run raises the largest retained value by at most the number of tokens consumed.