OAI/Computability/UniqueGames/Machines/MachineCanonicalOutputLemmas.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Canonical output for finite Boolean machines

A raw machine may halt with retained metadata and a changed finite state. This wrapper redirects its halt to a fixed list of actual tape drains, then executes one state-reset instruction. The output tape is preserved and the result is literally haltList. Its cost follows from the raw execution and the maximum number of pushes in a raw statement.

The cleanup list is fixed with the program, not selected from the input. It may contain repetitions and may be empty when output is the only tape.

  1. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program line 29

    Source documentation

    The homogeneous parts of a finite machine, without dependent alphabet casts.

    structure Program (K Λ σ : Type) where
…
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 40
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 44
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 50

    Source documentation

    Add one finite scratch register while preserving each raw transition.

    def extendedStmt (labels : Λ → Λ') (haltTarget : Option Λ') :
    TM2.Stmt (fun _ : K => Bool) Λ σ →
      TM2.Stmt (fun _ : K => Bool) Λ' (σ × Option Bool)
  | .push k f next => .push k (fun state => f state.1)
      (extendedStmt labels haltTarget next)
  | .peek k f next => .peek k (fun state symbol => (f state.1 symbol, state.2))
      (extendedStmt labels haltTarget next)
  | .pop k f next => .pop k (fun state symbol => (f state.1 symbol, state.2))
      (extendedStmt labels haltTarget next)
  | .load f next => .load (fun state => (f state.1, state.2))
      (extendedStmt labels haltTarget next)
  | .branch test yes no => .branch (fun state => test state.1)
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 68
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 92
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Label line 103
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 105
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 108
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 110
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 113
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 121

    Source documentation

    A fixed finite program over the same Boolean tapes as the raw machine.

    def completedMachine (P : Program K Λ σ) (chosen : List K) : FinTM2 where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program

  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 132
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 137
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 141
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 157
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 162
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 173
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 179

    Source documentation

    The cleanup path consists of actual drains and one physical state reset.

    def cleanupExecution (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output) (state : σ)
    (register : Option Bool) (base : K → List Bool) :
    StateTransition.EvalsToInTime (completedMachine P chosen).step
      ⟨cleanupEntry chosen, (state, register), base⟩
      (some (haltList (completedMachine P chosen) (base P.output)))
      (MachineDrainMany.steps chosen base + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 211

    Source documentation

    No assumption about cleanup execution or clean raw work tapes is required.

    def outputsInTime (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output)
    (input output : List Bool) (state : σ) (base : K → List Bool) (budget : Nat)
    (raw : StateTransition.EvalsToInTime (sourceMachine P).step
      (initList (sourceMachine P) input) (some ⟨none, state, base⟩) budget)
    (correctOutput : base P.output = output) :
    TM2OutputsInTime (completedMachine P chosen) input (some output)
      (budget + chosen.length *
        (input.length + budget * Runtime.programPushBound (sourceMachine P) + 1) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.sourceMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedTime line 236
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 241
  23. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 249

    Source documentation

    An actual raw terminal execution, with arbitrary remaining state and tapes.

    structure TerminalRun (P : Program K Λ σ) (input output : List Bool) (budget : Nat) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program

  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 257

    Source documentation

    A polynomial raw run becomes a full canonical-output computation certificate.

    noncomputable def computableInPolyTime {α β : Type}
    (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output)
    (encodeIn : α → List Bool) (encodeOut : β → List Bool) (f : α → β)
    (rawTime : Polynomial Nat)
    (run : ∀ a, TerminalRun P (encodeIn a) (encodeOut (f a))
      (rawTime.eval (encodeIn a).length)) :
    TM2ComputableInPolyTime encodeIn encodeOut f where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.TerminalRun

  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 276
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 288

    Source documentation

    An explicit finite enumeration supplies the fixed cleanup list.

    noncomputable def computableInPolyTimeOfEnumeration {α β : Type} {N : Nat}
    (P : Program K Λ σ) (enumeration : Fin N ≃ K)
    (encodeIn : α → List Bool) (encodeOut : β → List Bool) (f : α → β)
    (rawTime : Polynomial Nat)
    (run : ∀ a, TerminalRun P (encodeIn a) (encodeOut (f a))
      (rawTime.eval (encodeIn a).length)) :
    TM2ComputableInPolyTime encodeIn encodeOut f :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.TerminalRun

  27. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label line 306
  28. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label.enumList line 311
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label.enumList_getElem?_ctorIdx_eq line 314
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label.enumList_nodup line 318
  31. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.(instance at line 320) line 320
  32. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Alphabet line 326
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.routine line 330

    Source documentation

    fields 0, fields 1, and fields 2 are the tail, reverse index, and encoded relation tapes. Every instruction reads or writes a single tape head.

    def routine (fields : Fin 3 → K) (row output scratch : K)
    (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Alphabet

  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.fieldBits line 353

    Source documentation

    Exact row field concatenation at the level of stored bits.

    def fieldBits (fields : Fin 3 → K) (base : K → List Bool) : List Bool :=
…
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.fieldSize line 356
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.fieldBits_length line 360
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.prefixTapes line 364
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.prefixTrace line 368

    Source documentation

    The three actual preserving-copy phases, with exact tape handoffs.

    theorem prefixTrace (fields : Fin 3 → K) (row output scratch : K)
    (hfields : ∀ i, fields i ≠ row ∧ fields i ≠ scratch)
    (hrowScratch : row ≠ scratch) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Alphabet

  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.appendTrace line 420
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.rowBits_eq line 465

    Source documentation

    The full existing graph codec, including all 4096 unary predicate fields.

    theorem rowBits_eq {n m : Nat} (r : DartRow n m) :
    encodeWords (rowWords r) = encodeWord r.tail.val ++
      encodeWord r.reverseIndex.val ++ encodeWords (relationWords r.relation) := by
…

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

  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 471
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.timePolynomial line 479
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 482
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.rowAppendInTime line 491

    Source documentation

    A composable actual execution certificate for a correctly encoded row. The program is fixed; row data occur only in the input-tape equalities.

    def rowAppendInTime {n m : Nat} (r : DartRow n m)
    (fields : Fin 3 → K) (row output scratch : K)
    (hfields : ∀ i, fields i ≠ row ∧ fields i ≠ scratch)
    (hrowOutput : row ≠ output) (hrowScratch : row ≠ scratch)
    (houtputScratch : output ≠ scratch) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Alphabet

  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.machine line 518

    Source documentation

    A fixed nine-label six-stack finite machine implementing the routine. Its inputs may be supplied in a caller's distributed tape configuration.

    def machine : FinTM2 where
…
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.machineRowInTime line 531

    Source documentation

    Direct execution of the concrete finite machine on caller-supplied unary fields. This instantiates all program equations; no execution premise remains.

    def machineRowInTime {n m : Nat} (r : DartRow n m) (base : Fin 6 → List Bool)
    (hrow : base 3 = []) (hscratch : base 5 = [])
    (htail : base 0 = encodeWord r.tail.val)
    (hreverse : base 1 = encodeWord r.reverseIndex.val)
    (hrelation : base 2 = encodeWords (relationWords r.relation)) (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some .relationRead, ((), register), base⟩
      (some ⟨none, ((), none),
        Function.update base (4 : Fin 6) (base 4 ++ encodeWords (rowWords r))⟩)
      (timePolynomial.eval ((encodeWords (rowWords r)).length + (base 4).length)) := by
…

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

  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.outputFrame line 561
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueRelation line 582

    Source documentation

    The actual 64-by-64 always-accepting relation.

    def trueRelation : RelationTable := Vector.replicate 4096 true
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueBits line 584
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueBits_length line 586
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits line 592
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits_length line 594
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 598
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits line 604

    Source documentation

    Ordered serialized rows with successive physically stored reverse indices.

    def rowsBits (v e : Nat) : Nat → List Bool
  | 0 => []
  | count + 1 => rowBits v e ++ rowsBits v (e + 1) count

/-- One initialization label and ten labels per fixed port. -/

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits

  55. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Label line 609

    Source documentation

    One initialization label and ten labels per fixed port.

    abbrev Label (d : Nat) := Unit ⊕ (Fin d × (MachineTableRows.Label ⊕ Unit))

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.Label

  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start line 611
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowLabel line 612
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.bumpLabel line 614
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fields line 616
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.afterPort line 620

    Source documentation

    The only data-changing index operation is a tape push, below. This function chooses a finite continuation among the fixed port-control labels.

    def afterPort {d : Nat} (p : Fin d) : Option (Label d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Label

  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.entry line 623
  62. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Alphabet line 628
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.continueAt line 630
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 636
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program line 642

    Source documentation

    No input-dependent natural number occurs in the finite program.

    def program (d : Nat) : Label d → TM2.Stmt Alphabet (Label d) (σ × Option Bool)
  | .inl () => pushWord 2 trueBits.reverse
      (.load (fun state => (state.1, none)) (continueAt (entry d)))
  | .inr (p, .inl stage) => MachineTableRows.routine fields 3 4 5
      (rowLabel p) (some (bumpLabel p)) stage
  | .inr (p, .inr ()) => .push 1 (fun _ => true) (continueAt (afterPort p))

/-- The three unary row fields, two empty work tapes, and accumulated output. -/

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.continueAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.routine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fields, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.bumpLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.afterPort

  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes line 650

    Source documentation

    The three unary row fields, two empty work tapes, and accumulated output.

    def fieldTapes (v e : Nat) (output : List Bool) : Fin 6 → List Bool :=
…
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes line 654

    Source documentation

    Before initialization, the fixed-relation tape is empty.

    def initialTapes (v e : Nat) (output : List Bool) : Fin 6 → List Bool :=
…
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initializeStep line 658

    Source documentation

    The fixed literal relation is actually emitted by a finite push chain.

    theorem initializeStep (d v e : Nat) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.step (program d) ⟨some (start d), (ambient, register), initialTapes v e output⟩ =
      some ⟨entry d, (ambient, none), fieldTapes v e output⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes

  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowTrace line 671
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.bumpStep line 694

    Source documentation

    The reverse index advances by pushing a real unary bit. The delimiter, all input fields, output, and work tapes have their exact stated contents.

    theorem bumpStep {d : Nat} (p : Fin d) (v e : Nat) (output : List Bool) (ambient : σ) :
    TM2.step (program d) ⟨some (bumpLabel p), (ambient, none), fieldTapes v e output⟩ =
      some ⟨afterPort p, (ambient, none), fieldTapes v (e + 1) output⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.bumpLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.afterPort

  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 707

    Source documentation

    The concrete row body and its actual index increment are consecutive phases of one fixed program; no whole-body trace is supplied as a premise.

    theorem rowAndBumpTrace {d : Nat} (p : Fin d) (v e : Nat) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[
        4 * (v + e + 8194) + 2 * output.length + 10]
      (some ⟨some (rowLabel p .relationRead), (ambient, register), fieldTapes v e output⟩) =
      some ⟨afterPort p, (ambient, none), fieldTapes v (e + 1) (output ++ rowBits v e)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.afterPort, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits

  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps line 720

    Source documentation

    Exact sum of actual row-and-increment costs. This recurrence is matched to the program by suffixTrace, rather than postulated as a runtime.

    def steps (v e : Nat) (output : List Bool) : Nat → Nat
  | 0 => 0
  | count + 1 => (4 * (v + e + 8194) + 2 * output.length + 10) +
      steps v (e + 1) (output ++ rowBits v e) count

/-- Actual execution from any port boundary to the final halt. The finite
control index fixes the remaining number of rows; all unbounded values are
physically stored in `fieldTapes`. -/

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes

  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.suffixTrace line 728

    Source documentation

    Actual execution from any port boundary to the final halt. The finite control index fixes the remaining number of rows; all unbounded values are physically stored in fieldTapes.

    theorem suffixTrace {d : Nat} (count : Nat) (p : Fin d) (hp : p.val + count = d)
    (v e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[steps v e output count]
      (some ⟨some (rowLabel p .relationRead), (ambient, register), fieldTapes v e output⟩) =
      some ⟨none, (ambient, none), fieldTapes v (e + count) (output ++ rowsBits v e count)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits

  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.allTrace line 753

    Source documentation

    One fixed-relation initialization transition followed by all actual rows. At zero ports initialization itself halts; no row is spuriously produced.

    theorem allTrace (d v e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[steps v e output d + 1]
      (some ⟨some (start d), (ambient, register), initialTapes v e output⟩) =
      some ⟨none, (ambient, none), fieldTapes v (e + d) (output ++ rowsBits v e d)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits

  75. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.graphRows line 769

    Source documentation

    Actual finite graph rows in increasing reverse-index order.

    def graphRows {n m : Nat} (v : Fin n) (e : Nat) :
    (count : Nat) → e + count ≤ m → List (DartRow n m)
  | 0, _ => []
  | count + 1, h =>
      ⟨v, ⟨e, by omega⟩, trueRelation⟩ ::
        graphRows v (e + 1) count (by omega)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueRelation

  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.graphRows_length line 776
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 784

    Source documentation

    The machine's bit stream is exactly the existing codec on the actual ordered row list, including both index fields and every predicate entry.

    theorem rowsBits_eq_graphRows {n m : Nat} (v : Fin n) (e count : Nat)
    (h : e + count ≤ m) :
    rowsBits v.val e count = encodeWords ((graphRows v e count h).flatMap rowWords) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.graphRows

  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.dummyRows line 796

    Source documentation

    For one vertex of an n-vertex degree-d graph, every dummy dart is its own reverse. The caller's initial index is the actual unary value d * v.

    def dummyRows {n : Nat} (d : Nat) (v : Fin n) : List (DartRow n (n * d)) :=
…
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.dummyRows_length line 801
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 804
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps_le_bound line 818

    Source documentation

    Every actual row cost is bounded by the largest row and accumulated output encountered during this finite loop.

    theorem steps_le_bound (v e : Nat) (output : List Bool) (count : Nat) :
    steps v e output count ≤ count *
      (4 * (v + e + count + 8194) +
        2 * (output.length + count * (v + e + count + 8194)) + 10) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps

  82. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.inputSize line 852

    Source documentation

    The variable-size input is exactly the two physical unary fields and existing output. The relation field is a fixed program constant.

    def inputSize (v e : Nat) (output : List Bool) : Nat :=
…
  83. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.timePolynomial line 856

    Source documentation

    A linear polynomial for each fixed port count d.

    noncomputable def timePolynomial (d : Nat) : Polynomial Nat :=
…
  84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 862
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machine line 885

    Source documentation

    A fixed finite machine. Its control stores only the fixed port position; vertex and reverse-index values reside on the tapes.

    def machine (d : Nat) : FinTM2 where
…
  86. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machineInTime line 898

    Source documentation

    The full actual finite-machine execution, including initialization and all rows. No body trace or runtime hypothesis is an input to this certificate.

    def machineInTime (d v e : Nat) (output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine d).step
      ⟨some (start d), ((), register), initialTapes v e output⟩
      (some ⟨none, ((), none), fieldTapes v (e + d) (output ++ rowsBits v e d)⟩)
      ((timePolynomial d).eval (inputSize v e output)) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.timePolynomial, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.inputSize

  87. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 911

    Source documentation

    The same actual machine on the padding invariant e = d * v, with its exact existing-codec graph-row output.

    def machineDummyInTime {n : Nat} (d : Nat) (v : Fin n)
    (output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine d).step
      ⟨some (start d), ((), register), initialTapes v.val (d * v.val) output⟩
      (some ⟨none, ((), none), fieldTapes v.val (d * v.val + d)
        (output ++ encodeWords ((dummyRows d v).flatMap rowWords))⟩)
      ((timePolynomial d).eval (inputSize v.val (d * v.val) output)) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.dummyRows, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.timePolynomial, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.inputSize

  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.finalFrame line 926

    Source documentation

    Input tail and both work tapes retain their required contents. The relation tape keeps the one initialized fixed field for subsequent use.

    theorem finalFrame (v e : Nat) (output : List Bool) :
    fieldTapes v e output 0 = encodeWord v ∧
    fieldTapes v e output 2 = trueBits ∧
    fieldTapes v e output 3 = [] ∧ fieldTapes v e output 5 = [] :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueBits