One-prefix work-tape loop combinator — definitions

TM.forWorkOnesTM driverIdx body scans a work tape from left to right and invokes body once for each consecutive 1 symbol. The driver advances before each invocation and halts with its head on the first non-1 symbol. This is the machine-level control needed to consume the unary-width prefix of a self-delimiting binary word without materializing the prefix elsewhere.

Exact iteration semantics require body to preserve the already-advanced driver tape and head. The combinator itself is a concrete TM; loop certificates and proofs live in the adjacent internal and surface modules.

inductive Complexity.TM.ForWorkOnesPhase : Type

Driver states for a consecutive-one work-tape loop.

• scan : ForWorkOnesPhase
• done : ForWorkOnesPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqForWorkOnesPhase : DecidableEq ForWorkOnesPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeForWorkOnesPhase : Fintype ForWorkOnesPhase

ForWorkOnesPhase has exactly two states.

Equations

• Complexity.TM.instFintypeForWorkOnesPhase = { elems := {Complexity.TM.ForWorkOnesPhase.scan, Complexity.TM.ForWorkOnesPhase.done}, complete := ⋯ }

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

Advance over one 1 on work tape driverIdx and invoke body; halt on the first non-1 symbol. An initial left marker is skipped safely.

Equations

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

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

Exact remaining time for a one-prefix loop whose body takes bodyTime value steps on iteration value. The terminal non-one exit takes one step.

Equations

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

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

Wrapper-free exact-control certificate for a consecutive-one work loop.

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

  Canonical scanner configuration at iteration value.

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

  Canonical combined-machine configuration at body entry.

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

  Canonical combined-machine configuration after the exact body run.

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

  Canonical final driver configuration.

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

  One scanner step consumes a 1 and enters the body.

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

  The body has the advertised exact runtime.

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

  The preserving seam returns to the scanner.

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

  The scanner exits on the first non-1 symbol.