Bounded sparse-entry scan

This module exposes the complete time-bounded contract for the fixed sparse store scanner. The runtime entry count is read from a canonical binary tape; it is not hardwired into the finite controller.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_hoareTime_frame {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (queryBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) queryBits initialWork initialWork) (hcount : (initialWork tapes.count).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryScanTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryScanOutcome tapes store queryBits initialWork work ∧ out = out₀) (entryScanTime tapes queryBits store)

Scan a runtime-sized sparse store. A successful endpoint contains the first matching entry's decoded value; a miss certifies that every address was different. Input, output, and every work tape outside the ten-tape assignment are preserved exactly.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_isTransducer {n : ℕ} (tapes : EntryScanTapes n) : (entryScanTM tapes).IsTransducer

The bounded scanner preserves one-way output safety.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (queryBits : List Bool) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryScanTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryScanTM tapes).reachesIn time start current) (htime : time ≤ entryScanTime tapes queryBits store) : current.WithinAuxSpace inputLength (initialSpace + entryScanTime tapes queryBits store)

Coarse all-prefix auxiliary-space envelope for the bounded scan.

theorem Complexity.RAM.RegisterStore.Machine.entryScanOneTime_le_linear {n : ℕ} (tapes : EntryScanTapes n) (entry : Entry) (queryBits : List Bool) : entryScanOneTime tapes entry queryBits ≤ 400 * (entry.1.bits.length + entry.2.bits.length + queryBits.length + 1)

One invariant-preserving entry iteration is linear in the two serialized words and the query width.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTime_le_encoded {n : ℕ} (tapes : EntryScanTapes n) (queryBits : List Bool) (store : Store) : entryScanTime tapes queryBits store ≤ 1000 * (encodedStoreLength store + List.length store * (queryBits.length + bitlen (List.length store) + 2) + 1)

A complete sparse scan is charged by the serialized entries actually traversed, the repeated query width, and the binary remaining-count overhead. In particular, it no longer multiplies every entry by a run-wide square-width envelope.