Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.EntryUpdate.Internal.Inv

Bounded encoded sparse-store update — invariant internals #

Tape-layout views and frame lemmas used by the semantic update loop. In particular, this file isolates the only controller-local mutation: changing the canonical zero-valued found tape to canonical one after a hit.

source
def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remainingScan {n : ℕ} (tapes : EntryUpdateTapes n) :
EntryScanTapes n

View the update layout as an entry scanner whose count is remaining.

Equations
Instances For
    source
    def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.resultScan {n : ℕ} (tapes : EntryUpdateTapes n) :
    EntryScanTapes n

    View the update layout as an entry scanner whose count is resultCount.

    Equations
    Instances For
      source
      @[simp]
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remainingScan_entry {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.remainingScan.entry = tapes.entry
      source
      @[simp]
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remainingScan_count {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.remainingScan.count = tapes.remaining
      source
      @[simp]
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.resultScan_entry {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.resultScan.entry = tapes.entry
      source
      @[simp]
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.resultScan_count {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.resultScan.count = tapes.resultCount
      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remaining_ne_entry {n : ℕ} (tapes : EntryUpdateTapes n) (i : Fin 9) :
      tapes.remaining ≠ tapes.entry.idx i

      The remaining count is outside every entry-machine tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replacement_ne_entry {n : ℕ} (tapes : EntryUpdateTapes n) (i : Fin 9) :
      tapes.replacement ≠ tapes.entry.idx i

      The replacement source is outside every entry-machine tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.found_ne_entry {n : ℕ} (tapes : EntryUpdateTapes n) (i : Fin 9) :
      tapes.found ≠ tapes.entry.idx i

      The found flag is outside every entry-machine tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.resultCount_ne_entry {n : ℕ} (tapes : EntryUpdateTapes n) (i : Fin 9) :
      tapes.resultCount ≠ tapes.entry.idx i

      The result count is outside every entry-machine tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remaining_ne_replacement {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.remaining ≠ tapes.replacement

      The remaining count and replacement source are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remaining_ne_found {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.remaining ≠ tapes.found

      The remaining count and found flag are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remaining_ne_resultCount {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.remaining ≠ tapes.resultCount

      The remaining and result counts are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replacement_ne_found {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.replacement ≠ tapes.found

      The replacement source and found flag are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replacement_ne_resultCount {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.replacement ≠ tapes.resultCount

      The replacement source and result count are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.found_ne_resultCount {n : ℕ} (tapes : EntryUpdateTapes n) :
      tapes.found ≠ tapes.resultCount

      The found flag and result count are distinct.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork_apply_eq_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) :
      entryUpdateMarkFoundWork tapes work tapes.found = (work tapes.found).writeAndMove Γ.one (TM.idleDir (work tapes.found).read)

      The hit-marking update changes exactly the found tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork_apply_ne_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) (i : Fin n) (hi : i ≠ tapes.found) :
      entryUpdateMarkFoundWork tapes work i = work i

      The hit-marking update preserves every tape other than the found tape.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork_found_one_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) (hfound : (work tapes.found).HasBinaryNat 0) :
      (entryUpdateMarkFoundWork tapes work tapes.found).HasBinaryNat 1

      Writing 1 over the parked canonical zero flag produces canonical one.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateParked_of_hasBinaryNat_internal {t : Tape} {value : ℕ} (h : t.HasBinaryNat value) :
      TM.Parked t

      Canonical natural-number tapes are parked away from the left marker.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork_parked_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) (hfound : (work tapes.found).HasBinaryNat 0) (hparked : ∀ (i : Fin n), TM.Parked (work i)) (i : Fin n) :
      TM.Parked (entryUpdateMarkFoundWork tapes work i)

      Marking a canonical zero found flag preserves parkedness of the complete work family.

      source
      theorem Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork_found_read_one_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) (hfound : (work tapes.found).HasBinaryNat 0) :
      (entryUpdateMarkFoundWork tapes work tapes.found).read = Γ.one

      The marked found flag exposes 1 directly under its parked head.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.frame_outside_entry_internal {n : ℕ} {tapes : EntryUpdateTapes n} {remaining queryBits : List Bool} {initialWork finalWork : Fin n → Tape} (h : EntryScanReady tapes.entry remaining queryBits initialWork finalWork) (i : Fin n) (houtside : ∀ (j : Fin 9), i ≠ tapes.entry.idx j) :
      finalWork i = initialWork i

      The frame component of an entry-ready endpoint can be queried with one uniform proof that an index lies outside the nine entry-machine tapes.

      source
      theorem Complexity.RAM.RegisterStore.Machine.ReadableEntryMatch.frame_outside_entry_internal {n : ℕ} {tapes : EntryUpdateTapes n} {entry : Entry} {rest queryBits : List Bool} {initialWork finalWork : Fin n → Tape} (h : ReadableEntryMatch tapes.entry entry rest queryBits initialWork finalWork) (i : Fin n) (houtside : ∀ (j : Fin 9), i ≠ tapes.entry.idx j) :
      finalWork i = initialWork i

      The frame component of a readable match can be queried uniformly outside the nine entry-machine tapes.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.markFound_internal {n : ℕ} {tapes : EntryUpdateTapes n} {remaining queryBits : List Bool} {initialWork finalWork : Fin n → Tape} (h : EntryScanReady tapes.entry remaining queryBits initialWork finalWork) (hfound : (finalWork tapes.found).HasBinaryNat 0) :
      EntryScanReady tapes.entry remaining queryBits (entryUpdateMarkFoundWork tapes initialWork) (entryUpdateMarkFoundWork tapes finalWork)

      Marking the external found flag preserves an entry-ready invariant while updating both sides of its exact frame.

      source
      theorem Complexity.RAM.RegisterStore.Machine.ReadableEntryMatch.markFound_internal {n : ℕ} {tapes : EntryUpdateTapes n} {entry : Entry} {rest queryBits : List Bool} {initialWork finalWork : Fin n → Tape} (h : ReadableEntryMatch tapes.entry entry rest queryBits initialWork finalWork) (hfound : (finalWork tapes.found).HasBinaryNat 0) :
      ReadableEntryMatch tapes.entry entry rest queryBits (entryUpdateMarkFoundWork tapes initialWork) (entryUpdateMarkFoundWork tapes finalWork)

      Marking the external found flag preserves a readable matched-entry endpoint while updating both sides of its exact frame.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.change_remaining_internal {n : ℕ} {tapes : EntryUpdateTapes 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.remaining → finalWork i = work i) (hcount : (finalWork tapes.remaining).HasBinaryNat count) :
      EntryScanReady tapes.entry remaining queryBits finalWork finalWork

      A frame-rich binary operation on the remaining-count tape preserves and rebases the entry-ready invariant.

      source
      theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.change_resultCount_internal {n : ℕ} {tapes : EntryUpdateTapes 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.resultCount → finalWork i = work i) (hcount : (finalWork tapes.resultCount).HasBinaryNat count) :
      EntryScanReady tapes.entry remaining queryBits finalWork finalWork

      A frame-rich binary operation on the result-count tape preserves and rebases the entry-ready invariant.