Semantic glue for the streaming Tseitin controller

This proof-only module identifies the register and output updates exposed by Machine.Internal.BufferSpecs with the corresponding pure transitions in ThreeSAT.Streaming. No concrete Turing-machine execution is simulated here. The results are definitional seams used by the later controller induction.

Main results

• literalBits_eq_encodeTokens_literal_internal
• clauseBits_eq_encodeTokens_clause_internal
• bufferValues_startLiteral_internal
• bufferValues_incrementLiteral_internal
• bufferValues_committed_eq_pushLiteral_internal
• commitBits_eq_pushLiteral_emitted_internal
• bufferValues_closed_eq_closeClause_internal
• pendingBits_eq_closeClause_emitted_internal

Canonical encodings of emitted chunks

theorem Complexity.SAT.ThreeSAT.Machine.literalBits_eq_encodeTokens_literal_internal (sign : Bool) (var : ℕ) : literalBits sign var = encodeTokens (Clause.tokens [{ sign := sign, var := var }])

The literal chunk used by emitLitTM is exactly the canonical token encoding of one completed literal.

theorem Complexity.SAT.ThreeSAT.Machine.clauseBits_eq_encodeTokens_clause_internal (aSign : Bool) (a : ℕ) (bSign : Bool) (b : ℕ) (cSign : Bool) (c : ℕ) : clauseBits aSign a bSign b cSign c = encodeTokens (CNF.tokens [[{ sign := aSign, var := a }, { sign := bSign, var := b }, { sign := cSign, var := c }]])

The clause chunk used by emitClauseTM is exactly the canonical token encoding of one exact-three-literal CNF clause.

Simple scanner transitions

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_startLiteral_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) : BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted } = BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.literal sign 0, emitted := emitted }

Reading a sign bit at a clause boundary starts a zero-valued literal and does not change any register value.

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_incrementLiteral_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) (var : ℕ) : (have __src := BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted }; { fresh := __src.fresh, current := var + 1, a := __src.a, b := __src.b, c := __src.c, scratch := __src.scratch }) = BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.literal sign (var + 1), emitted := emitted }

Reading a unary true body bit increments exactly the current-literal register.

theorem Complexity.SAT.ThreeSAT.Machine.streaming_step_boundary_bit_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) : Streaming.step { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted } (EncToken.bit sign) = some { next := next, pending := pending, scan := Streaming.Scan.literal sign 0, emitted := emitted }

Pure boundary-bit transition, stated in the form consumed by the controller token induction.

theorem Complexity.SAT.ThreeSAT.Machine.streaming_step_literal_true_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) (var : ℕ) : Streaming.step { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted } (EncToken.bit true) = some { next := next, pending := pending, scan := Streaming.Scan.literal sign (var + 1), emitted := emitted }

Pure unary-body transition corresponding to incRegTM currentReg.

Literal commit

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_committed_eq_pushLiteral_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) (var : ℕ) : BufferValues.committed (PendingSigns.ofStreaming pending) (BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted }) = BufferValues.ofStreaming (Streaming.pushLiteral { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted } { sign := sign, var := var })

The post-register tuple of commitLiteralTM is exactly the register representation of the pure pushLiteral result.

theorem Complexity.SAT.ThreeSAT.Machine.commitBits_eq_pushLiteral_emitted_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) (sign : Bool) (var : ℕ) : encodeTokens emitted ++ commitBits (PendingSigns.ofStreaming pending) (BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted }) = encodeTokens (Streaming.pushLiteral { next := next, pending := pending, scan := Streaming.Scan.literal sign var, emitted := emitted } { sign := sign, var := var }).emitted

The bits appended by commitLiteralTM turn the old pure output accumulator into exactly the pushLiteral accumulator.

Clause close

theorem Complexity.SAT.ThreeSAT.Machine.bufferValues_closed_eq_closeClause_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) : BufferValues.closed (PendingSigns.ofStreaming pending) (BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted }) = BufferValues.ofStreaming (Streaming.closeClause { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted })

Closing a pure pending window produces exactly the post-register tuple specified by closeClauseTM.

theorem Complexity.SAT.ThreeSAT.Machine.pendingBits_eq_to3CNF_tokens_internal (next : ℕ) (pending : Streaming.Pending) : pendingBits (PendingSigns.ofStreaming pending) (BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := [] }) = encodeTokens (Clause.to3CNF next pending.toClause).tokens

The chunk selected by pendingBits is the canonical token encoding of the pure pending clause's exact-three transformation.

theorem Complexity.SAT.ThreeSAT.Machine.pendingBits_eq_closeClause_emitted_internal (next : ℕ) (pending : Streaming.Pending) (emitted : List EncToken) : encodeTokens emitted ++ pendingBits (PendingSigns.ofStreaming pending) (BufferValues.ofStreaming { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted }) = encodeTokens (Streaming.closeClause { next := next, pending := pending, scan := Streaming.Scan.boundary, emitted := emitted }).emitted

Appending pendingBits to the represented output accumulator yields exactly the output accumulator of Streaming.closeClause.