Bounded sparse-entry scan — invariant internals #
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.stepTime_eq_oneTime_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{entry : Entry}
{rest queryBits : List Bool}
{initialWork work : Fin n → Tape}
(h : EntryScanReady tapes.entry (entry.encode ++ rest) queryBits initialWork work)
:
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.rebase_self_internal
{n : ℕ}
{tapes : EntryMatchTapes n}
{remaining queryBits : List Bool}
{initialWork work : Fin n → Tape}
(h : EntryScanReady tapes remaining queryBits initialWork work)
:
EntryScanReady tapes remaining queryBits work work
Forget an older frame base and use the current work family as the exact base for the next loop iteration.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.change_count_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{remaining queryBits : List Bool}
{initialWork work finalWork : Fin n → Tape}
{count : ℕ}
(h : EntryScanReady tapes.entry remaining queryBits initialWork work)
(hother : ∀ (i : Fin n), i ≠ tapes.count → finalWork i = work i)
(hcount : (finalWork tapes.count).HasBinaryNat count)
:
EntryScanReady tapes.entry remaining queryBits finalWork finalWork
Changing only the distinct count tape preserves the entry-loop invariant; the new count representation supplies parkedness for that tape.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.scanFrame_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{remaining queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanReady tapes.entry remaining queryBits initialWork finalWork)
:
EntryScanFrame tapes initialWork finalWork
An entry-ready frame implies the scanner's weaker ten-tape frame.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanHit.scanFrame_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{entry : Entry}
{rest queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanHit tapes.entry entry rest queryBits initialWork finalWork)
:
EntryScanFrame tapes initialWork finalWork
A successful entry endpoint implies the scanner's ten-tape frame.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanFrame.trans_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{work₀ work₁ work₂ : Fin n → Tape}
(h₁ : EntryScanFrame tapes work₀ work₁)
(h₂ : EntryScanFrame tapes work₁ work₂)
:
EntryScanFrame tapes work₀ work₂
Scanner frames compose across loop iterations.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.count_eq_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{remaining queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanReady tapes.entry remaining queryBits initialWork finalWork)
:
The count tape is in the frame of every entry-ready endpoint.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanHit.count_eq_internal
{n : ℕ}
{tapes : EntryScanTapes n}
{entry : Entry}
{rest queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanHit tapes.entry entry rest queryBits initialWork finalWork)
:
The count tape is in the frame of every successful entry endpoint.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanReady.result_read_blank_internal
{n : ℕ}
{tapes : EntryMatchTapes n}
{remaining queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanReady tapes remaining queryBits initialWork finalWork)
:
A restored miss invariant exposes a blank readable result.
theorem
Complexity.RAM.RegisterStore.Machine.EntryScanHit.result_read_one_internal
{n : ℕ}
{tapes : EntryMatchTapes n}
{entry : Entry}
{rest queryBits : List Bool}
{initialWork finalWork : Fin n → Tape}
(h : EntryScanHit tapes entry rest queryBits initialWork finalWork)
:
A successful hit exposes the readable one flag.