OAI/Computability/MaxCut/Machines/MachineLookupCore.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Finite control for destructive unary-indexed table lookup. The guard decreases the index even when the table is exhausted. Selection tests for an empty table before writing the destination. All tests inspect just one finite head register.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet line 18
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discard line 20
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.select line 28

    Source documentation

    Check that a field exists before seeding its destination delimiter.

    def select (source destination : K) (copyLabel rejected : Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  4. inductive OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label line 35
  5. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label.enumList line 39
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label.enumList_getElem?_ctorIdx_eq line 42
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label.enumList_nodup line 46
  8. instance OAI.MaxCutGames.Foundations.Complexity.MachineLookup.(instance at line 48) line 48
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program line 53

    Source documentation

    Six fixed labels and a single optional-bit register, independent of input.

    def program (index source destination : K) :
    Label → TM2.Stmt (Alphabet (K := K)) Label (σ × Option Bool)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  10. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes line 63

    Source documentation

    Three caller tapes with every other tape retained verbatim.

    def tapes (index source destination : K) (base : K → List Bool)
    (counter input output : List Bool) : K → List Bool :=
…
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes_index line 68
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes_source line 74
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes_destination line 80
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes_other line 85
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.update_index line 91
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.update_source line 105
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.update_destination line 116
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.fieldTapes_eq line 122
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.machine line 131

    Source documentation

    A concrete finite machine using exactly three binary stacks. Its table and unary index may be supplied in a caller configuration; no list oracle is used.

    def machine : FinTM2 where
…
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.skipWord line 152

    Source documentation

    Saturating removal of one zero-delimited word.

    def skipWord : List Bool → List Bool
  | [] => []
  | true :: bs => skipWord bs
  | false :: bs => bs
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 157
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 166

    Source documentation

    Iterated word removal agrees with zero-based list dropping, even after running past the end of the table.

    theorem skipWord_iterate_encodeWords (i : Nat) (values : List Nat) :
    (skipWord^[i]) (encodeWords values) = encodeWords (values.drop i) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.skipWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  23. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.headWord line 179

    Source documentation

    Copy the next complete word, including its delimiter. Empty input and unterminated words fail explicitly.

    def headWord : List Bool → Option (List Bool)
  | [] => none
  | false :: _ => some [false]
  | true :: bs => (headWord bs).map (true :: ·)
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 184
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 192
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupBits line 198
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 201
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 207

    Source documentation

    The index is on a separate tape and must decode to exactly one word.

    def lookupEncoded (index table : List Bool) : Option (List Bool) :=
…
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 212
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 216
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 221
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 226
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 232

    Source documentation

    Literal split at the selected word.

    theorem encoded_selected_split (values : List Nat) (i value : Nat)
    (h : values[i]? = some value) :
    encodeWords values = encodeWords (values.take i) ++ encodeWord value ++
      encodeWords (values.drop (i + 1)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  34. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.scannedBits line 246

    Source documentation

    This counts the bits through the selected word, capped at the whole table when the index is invalid. It is not a machine step count.

    def scannedBits (values : List Nat) (i : Nat) : Nat :=
…
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 249
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 258
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 262
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 269
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.output_length_le line 276
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.index_length_le line 283
  41. def OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps line 297
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 303

    Source documentation

    A uniform bound, including indices beyond the end of the table.

    theorem steps_le_encoded_length_strong (values : List Nat) (i : Nat) :
    steps values i ≤ (encodeWords values).length + 2 * i + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 318

    Source documentation

    The requested recurrence bound with one further unit of slack.

    theorem steps_le_encoded_length (values : List Nat) (i : Nat) :
    steps values i ≤ (encodeWords values).length + 2 * i + 3 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 325

    Source documentation

    Successful lookup uses exactly the consumed table prefix, one guard per skipped word, and the two final control steps.

    theorem steps_eq_scannedBits_of_lt (values : List Nat) (i : Nat)
    (h : i < values.length) :
    steps values i = scannedBits values i + i + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.scannedBits

  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 340
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 348

    Source documentation

    A subtraction-free exact failure formula: the whole table has been consumed, and every remaining unary index bit costs two steps.

    theorem steps_add_length_of_invalid (values : List Nat) (i : Nat)
    (h : values.length ≤ i) :
    steps values i + values.length = (encodeWords values).length + 2 * i + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 364

    Source documentation

    Linear in the combined encoded tape lengths. This is a bound for steps, not yet a theorem about a concrete machine's execution.

    theorem steps_le_input_encoding_size (values : List Nat) (i : Nat) :
    steps values i ≤ (encodeWords values).length + 2 * (encodeWord i).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discard_update_twice_inline_MachineLookupDiscard line 385
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardStep_delimiter line 394
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardStep_true line 407
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discard_empty_step line 421

    Source documentation

    EOF returns to the guard in one transition, without changing any tape.

    theorem discard_empty_step (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardTrace_update line 438

    Source documentation

    A normalized tape form for the field-discard trace.

    theorem discardTrace_update (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardTrace line 463

    Source documentation

    Discard exactly the first encoded field, in one transition per payload bit plus one transition for its delimiter. No condition is imposed on other tapes.

    theorem discardTrace (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  54. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discardInTime line 483

    Source documentation

    The same exact trace packaged for composition with ambient machine phases.

    def discardInTime (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Alphabet

  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.guard_step_succ line 513
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.guard_step_zero line 526
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.select_step_nonempty line 539
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.select_step_empty line 555
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.copyTrace line 566
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.selectTrace line 581
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.skipCycleTrace line 596
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.emptyCycleTrace line 614
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.successPrefixTrace line 632

    Source documentation

    A successful positional lookup scans precisely its prior and selected field. The suffix is arbitrary and is retained byte for byte.

    theorem successPrefixTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (prior : List Nat) (value : Nat)
    (indexSuffix suffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[
        (encodeWords prior).length + prior.length + value + 3]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord prior.length ++ indexSuffix)
        (encodeWords prior ++ (encodeWord value ++ suffix)) output⟩) =
      some ⟨some .accepted, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) suffix (encodeWord value ++ output)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupTrace_some line 660

    Source documentation

    Successful array access, with explicit selected value and preserved framing.

    theorem lookupTrace_some (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i value : Nat)
    (selected : values[i]? = some value)
    (indexSuffix suffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values ++ suffix) output⟩) =
      some ⟨some .accepted, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)) ++ suffix)
        (encodeWord value ++ output)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.emptyTrace line 689
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupTrace_invalid line 712

    Source documentation

    Invalid indices reject on a complete encoded table, after consuming that table and all positive index bits. The output and other tapes are unchanged.

    theorem lookupTrace_invalid (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat) (invalid : values.length ≤ i)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨some .rejected, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) [] output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  67. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultLabel line 735

    Source documentation

    The two explicit control outcomes on a complete encoded table.

    def resultLabel (values : List Nat) (i : Nat) : Label :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label

  68. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultOutput line 741

    Source documentation

    Successful lookup prefixes a complete unary word; failure writes nothing.

    def resultOutput (values : List Nat) (i : Nat) (output : List Bool) : List Bool :=
…
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupTrace line 748

    Source documentation

    A total execution statement for every natural index and complete table. No bound or validity assumption on the index is needed.

    theorem lookupTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨some (resultLabel values i), (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultLabel, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultOutput

  70. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupInTime line 772

    Source documentation

    A proved linear transition budget in the lengths of the encoded table and index, including invalid indices. The witness is the actual trace above.

    def lookupInTime (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program index source destination))
      ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩
      (some ⟨some (resultLabel values i), (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩)
      ((encodeWords values).length + 2 * (encodeWord i).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultLabel, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultOutput

  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.lookupHaltTrace line 789

    Source documentation

    The final control label executes a genuine halt in one more transition.

    theorem lookupHaltTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i + 1]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨none, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachineLookupSpec.steps, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.resultOutput

  72. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.timePolynomial line 804

    Source documentation

    A single polynomial in the combined two input lengths.

    noncomputable def timePolynomial : Polynomial Nat := Polynomial.C 2 * Polynomial.X + 1
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLookup.timePolynomial_bounds line 806
  74. def OAI.MaxCutGames.Foundations.Complexity.MachineLookup.machineInTime line 817

    Source documentation

    The same exact computation as a certificate for the concrete finite three-stack machine. Both valid and invalid indices terminate with reset local state, retaining the zero index delimiter and all other stated tape contents.

    def machineInTime (base : Fin 3 → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some .guard, ((), register), tapes (K := Fin 3) 0 1 2 base
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.tapes