Coarse runtime bounds for the streaming Tseitin controller

This proof-only module rounds the token-level state bounds and the concrete register-operation bounds to one uniform controller budget. For an input of bit length n, every state reached along a valid typed token prefix has all six register values below 2 * (n + 1). One controller token therefore fits within sixteen copies of TM.opBudget at that cap, including sequencing overhead. The complete token pass is bounded by an explicit quartic.

Main results

• two_mul_tokens_length_eq_encode_length_internal
• streaming_maxValue_run_prefix_le_internal
• bufferValues_run_prefix_bounded_internal
• commitLiteralTime_le_controllerTokenBudget_internal
• closeClauseTime_le_controllerTokenBudget_internal
• controllerRunBudget_le_quartic_internal
• typed_controllerRun_le_quartic_internal

Token count and streaming-state bounds

theorem Complexity.SAT.ThreeSAT.Machine.encodeTokens_length_internal (toks : List EncToken) : (encodeTokens toks).length = 2 * toks.length

Every concrete token contributes exactly two encoded bits.

theorem Complexity.SAT.ThreeSAT.Machine.two_mul_tokens_length_eq_encode_length_internal (φ : CNF) : 2 * φ.tokens.length = φ.encode.length

The token count of a typed CNF is exactly half its concrete bit length.

theorem Complexity.SAT.ThreeSAT.Machine.tokens_length_le_encode_length_internal (φ : CNF) : φ.tokens.length ≤ φ.encode.length

In particular, the number of typed tokens is at most the bit length.

def Complexity.SAT.ThreeSAT.Machine.controllerValueCap (inputLength : ℕ) : ℕ

One cap used for every unary register during a valid controller run.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerValueCap inputLength = 2 * (inputLength + 1)

def Complexity.SAT.ThreeSAT.Machine.BufferValues.BoundedBy (v : BufferValues) (cap : ℕ) : Prop

All six concrete buffer-register values lie below a common cap.

Equations

• v.BoundedBy cap = (v.fresh ≤ cap ∧ v.current ≤ cap ∧ v.a ≤ cap ∧ v.b ≤ cap ∧ v.c ≤ cap ∧ v.scratch ≤ cap)

theorem Complexity.SAT.ThreeSAT.Machine.BufferValues.BoundedBy.mono {v : BufferValues} {cap cap' : ℕ} (h : v.BoundedBy cap) (hcap : cap ≤ cap') : v.BoundedBy cap'

A buffer bound can be enlarged.

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_ofStreaming_boundedBy_maxValue_internal (st : Streaming.State) : (BufferValues.ofStreaming st).BoundedBy st.maxValue

The machine-register representation of a pure state is bounded by that state's maxValue.

theorem Complexity.SAT.ThreeSAT.Machine.streaming_maxValue_run_prefix_le_internal {z : List Bool} (φ : CNF) (hz : z = φ.encode) {pre suffix : List EncToken} {st : Streaming.State} (hsplit : φ.tokens = pre ++ suffix) (hrun : Streaming.run (Streaming.initial (z.length + 1)) pre = some st) : st.maxValue ≤ controllerValueCap z.length

Every successful state reached along a prefix of a typed CNF token stream fits the global input-length cap.

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_run_prefix_bounded_internal {z : List Bool} (φ : CNF) (hz : z = φ.encode) {pre suffix : List EncToken} {st : Streaming.State} (hsplit : φ.tokens = pre ++ suffix) (hrun : Streaming.run (Streaming.initial (z.length + 1)) pre = some st) : (BufferValues.ofStreaming st).BoundedBy (controllerValueCap z.length)

The corresponding six unary-register values fit the same prefix-global cap.

Uniform per-token register budget

def Complexity.SAT.ThreeSAT.Machine.controllerTokenBudget (cap : ℕ) : ℕ

A deliberately coarse budget for every controller action associated with one input token.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerTokenBudget cap = 16 * (Complexity.TM.opBudget cap + 1)

theorem Complexity.SAT.ThreeSAT.Machine.clauseTime_le_four_opBudgets_internal {a b c cap : ℕ} (ha : a ≤ cap) (hb : b ≤ cap) (hc : c ≤ cap) : clauseTime a b c ≤ 4 * (TM.opBudget cap + 1)

Three literal emissions and their small sequencing overhead fit within four augmented operation budgets.

theorem Complexity.SAT.ThreeSAT.Machine.pendingTime_le_nine_opBudgets_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : pendingTime pending v ≤ 9 * (TM.opBudget cap + 1)

The largest pending-clause emission is the empty-clause two-clause gadget, bounded by nine augmented operation budgets.

theorem Complexity.SAT.ThreeSAT.Machine.clearBuffersTime_le_four_opBudgets_internal (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : clearBuffersTime v ≤ 4 * (TM.opBudget cap + 1)

Clearing the four literal buffers fits within four augmented operation budgets.

theorem Complexity.SAT.ThreeSAT.Machine.rollWideBuffersTime_le_five_opBudgets_internal (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : rollWideBuffersTime v ≤ 5 * (TM.opBudget cap + 1)

The three copies, increment, and clear in a wide-window rotation fit within five augmented operation budgets.

theorem Complexity.SAT.ThreeSAT.Machine.commitLiteralTime_le_ten_opBudgets_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : commitLiteralTime pending v ≤ 10 * (TM.opBudget cap + 1)

Every literal-commit branch fits within ten augmented operation budgets, well below the uniform per-token allowance.

theorem Complexity.SAT.ThreeSAT.Machine.closeClauseTime_add_three_le_controllerTokenBudget_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : closeClauseTime pending v + 3 ≤ controllerTokenBudget cap

The close-clause branch is the worst token action. Its structural time plus two bit reads and the child-return step still fits the uniform allowance.

theorem Complexity.SAT.ThreeSAT.Machine.closeClauseTime_le_controllerTokenBudget_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : closeClauseTime pending v ≤ controllerTokenBudget cap

The structural close-clause time alone fits the per-token allowance.

theorem Complexity.SAT.ThreeSAT.Machine.commitLiteralTime_le_controllerTokenBudget_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : commitLiteralTime pending v ≤ controllerTokenBudget cap

Literal commits also fit the same uniform per-token allowance.

theorem Complexity.SAT.ThreeSAT.Machine.commitLiteralTime_add_three_le_controllerTokenBudget_internal (pending : PendingSigns) (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : commitLiteralTime pending v + 3 ≤ controllerTokenBudget cap

A literal commit together with both bit reads and the child-return step fits the uniform per-token allowance.

theorem Complexity.SAT.ThreeSAT.Machine.unaryUpdateTime_current_add_three_le_controllerTokenBudget_internal (v : BufferValues) {cap : ℕ} (hv : v.BoundedBy cap) : unaryUpdateTime v.current + 3 ≤ controllerTokenBudget cap

Incrementing the current literal counter, including both input reads and the child-return step, fits the uniform per-token allowance.

Quartic whole-run budget

def Complexity.SAT.ThreeSAT.Machine.controllerRunBudget (inputLength : ℕ) : ℕ

Token processing plus one sequencing step per token and a final halt.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.ThreeSAT.Machine.opBudget_controllerValueCap_eq_internal (n : ℕ) : TM.opBudget (controllerValueCap n) = 256 * (n + 2) ^ 3

At the input-derived cap, the cubic register budget has a simple closed form.

theorem Complexity.SAT.ThreeSAT.Machine.controllerTokenBudget_valueCap_le_cubic_internal (n : ℕ) : controllerTokenBudget (controllerValueCap n) + 1 ≤ 8192 * (n + 2) ^ 3

The augmented per-token budget is bounded by a convenient cubic.

theorem Complexity.SAT.ThreeSAT.Machine.controllerRunBudget_le_quartic_internal (n : ℕ) : controllerRunBudget n ≤ 16384 * (n + 2) ^ 4

The full controller pass has an explicit quartic time envelope.

theorem Complexity.SAT.ThreeSAT.Machine.typed_controllerRun_le_quartic_internal {z : List Bool} (φ : CNF) (hz : z = φ.encode) : (φ.tokens.length + 1) * (controllerTokenBudget (controllerValueCap z.length) + 1) + 1 ≤ 16384 * (z.length + 2) ^ 4

For a typed input z = φ.encode, even charging one controller allowance for every token and one terminal action lies below the same quartic.