Dense public-input lookup -- definitions

These finite controllers are the concrete bridge from a sparse mutable RAM overlay to the immutable public input on the Turing input tape. The scan keeps a binary countdown on a work tape. When that countdown first reaches zero, the preceding input symbol is copied to a canonical Boolean result tape.

inductive Complexity.RAM.RegisterStore.Machine.DenseInputIdlePhase : Type

Two-state framed identity used as a direct-branch leaf.

• run : DenseInputIdlePhase
• done : DenseInputIdlePhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqDenseInputIdlePhase : DecidableEq DenseInputIdlePhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqDenseInputIdlePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeDenseInputIdlePhase : Fintype DenseInputIdlePhase

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputIdleTM {n : ℕ} : TM n

A one-step identity on every parked tape.

Equations

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

inductive Complexity.RAM.RegisterStore.Machine.DenseInputCapturePhase : Type

Two-step controller that moves left to the preceding input symbol, copies that Boolean value to one work cell, and restores the input head.

• moveLeft : DenseInputCapturePhase
• write : DenseInputCapturePhase
• done : DenseInputCapturePhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqDenseInputCapturePhase : DecidableEq DenseInputCapturePhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqDenseInputCapturePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeDenseInputCapturePhase : Fintype DenseInputCapturePhase

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputBitTape (bit : Bool) : Tape

Canonical binary work tape representing one public-input bit.

Equations

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

def Complexity.RAM.RegisterStore.Machine.capturePreviousInputBitTM {n : ℕ} (result : Fin n) : TM n

Copy the Boolean input symbol immediately to the left of the current head onto a blank canonical result tape, restoring the input head in two steps.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputStepTM {n : ℕ} (counter result : Fin n) : TM n

One input-scan body step. A zero countdown is stationary. A positive countdown is decremented; when it becomes zero, the preceding input bit is captured exactly once.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputStepTime (remaining : ℕ) : ℕ

Exact body time as a function of the positive-or-zero countdown.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputStepResult (remaining : ℕ) (bit : Bool) (current : Tape) : Tape

Result tape after one scan iteration. Only the transition from countdown one to zero captures the current input bit.

Equations

• Complexity.RAM.RegisterStore.Machine.denseInputStepResult remaining bit current = if remaining = 1 then Complexity.RAM.RegisterStore.Machine.denseInputBitTape bit else current

def Complexity.RAM.RegisterStore.Machine.denseInputScanTM {n : ℕ} (counter result : Fin n) : TM n

Scan the entire immutable Boolean input while decrementing a canonical binary address counter and capturing the addressed bit.

Equations

• Complexity.RAM.RegisterStore.Machine.denseInputScanTM counter result = (Complexity.RAM.RegisterStore.Machine.denseInputStepTM counter result).forInputTM

def Complexity.RAM.RegisterStore.Machine.denseInputScanTime (inputLength address : ℕ) : ℕ

Exact complete input-scan time from a positive address.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputLookupTM {n : ℕ} (query counter result scratch : Fin n) : TM n

Full positive-address dense-bank fallback: copy the query into a private countdown, scan the immutable input, rewind the input head, and clear the countdown back to the reusable blank boundary.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInputLookupTime (inputLength address : ℕ) : ℕ

Complete fallback budget, including all three sequencing seams.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.DenseInputLookupReady {n : ℕ} (query counter result scratch : Fin n) (address : ℕ) (work : Fin n → Tape) : Prop

Reusable work-tape boundary before a positive-address dense-bank lookup.

• query : (work query).HasBinaryNat address
• counter : (work counter).HasBinaryNat 0
• result : (work result).HasBinaryNat 0
• scratch : (work scratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (work i)

structure Complexity.RAM.RegisterStore.Machine.DenseInputLookupResult {n : ℕ} (query counter result scratch : Fin n) (input : List Bool) (address : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Reusable work-tape endpoint after dense-bank fallback.

• query_eq : finalWork query = initialWork query
• counter_zero : (finalWork counter).HasBinaryNat 0
• result_value : (finalWork result).HasBinaryNat (initRegs input address)
• scratch_eq : finalWork scratch = initialWork scratch
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : i ≠ query → i ≠ counter → i ≠ result → i ≠ scratch → finalWork i = initialWork i