OAI/Computability/UniqueGames/Machines/MachineLemmas.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Verifier-defined NP over finite bitstring machines. This definition does not mention SAT. Inputs and witnesses use a fixed explicit framing, verifiers return one Boolean symbol, and all stacks have finite alphabets. The Cook–Levin target separately requires an actual polynomial-time machine producing the established formulaBits serialization, in addition to satisfiability equivalence.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.naturalWordsEncoding line 13
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.formulaEncoding line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.gameEncoding line 24

    Source documentation

    Concrete forward-table output syntax with a checked parser.

    def gameEncoding (alphabet : Nat) : Computability.Encoding (Target.Instance alphabet) Bool where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Instance

  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.prefixBitMachine line 31

    Source documentation

    A fixed-bit prefixer uses one finite stack, one label, and one internal state. The bit is fixed in the program; it is not a second, freely accessible input.

    def prefixBitMachine (bit : Bool) : Turing.FinTM2 where
…
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.prefixBitPolyTime line 45

    Source documentation

    A real machine certificate: one transition performs the push and halts. TM2 counts execution of one finite statement as one transition. Here that statement contains exactly one stack push.

    noncomputable def prefixBitPolyTime (bit : Bool) :
    Turing.TM2ComputableInPolyTime (id : List Bool → List Bool) id (bit :: ·) where
…
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.enlargePolynomialBound line 65

    Source documentation

    Increasing a polynomial bound preserves the actual execution witness.

    def enlargePolynomialBound {α β αΓ βΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
    (certificate : Turing.TM2ComputableInPolyTime ea eb f)
    (bound : Polynomial Nat)
    (larger : ∀ n, certificate.time.eval n ≤ bound.eval n) :
    Turing.TM2ComputableInPolyTime ea eb f where
…
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.composeMachinePhases line 81

    Source documentation

    Two verified phases of one transition system compose with added polynomial budgets, both measured in the original input length. This theorem preserves the actual sequence of transition steps, not merely the sizes of configurations.

    def composeMachinePhases {σ : Type} (step : σ → Option σ)
    (start intermediate : σ) (finish : Option σ)
    (p q : Polynomial Nat) (inputLength : Nat)
    (first : StateTransition.EvalsToInTime step start (some intermediate) (p.eval inputLength))
    (second : StateTransition.EvalsToInTime step intermediate finish (q.eval inputLength)) :
    StateTransition.EvalsToInTime step start finish ((p + q).eval inputLength) := by
…
  8. structure OAI.UniqueGamesTheorem.Foundations.Complexity.PolynomialGapReduction line 93
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.pairBits line 116

    Source documentation

    A unary length frame followed by input bits and witness bits.

    def pairBits (input : List Bool × List Bool) : List Bool :=
…
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodePairAux line 119
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodePair line 125
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodePairAux_frame line 128
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodePair_pairBits line 138
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.pairBits_injective line 144
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.pairBits_length line 149
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.pairEncoding line 154
  17. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier line 163

    Source documentation

    A standard polynomial-time Boolean verifier. FinTM2 already requires finitely many stacks, control labels, and internal states; this field also requires every stack alphabet to be finite. The actual machine runs on the explicit paired input and halts with exactly one Boolean output symbol.

    structure NPVerifier where
…
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.Accepts line 169
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InNP line 176

    Source documentation

    NP is specified by polynomial witnesses and genuine finite-machine verification, independently of any reduction or satisfiability problem.

    def InNP (language : List Bool → Prop) : Prop :=
…
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.acceptedLanguage_inNP line 179
  21. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialThreeSATReduction line 185

    Source documentation

    The demanded Cook–Levin endpoint: both the SAT equivalence and an actual machine producing the fixed existing unary-token 3CNF encoding. This structure contains obligations; its inhabitance is not assumed or asserted here.

    structure PolynomialThreeSATReduction (language : List Bool → Prop) where
…
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.horizon line 191

    Source documentation

    A common clock for all witnesses of permitted length for one input.

    noncomputable def NPVerifier.horizon (verifier : NPVerifier) (inputLength : Nat) : Nat :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier

  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.input_time_le_horizon line 195
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier.runWithinHorizon line 206

    Source documentation

    A real verifier execution, enlarged to the single input-dependent clock. The machine and its output are the ones supplied in the verifier definition.

    def NPVerifier.runWithinHorizon (verifier : NPVerifier)
    (input witness : List Bool)
    (bounded : witness.length ≤ verifier.witnessBound.eval input.length) :
    Turing.TM2OutputsInTime verifier.computation.tm
      ((pairBits (input, witness)).map verifier.computation.inputAlphabet.invFun)
      (some ([verifier.verify (input, witness)].map verifier.computation.outputAlphabet.invFun))
      (verifier.horizon input.length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.NPVerifier, OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.pairBits

  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.skipWord line 232

    Source documentation

    Saturating removal of one zero-delimited word.

    def skipWord : List Bool → List Bool
  | [] => []
  | true :: bs => skipWord bs
  | false :: bs => bs
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 237
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 246

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.skipWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.headWord line 259

    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 :: ·)
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 264
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 272
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupBits line 278
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 281
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 287

    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) :=
…
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 292
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 296
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 301
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 306
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 312

    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.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.scannedBits line 326

    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 :=
…
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 329
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 338
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 342
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 349
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.output_length_le line 356
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.index_length_le line 363
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps line 377
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 383

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 398

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 405

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.scannedBits

  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 420
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 428

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 444

    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.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  53. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.Alphabet line 469
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guard line 473

    Source documentation

    A single finite statement: inspect the counter, decrement a positive counter, and jump to the body or exit. The zero delimiter is never consumed.

    def guard (counter : K) (bodyLabel exitLabel : Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.Alphabet

  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes line 482

    Source documentation

    An arbitrary caller frame with one tape holding the unary counter and its unread suffix. Only this tape depends on the counter value.

    def counterTapes (counter : K) (base : K → List Bool) (n : Nat)
    (suffix : List Bool) : K → List Bool :=
…
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes_counter line 486
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes_other line 491
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardPushBound line 497
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.stepAux_succ line 503

    Source documentation

    Positive counters lose exactly one true bit; the delimiter and suffix remain. Ambient state, unrelated tapes, and labels are accounted for explicitly.

    theorem stepAux_succ (counter : K) (bodyLabel exitLabel : Λ)
    (base : K → List Bool) (n : Nat) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.stepAux (guard counter bodyLabel exitLabel) (ambient, register)
      (counterTapes counter base (n + 1) suffix) =
      ⟨some bodyLabel, (ambient, none), counterTapes counter base n suffix⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes

  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.stepAux_zero line 512

    Source documentation

    A zero counter is inspected without removing its delimiter.

    theorem stepAux_zero (counter : K) (bodyLabel exitLabel : Λ)
    (base : K → List Bool) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.stepAux (guard counter bodyLabel exitLabel) (ambient, register)
      (counterTapes counter base 0 suffix) =
      ⟨some exitLabel, (ambient, none), counterTapes counter base 0 suffix⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes

  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardStep_succ line 520
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardStep_zero line 532
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardTrace_succ line 545

    Source documentation

    The positive branch executes in exactly one transition of the ambient program.

    theorem guardTrace_succ (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.Alphabet

  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardTrace_zero line 558
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardInTime_succ line 570
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guardInTime_zero line 585
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 624
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 630
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 635
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.BodyTraces line 642

    Source documentation

    The hypotheses are actual traces of the caller's body in the same program. Both endpoints have the same unary remainder and unread suffix.

    def BodyTraces (counter : K) (guardLabel bodyLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.totalSteps line 652

    Source documentation

    Exactly n supplied body blocks and n + 1 concrete guard transitions.

    def totalSteps (cost : Nat → Nat) (n : Nat) : Nat :=
…
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 655
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 658
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.loopTrace line 665

    Source documentation

    The loop trace is derived by composing each actual unary guard transition with one supplied body trace. No whole-loop execution is assumed.

    theorem loopTrace (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 698
  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.loopInTime line 710

    Source documentation

    An actual timed execution witness with the exact composed step count.

    def loopInTime (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.baseFrame line 731

    Source documentation

    Chaining the caller's declared per-body frame equalities.

    theorem baseFrame (base : Nat → K → List Bool) (frame : K → Prop) (n : Nat)
    (bodyFrame : ∀ r, r < n → ∀ k, frame k → base (r + 1) k = base r k) :
    ∀ k, frame k → base n k = base 0 k := by
…
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.counterFrame line 744

    Source documentation

    Protected tapes are unchanged by the complete loop, including its guard steps. The counter itself is explicitly excluded from this frame.

    theorem counterFrame (counter : K) (suffix : List Bool)
    (base : Nat → K → List Bool) (frame : K → Prop) (n : Nat)
    (counterOutside : ∀ k, frame k → k ≠ counter)
    (bodyFrame : ∀ r, r < n → ∀ k, frame k → base (r + 1) k = base r k) :
    ∀ k, frame k →
      counterTapes counter (base n) n suffix k = counterTapes counter (base 0) 0 suffix k := by
…
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 756

    Source documentation

    Actual loop execution and preservation of an arbitrary declared tape frame.

    theorem loopTrace_framed (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…