Child-execution lifting for the Tseitin streaming controller

The concrete streaming controller runs three families of child machines: unary increments, literal commits, and clause closes. This file proves only the control-flow plumbing for those calls. A child step and hence an exact reachesIn trace lift into validEmitterTM while all tapes are shared literally. Once a child reaches its halt state, one controller step returns to the appropriate first-bit read mode.

The generic return lemmas expose the standard phase-boundary tape operations TM.transitionInput and TM.transitionTape. Parked specializations show that these operations are identities in the register invariants used later.

No token semantics are proved here.

Main results

• validEmitterTM_increment_reachesIn_internal
• validEmitterTM_commit_reachesIn_internal
• validEmitterTM_close_reachesIn_internal
• validEmitterTM_increment_return_step_internal
• validEmitterTM_commit_return_step_internal
• validEmitterTM_close_return_step_internal

Configuration embeddings

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

Embed arbitrary tapes into the controller at the first bit of mode.

Equations

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

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

The read continuation after the controller's standard boundary tape transition.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.controllerIncrementCfg (mode : StreamMode) (c : Cfg workTapeCount (TM.incRegTM currentReg).Q) : Cfg workTapeCount validEmitterTM.Q

Embed an increment-child configuration in the controller state space.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.controllerCommitCfg (pending : PendingSigns) (sign : Bool) (c : Cfg workTapeCount (commitLiteralTM pending).Q) : Cfg workTapeCount validEmitterTM.Q

Embed a pending-dependent commit-child configuration in the controller.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.controllerCloseCfg (pending : PendingSigns) (c : Cfg workTapeCount (closeClauseTM pending).Q) : Cfg workTapeCount validEmitterTM.Q

Embed a pending-dependent close-child configuration in the controller.

Equations

• Complexity.SAT.ThreeSAT.Machine.controllerCloseCfg pending c = { state := Complexity.SAT.ThreeSAT.Machine.controllerClose pending c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.SAT.ThreeSAT.Machine.controllerReadTransitionCfg_eq_readCfg_internal {Q : Type} (mode : StreamMode) (c : Cfg workTapeCount Q) (hinp : TM.Parked c.input) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : controllerReadTransitionCfg mode c = controllerReadCfg mode c

A standard boundary transition is the identity on parked tapes.

Increment child

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_increment_step_internal (mode : StreamMode) {c c' : Cfg workTapeCount (TM.incRegTM currentReg).Q} (hstep : (TM.incRegTM currentReg).step c = some c') : validEmitterTM.step (controllerIncrementCfg mode c) = some (controllerIncrementCfg mode c')

One step of the unary increment child is one controller increment-call step with literally identical tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_increment_reachesIn_internal (mode : StreamMode) {t : ℕ} {c c' : Cfg workTapeCount (TM.incRegTM currentReg).Q} (hreach : (TM.incRegTM currentReg).reachesIn t c c') : validEmitterTM.reachesIn t (controllerIncrementCfg mode c) (controllerIncrementCfg mode c')

An exact unary-increment trace lifts point-for-point into the controller.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_increment_return_step_internal (mode : StreamMode) (c : Cfg workTapeCount (TM.incRegTM currentReg).Q) (hhalt : c.state = (TM.incRegTM currentReg).qhalt) : validEmitterTM.step (controllerIncrementCfg mode c) = some (controllerReadTransitionCfg mode c)

A halted increment child returns to the saved parser mode after one standard boundary transition.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_increment_return_parked_step_internal (mode : StreamMode) (c : Cfg workTapeCount (TM.incRegTM currentReg).Q) (hhalt : c.state = (TM.incRegTM currentReg).qhalt) (hinp : TM.Parked c.input) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerIncrementCfg mode c) = some (controllerReadCfg mode c)

Parked-tape specialization of the increment-child return step.

Commit child

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_commit_step_internal (pending : PendingSigns) (sign : Bool) {c c' : Cfg workTapeCount (commitLiteralTM pending).Q} (hstep : (commitLiteralTM pending).step c = some c') : validEmitterTM.step (controllerCommitCfg pending sign c) = some (controllerCommitCfg pending sign c')

One step of a pending-dependent commit child is one controller call step with literally identical tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_commit_reachesIn_internal (pending : PendingSigns) (sign : Bool) {t : ℕ} {c c' : Cfg workTapeCount (commitLiteralTM pending).Q} (hreach : (commitLiteralTM pending).reachesIn t c c') : validEmitterTM.reachesIn t (controllerCommitCfg pending sign c) (controllerCommitCfg pending sign c')

An exact commit-child trace lifts point-for-point into the controller.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_commit_return_step_internal (pending : PendingSigns) (sign : Bool) (c : Cfg workTapeCount (commitLiteralTM pending).Q) (hhalt : c.state = (commitLiteralTM pending).qhalt) : validEmitterTM.step (controllerCommitCfg pending sign c) = some (controllerReadTransitionCfg (StreamMode.boundary (pending.push sign)) c)

A halted commit child returns to the boundary mode containing its pushed sign after one standard boundary transition.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_commit_return_parked_step_internal (pending : PendingSigns) (sign : Bool) (c : Cfg workTapeCount (commitLiteralTM pending).Q) (hhalt : c.state = (commitLiteralTM pending).qhalt) (hinp : TM.Parked c.input) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerCommitCfg pending sign c) = some (controllerReadCfg (StreamMode.boundary (pending.push sign)) c)

Parked-tape specialization of the commit-child return step.

Close child

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_close_step_internal (pending : PendingSigns) {c c' : Cfg workTapeCount (closeClauseTM pending).Q} (hstep : (closeClauseTM pending).step c = some c') : validEmitterTM.step (controllerCloseCfg pending c) = some (controllerCloseCfg pending c')

One step of a pending-dependent close child is one controller call step with literally identical tapes.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_close_reachesIn_internal (pending : PendingSigns) {t : ℕ} {c c' : Cfg workTapeCount (closeClauseTM pending).Q} (hreach : (closeClauseTM pending).reachesIn t c c') : validEmitterTM.reachesIn t (controllerCloseCfg pending c) (controllerCloseCfg pending c')

An exact close-child trace lifts point-for-point into the controller.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_close_return_step_internal (pending : PendingSigns) (c : Cfg workTapeCount (closeClauseTM pending).Q) (hhalt : c.state = (closeClauseTM pending).qhalt) : validEmitterTM.step (controllerCloseCfg pending c) = some (controllerReadTransitionCfg (StreamMode.boundary PendingSigns.zero) c)

A halted close child returns to the empty boundary mode after one standard boundary transition.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_close_return_parked_step_internal (pending : PendingSigns) (c : Cfg workTapeCount (closeClauseTM pending).Q) (hhalt : c.state = (closeClauseTM pending).qhalt) (hinp : TM.Parked c.input) (hwork : ∀ (i : Fin workTapeCount), TM.Parked (c.work i)) (hout : TM.Parked c.output) : validEmitterTM.step (controllerCloseCfg pending c) = some (controllerReadCfg (StreamMode.boundary PendingSigns.zero) c)

Parked-tape specialization of the close-child return step.