Dense public-input lookup

This module exposes the fixed leaves used to look through a sparse tagged overlay into the immutable public-input bank.

theorem Complexity.RAM.RegisterStore.Machine.denseInputIdleTM_reachesIn_frame {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n denseInputIdleTM.Q), denseInputIdleTM.reachesIn 1 { state := denseInputIdleTM.qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ denseInputIdleTM.halted c' ∧ c'.input = inp₀ ∧ c'.work = work₀ ∧ c'.output = out₀

The direct-branch identity leaf preserves a fully parked frame exactly.

theorem Complexity.RAM.RegisterStore.Machine.capturePreviousInputBitTM_reachesIn_frame {n : ℕ} (result : Fin n) (bit : Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : inp₀.StartInvariant) (hhead : 2 ≤ inp₀.head) (hbit : inp₀.cells (inp₀.head - 1) = Γ.ofBool bit) (hresult : work₀ result = TM.resetBinaryBlank) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n (capturePreviousInputBitTM result).Q), (capturePreviousInputBitTM result).reachesIn 2 { state := (capturePreviousInputBitTM result).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (capturePreviousInputBitTM result).halted c' ∧ c'.input = inp₀ ∧ c'.work = Function.update work₀ result (denseInputBitTape bit) ∧ c'.output = out₀

Copy the preceding Boolean input symbol into one canonical work tape and restore the read-only input head in exactly two transitions.

theorem Complexity.RAM.RegisterStore.Machine.denseInputBitTape_hasBinaryNat (bit : Bool) : (denseInputBitTape bit).HasBinaryNat (if bit = true then 1 else 0)

The canonical captured-bit tape represents exactly zero or one.

theorem Complexity.RAM.RegisterStore.Machine.denseInputBitTape_parked (bit : Bool) : TM.Parked (denseInputBitTape bit)

Every captured-bit tape is parked at its first data cell.

theorem Complexity.RAM.RegisterStore.Machine.denseInputStepTM_reachesIn_frame {n : ℕ} (counter result : Fin n) (hne : counter ≠ result) (remaining : ℕ) (bit : Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : inp₀.StartInvariant) (hhead : 2 ≤ inp₀.head) (hbit : inp₀.cells (inp₀.head - 1) = Γ.ofBool bit) (hcounter : (work₀ counter).HasBinaryNat remaining) (hresult : remaining = 1 → work₀ result = TM.resetBinaryBlank) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n (denseInputStepTM counter result).Q), (denseInputStepTM counter result).reachesIn (denseInputStepTime remaining) { state := (denseInputStepTM counter result).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (denseInputStepTM counter result).halted c' ∧ c'.input = inp₀ ∧ (c'.work counter).HasBinaryNat (remaining - 1) ∧ c'.work result = denseInputStepResult remaining bit (work₀ result) ∧ (∀ (i : Fin n), i ≠ counter → i ≠ result → c'.work i = work₀ i) ∧ c'.output = out₀

One scan body step decrements a positive countdown, captures the preceding input bit exactly when the countdown reaches zero, and preserves every frame.

theorem Complexity.RAM.RegisterStore.Machine.denseInputScanTM_reachesIn_frame {n : ℕ} (counter result : Fin n) (hne : counter ≠ result) (input : List Bool) (address : ℕ) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : address ≠ 0) (hcounter : (work₀ counter).HasBinaryNat address) (hresult : work₀ result = TM.resetBinaryBlank) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n (denseInputScanTM counter result).Q), (denseInputScanTM counter result).reachesIn (denseInputScanTime input.length address) { state := (denseInputScanTM counter result).qstart, input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := work₀, output := out₀ } c' ∧ (denseInputScanTM counter result).halted c' ∧ c'.input.head = input.length + 1 ∧ c'.input.cells = (Tape.init (List.map Γ.ofBool input)).cells ∧ (c'.work counter).HasBinaryNat (address - input.length) ∧ (c'.work result).HasBinaryNat (initRegs input address) ∧ (∀ (i : Fin n), i ≠ counter → i ≠ result → c'.work i = work₀ i) ∧ c'.output = out₀

A positive RAM address can be looked up by one exact scan of the immutable input bank. The scanner leaves the input contents unchanged, parks at the first blank, decrements its counter once per bit, and returns RAM.initRegs.

theorem Complexity.RAM.RegisterStore.Machine.denseInputScanTime_le_width (inputLength address : ℕ) : denseInputScanTime inputLength address ≤ inputLength * (2 * address.size + 9) + 1

Dense-bank lookup is linear in the public-input length and logarithmic in the queried positive address.

theorem Complexity.RAM.RegisterStore.Machine.denseInputLookupTM_hoareTime {n : ℕ} (query counter result scratch : Fin n) (hqc : query ≠ counter) (hqr : query ≠ result) (hqs : query ≠ scratch) (hcr : counter ≠ result) (hcs : counter ≠ scratch) (hrs : result ≠ scratch) (input : List Bool) (address : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (haddress : address ≠ 0) (hready : DenseInputLookupReady query counter result scratch address initialWork) (houtput : TM.Parked out₀) : (denseInputLookupTM query counter result scratch).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInputLookupResult query counter result scratch input address initialWork work ∧ out = out₀) (denseInputLookupTime input.length address)

Full dense-bank fallback preserves the query and scratch tapes, restores the input head and countdown tape, and returns the standard RAM input value.