RAM sparse-entry matching — proof internals

theorem Complexity.RAM.RegisterStore.Machine.entryMatchTM_reachesIn_frame_internal {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ tapes.source).HasBinarySuffix (entry.encode ++ rest)) (haddress : (work₀ tapes.address).HasBinaryPrefix []) (hvalue : (work₀ tapes.value).HasBinaryPrefix []) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (haddressCounter : (work₀ tapes.addressCounter).HasBinaryNat 0) (haddressWidth : (work₀ tapes.addressWidth).HasBinaryNat 0) (hvalueCounter : (work₀ tapes.valueCounter).HasBinaryNat 0) (hvalueWidth : (work₀ tapes.valueWidth).HasBinaryNat 0) (hquery : (work₀ tapes.query).HasBinaryString queryBits) (hqueryStart : (work₀ tapes.query).cells 0 = Γ.start) (hresult : (work₀ tapes.result).HasBinaryPrefix []) (hresultStart : (work₀ tapes.result).cells 0 = Γ.start) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n (entryMatchTM tapes).Q), ∃ t ≤ entryMatchTime entry queryBits, (entryMatchTM tapes).reachesIn t { state := (entryMatchTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryMatchTM tapes).halted c' ∧ c'.input = inp₀ ∧ (c'.work tapes.source).HasBinarySuffix rest ∧ (c'.work tapes.address).HasBinaryContent entry.1.bits ∧ 1 ≤ (c'.work tapes.address).head ∧ (c'.work tapes.address).cells 0 = Γ.start ∧ (c'.work tapes.value).HasBinaryPrefix entry.2.bits ∧ (c'.work tapes.value).cells 0 = Γ.start ∧ (c'.work tapes.addressCounter).HasBinaryPrefix (List.replicate (bitlen entry.1) true) ∧ (c'.work tapes.addressCounter).cells 0 = Γ.start ∧ (c'.work tapes.addressWidth).HasBinaryNat 0 ∧ (c'.work tapes.valueCounter).HasBinaryPrefix (List.replicate (bitlen entry.2) true) ∧ (c'.work tapes.valueCounter).cells 0 = Γ.start ∧ (c'.work tapes.valueWidth).HasBinaryNat 0 ∧ (c'.work tapes.query).HasBinaryContent queryBits ∧ 1 ≤ (c'.work tapes.query).head ∧ (c'.work tapes.query).cells 0 = Γ.start ∧ (c'.work tapes.result).HasBinaryPrefix [decide (entry.1.bits = queryBits)] ∧ (c'.work tapes.result).cells 0 = Γ.start ∧ (∀ (i : Fin n), TM.Parked (c'.work i)) ∧ (∀ (i : Fin n), i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.addressWidth → i ≠ tapes.valueCounter → i ≠ tapes.valueWidth → i ≠ tapes.query → i ≠ tapes.result → c'.work i = work₀ i) ∧ c'.output = out₀

theorem Complexity.RAM.RegisterStore.Machine.entryMatchReadTM_reachesIn_frame_internal {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ tapes.source).HasBinarySuffix (entry.encode ++ rest)) (haddress : (work₀ tapes.address).HasBinaryPrefix []) (hvalue : (work₀ tapes.value).HasBinaryPrefix []) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (haddressCounter : (work₀ tapes.addressCounter).HasBinaryNat 0) (haddressWidth : (work₀ tapes.addressWidth).HasBinaryNat 0) (hvalueCounter : (work₀ tapes.valueCounter).HasBinaryNat 0) (hvalueWidth : (work₀ tapes.valueWidth).HasBinaryNat 0) (hquery : (work₀ tapes.query).HasBinaryString queryBits) (hqueryStart : (work₀ tapes.query).cells 0 = Γ.start) (hresult : (work₀ tapes.result).HasBinaryPrefix []) (hresultStart : (work₀ tapes.result).cells 0 = Γ.start) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) (houtput : TM.Parked out₀) : ∃ (c' : Complexity.Cfg n (entryMatchReadTM tapes).Q), ∃ t ≤ entryMatchReadTime entry queryBits, (entryMatchReadTM tapes).reachesIn t { state := (entryMatchReadTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryMatchReadTM tapes).halted c' ∧ c'.input = inp₀ ∧ ReadableEntryMatch tapes entry rest queryBits work₀ c'.work ∧ c'.output = out₀

theorem Complexity.RAM.RegisterStore.Machine.entryMatchReadTime_eq_internal (entry : Entry) (queryBits : List Bool) : entryMatchReadTime entry queryBits = 4 * entry.1.bits.length + 3 * entry.2.bits.length + max entry.1.bits.length queryBits.length + 18

Closed form for the optimized unary-marker decode-and-match runtime.

theorem Complexity.RAM.RegisterStore.Machine.entryMatchReadTime_le_linear_internal (entry : Entry) (queryBits : List Bool) : entryMatchReadTime entry queryBits ≤ 5 * entry.1.bits.length + 3 * entry.2.bits.length + queryBits.length + 18

One optimized readable match is linear in the two encoded word widths and the preserved query width.