Concrete read paths for the Tseitin streaming controller

This file proves the input-reader plumbing of validEmitterTM. Every SAT token occupies two input bits. Starting in a first-bit read state, the controller reads those bits in exactly two steps, advances the input head twice, and reaches the state selected by scheduleToken; parked work and output tapes are unchanged. A first-bit read of the trailing blank reaches controllerDone in one step with all tapes unchanged.

The scheduled state is not interpreted here. Child execution and pure token semantics remain separate layers.

Main results

• validEmitterTM_read_token_reachesIn_internal
• validEmitterTM_read_blank_step_internal
• validEmitterTM_read_blank_reachesIn_internal

Token-bit framing

def Complexity.SAT.ThreeSAT.Machine.tokenFirstBit : EncToken → Bool

First concrete bit of a SAT encoding token.

Equations

• Complexity.SAT.ThreeSAT.Machine.tokenFirstBit (Complexity.SAT.EncToken.bit b) = b
• Complexity.SAT.ThreeSAT.Machine.tokenFirstBit Complexity.SAT.EncToken.litSep = false
• Complexity.SAT.ThreeSAT.Machine.tokenFirstBit Complexity.SAT.EncToken.clauseSep = true

def Complexity.SAT.ThreeSAT.Machine.tokenSecondBit : EncToken → Bool

Second concrete bit of a SAT encoding token.

Equations

• Complexity.SAT.ThreeSAT.Machine.tokenSecondBit (Complexity.SAT.EncToken.bit b) = b
• Complexity.SAT.ThreeSAT.Machine.tokenSecondBit Complexity.SAT.EncToken.litSep = true
• Complexity.SAT.ThreeSAT.Machine.tokenSecondBit Complexity.SAT.EncToken.clauseSep = false

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.token_encode_eq_bits (tok : EncToken) : tok.encode = [tokenFirstBit tok, tokenSecondBit tok]

The named token bits are exactly the existing concrete token encoding.

theorem Complexity.SAT.ThreeSAT.Machine.tokenOfPair_token_bits (tok : EncToken) : tokenOfPair (tokenFirstBit tok) (tokenSecondBit tok) = tok

Decoding the two named encoding bits recovers the token.

def Complexity.SAT.ThreeSAT.Machine.InputTokenAt (input : Tape) (tok : EncToken) : Prop

The input head and its right neighbor contain the encoding of tok.

Equations

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

Read configurations

def Complexity.SAT.ThreeSAT.Machine.controllerSecondCfg {Q : Type} (mode : StreamMode) (first : Bool) (c : Cfg workTapeCount Q) : Cfg workTapeCount validEmitterTM.Q

Controller configuration after reading the first bit of a token.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) : Cfg workTapeCount validEmitterTM.Q

Controller configuration after reading a complete token.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.controllerDoneCfg {Q : Type} (c : Cfg workTapeCount Q) : Cfg workTapeCount validEmitterTM.Q

Halting controller configuration that shares all tapes with c.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerDoneCfg c = { state := Complexity.SAT.ThreeSAT.Machine.controllerDone, input := c.input, work := c.work, output := c.output }

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg_input_head {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) : (controllerScheduledCfg mode tok c).input.head = c.input.head + 2

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg_input_cells {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) : (controllerScheduledCfg mode tok c).input.cells = c.input.cells

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg_work {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) : (controllerScheduledCfg mode tok c).work = c.work

@[simp]

theorem Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg_output {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) : (controllerScheduledCfg mode tok c).output = c.output

The two bit-reading steps

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_read_first_step_internal {Q : Type} (mode : StreamMode) (bit : Bool) (c : Cfg workTapeCount Q) (hread : c.input.read = Γ.ofBool bit) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerReadCfg mode c) = some (controllerSecondCfg mode bit c)

Read the first nonblank input bit, advancing right and preserving parked work and output tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_read_second_step_internal {Q : Type} (mode : StreamMode) (first second : Bool) (c : Cfg workTapeCount Q) (hread : (c.input.move Dir3.right).read = Γ.ofBool second) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerSecondCfg mode first c) = some (controllerScheduledCfg mode (tokenOfPair first second) c)

Read the second nonblank input bit, schedule its decoded token, advance right, and preserve parked work and output tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_read_token_reachesIn_internal {Q : Type} (mode : StreamMode) (tok : EncToken) (c : Cfg workTapeCount Q) (hinput : InputTokenAt c.input tok) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.reachesIn 2 (controllerReadCfg mode c) (controllerScheduledCfg mode tok c)

Reading the two concrete bits of tok schedules that token in exactly two controller steps. The endpoint records exact head/cell and tape framing.

Trailing blank

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_read_blank_step_internal {Q : Type} (mode : StreamMode) (c : Cfg workTapeCount Q) (hread : c.input.read = Γ.blank) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerReadCfg mode c) = some (controllerDoneCfg c)

A blank in first-bit mode halts the controller in one step and preserves the input and all parked work/output tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_read_blank_reachesIn_internal {Q : Type} (mode : StreamMode) (c : Cfg workTapeCount Q) (hread : c.input.read = Γ.blank) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.reachesIn 1 (controllerReadCfg mode c) (controllerDoneCfg c)

Exact one-step reachability form of the first-bit blank transition.