Documentation

Complexitylib.Circuits.Encoding.Machine.Core.Internal.Action

Projection lemmas for streaming evaluator actions #

These narrowly oriented rewrites expose the named code, wire, and counter actions behind the finite-index projections used by TM.δ. They keep later one-step proofs independent of the implementation's nested index tests.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workWrite_codeIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workWrite codeIdx = action.code.write

Projecting the code-tape write exposes the named code action.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workWrite_wiresIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workWrite wiresIdx = action.wires.write

Projecting the wire-tape write exposes the named wire action.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workWrite_counterIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workWrite counterIdx = action.counter.write

Projecting the counter-tape write exposes the named counter action.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workDir_codeIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workDir codeIdx = action.code.dir

Projecting the code-tape direction exposes the named code action.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workDir_wiresIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workDir wiresIdx = action.wires.dir

Projecting the wire-tape direction exposes the named wire action.

source
@[simp]
theorem Complexity.CircuitCode.Machine.Internal.workDir_counterIdx {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) :
action.workDir counterIdx = action.counter.dir

Projecting the counter-tape direction exposes the named counter action.

source
theorem Complexity.CircuitCode.Machine.Internal.evalFamilyCoreTM_step (c : Cfg workTapeCount evalFamilyCoreTM.Q) (hstate : c.state ≠ CorePhase.done) :
evalFamilyCoreTM.step c = have action := coreAction c.state (fun (i : Fin workTapeCount) => (c.work i).read) c.output.read; some { state := action.next, input := c.input.move (TM.idleDir c.input.read), work := fun (i : Fin workTapeCount) => (c.work i).writeAndMove (action.workWrite i).toΓ (action.workDir i), output := c.output.writeAndMove action.output.write.toΓ action.output.dir }

Unfold one nonhalting evaluator step through its named CoreAction.