Binary work-tape loop combinator -- definitions

TM.forBinaryWorkTM driverIdx body invokes body once for each 0 or 1 under a designated work-tape cursor and stops on the first blank. The body sees the current bit; the loopback seam advances the driver by one cell. This is the width-driven control needed by bitwise algorithms such as schoolbook multiplication, without a numeric-value counter.

inductive Complexity.TM.ForBinaryWorkPhase : Type

Scanner and terminal states outside the nested body machine.

• scan : ForBinaryWorkPhase
• done : ForBinaryWorkPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqForBinaryWorkPhase : DecidableEq ForBinaryWorkPhase

Equations

• Complexity.TM.instDecidableEqForBinaryWorkPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeForBinaryWorkPhase : Fintype ForBinaryWorkPhase

ForBinaryWorkPhase has exactly two states.

Equations

• Complexity.TM.instFintypeForBinaryWorkPhase = { elems := {Complexity.TM.ForBinaryWorkPhase.scan, Complexity.TM.ForBinaryWorkPhase.done}, complete := ⋯ }

def Complexity.TM.forBinaryWorkTM {n : ℕ} (driverIdx : Fin n) (body : TM n) : TM n

Iterate body over the Boolean cells of work tape driverIdx.

The scanner skips an initial left marker, halts on blank, and enters body without moving on either Boolean symbol. When the body halts, one preserving seam step advances only the driver and resumes scanning. Exact once-per-bit semantics therefore requires the body to preserve the driver tape and head.

Equations

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

def Complexity.TM.forBinaryWorkLoopTime (bodyTime : ℕ → ℕ) (value : ℕ) : ℕ → ℕ

Exact remaining time for a bit-driven work loop. Each live iteration takes one scanner step, the body run, and one advancing loopback step; the terminal blank exit takes one step.

Equations

• Complexity.TM.forBinaryWorkLoopTime bodyTime value 0 = 1
• Complexity.TM.forBinaryWorkLoopTime bodyTime value count.succ = 1 + bodyTime value + 1 + Complexity.TM.forBinaryWorkLoopTime bodyTime (value + 1) count

structure Complexity.TM.ForBinaryWorkLoopSpec {n : ℕ} (driverIdx : Fin n) (body : TM n) (bodyTime : ℕ → ℕ) (total : ℕ) : Type

Wrapper-free exact-control certificate for a binary work-tape loop.

• scanCfg : ℕ → Cfg n (forBinaryWorkTM driverIdx body).Q

  Canonical scanner configuration at iteration value.

• bodyStartCfg : ℕ → Cfg n (forBinaryWorkTM driverIdx body).Q

  Canonical combined-machine configuration at body entry.

• bodyDoneCfg : ℕ → Cfg n (forBinaryWorkTM driverIdx body).Q

  Canonical combined-machine configuration after the exact body run.

• doneCfg : Cfg n (forBinaryWorkTM driverIdx body).Q

  Canonical final driver configuration.

• scanStep (value : ℕ) : value < total → (forBinaryWorkTM driverIdx body).step (self.scanCfg value) = some (self.bodyStartCfg value)

  One scanner step on a Boolean cell enters the body.

• bodyRun (value : ℕ) : value < total → (forBinaryWorkTM driverIdx body).reachesIn (bodyTime value) (self.bodyStartCfg value) (self.bodyDoneCfg value)

  The body has the advertised exact runtime.

• loopbackStep (value : ℕ) : value < total → (forBinaryWorkTM driverIdx body).step (self.bodyDoneCfg value) = some (self.scanCfg (value + 1))

  The preserving loopback advances the driver to the next cell.

• stopStep : (forBinaryWorkTM driverIdx body).step (self.scanCfg total) = some self.doneCfg

  The scanner exits on the first blank.

structure Complexity.TM.ForBinaryWorkLoopSpaceSpec {n : ℕ} {driverIdx : Fin n} {body : TM n} {bodyTime : ℕ → ℕ} {total : ℕ} (spec : ForBinaryWorkLoopSpec driverIdx body bodyTime total) (inputLength spaceBound : ℕ) : Prop

Space obligations turning an exact binary-work loop certificate into an all-prefix auxiliary-space certificate.

• scanWithin (value : ℕ) : value ≤ total → (spec.scanCfg value).WithinAuxSpace inputLength spaceBound

  Every canonical scanner configuration is within the space budget.

• doneWithin : spec.doneCfg.WithinAuxSpace inputLength spaceBound

  The canonical terminal configuration is within the space budget.

• bodyPrefixWithin (value t : ℕ) (c : Cfg n (forBinaryWorkTM driverIdx body).Q) : value < total → t ≤ bodyTime value → (forBinaryWorkTM driverIdx body).reachesIn t (spec.bodyStartCfg value) c → c.WithinAuxSpace inputLength spaceBound

  Every prefix of each exact body run remains within the budget.