OAI/Computability/UniqueGames/Machines/PoweringMachineLoop.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-control preparation and enumeration for the powered-table machine. The degree and radius determine a fixed multiplier B = 2*d^t. Only the input vertex count varies at runtime, and it is stored on unary tapes. The header machine consumes a cloned first input field, preserving its unread suffix, and writes the three fields needed by the outer loop.

The row enumeration lemmas specify the canonical suffix invariant used with MachineCountedLoop. They do not stand in for the caller's per-row machine traces, which must be supplied by the actual walk and relation evaluator.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 20
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList line 24
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_getElem?_ctorIdx_eq line 26
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_nodup line 30
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.(instance at line 32) line 32
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 36
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList line 40
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_getElem?_ctorIdx_eq line 42
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_nodup line 46
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.(instance at line 48) line 48
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 52
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderState line 53
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.pushTrue line 56

    Source documentation

    A syntactic chain of a fixed number of true-bit pushes.

    def pushTrue {K Λ σ : Type} (destination : K) : Nat →
    TM2.Stmt (fun _ : K => Bool) Λ σ → TM2.Stmt (fun _ : K => Bool) Λ σ
  | 0, next => next
  | count + 1, next => pushTrue destination count (.push destination (fun _ => true) next)
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 61
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 73
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerProgram line 83

    Source documentation

    Each true bit from the first input field contributes one counter bit, one vertex-header bit, and B dart-header bits. No numeric register is used.

    def headerProgram {σ : Type} (B : Nat) :
    HeaderLabel → TM2.Stmt HeaderAlphabet HeaderLabel (HeaderState σ)
  | .initialize =>
      .push .counter (fun _ => false)
        (.push .vertices (fun _ => false)
          (.push .darts (fun _ => false)
            (.load (fun state => (state.1, none)) (.goto fun _ => .scan))))
  | .scan =>
      .pop .source (fun state head => (state.1, head))
        (.branch (fun state => state.2.getD false)
          (.push .counter (fun _ => true)
            (.push .vertices (fun _ => true)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.HeaderState

  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerMachine line 99
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.initialTapes line 110
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanTapes line 114
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.finalTapes line 120
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 126
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 131
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.initializeStep line 135
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 145
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 156
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanTrace line 174

    Source documentation

    The loop consumes precisely the unary field, including its delimiter.

    theorem scanTrace {σ : Type} (B remaining processed : Nat) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (headerProgram B)))^[remaining + 1]
      (some (scanConfiguration B remaining processed suffix ambient register)) =
      some (finalConfiguration B (processed + remaining) suffix ambient) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.scanConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.finalConfiguration

  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerTrace line 191
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerInTime line 204

    Source documentation

    A genuine finite TM2 execution certificate for the header phase.

    def headerInTime {σ : Type} (B n : Nat) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (headerProgram B))
      ⟨some .initialize, (ambient, register), initialTapes n suffix⟩
      (some (finalConfiguration B n suffix ambient)) (n + 2) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.finalConfiguration

  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.remainingRows line 215

    Source documentation

    Completed rows at guard remainder r are precisely vertices r,...,n-1. This is a semantic description of the output tape, not a machine instruction.

    def remainingRows (rowBlock : Nat → List Bool) (n r : Nat) : List Bool :=
…
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 218
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 221
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.rowBase line 228
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 235

    Source documentation

    A per-vertex body certificate must actually execute in the combined program, preserve the remaining unary vertex counter and caller frame, and prepend precisely that vertex's ordered block of rows.

    def VertexBodyTraces (counter output : K) (guardLabel bodyLabel : Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (base : K → List Bool) (suffix : List Bool) (ambient : σ)
    (rowBlock : Nat → List Bool) (cost : Nat → Nat) (n : Nat) : Prop :=
…
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 248
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 264

    Source documentation

    Derives the complete outer enumeration trace from the actual row-body traces. Descending cursor order and prepending produce canonical ascending vertex order on the output tape. The zero delimiter is retained for cleanup.

    def vertexLoopInTime (counter output : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atGuard : program guardLabel = MachineUnaryCounter.guard counter bodyLabel exitLabel)
    (base : K → List Bool) (suffix : List Bool) (ambient : σ)
    (rowBlock : Nat → List Bool) (cost : Nat → Nat) (n bodyBound : Nat)
    (bodies : VertexBodyTraces counter output guardLabel bodyLabel program
      base suffix ambient rowBlock cost n)
    (bounded : ∀ r, r < n → cost r ≤ bodyBound) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some guardLabel, (ambient, none),
        MachineUnaryCounter.counterTapes counter base n suffix⟩
      (some ⟨some exitLabel, (ambient, none),
…

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

  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 288

    Source documentation

    The output field is exactly the completed canonical row stream.

    theorem vertexLoop_output (counter output : K) (different : output ≠ counter)
    (base : K → List Bool) (suffix : List Bool) (rowBlock : Nat → List Bool) (n : Nat) :
    MachineUnaryCounter.counterTapes counter (rowBase output base rowBlock n 0) 0 suffix output =
      remainingRows rowBlock n 0 ++ base output := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.counterTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.rowBase, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.remainingRows

  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 296

    Source documentation

    Lookup scan suffixes and other work tapes may evolve between vertices. Only the output field is replaced by the prescribed canonical row suffix.

    def varyingRowBase (output : K) (base : Nat → K → List Bool)
    (rowBlock : Nat → List Bool) (n r : Nat) : K → List Bool :=
…
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 300
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 313
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 328

    Source documentation

    The outer loop with a varying work-tape frame. Actual row-body traces determine that frame; no cleanup of accumulated lookup suffixes is assumed.

    def vertexLoopInTime_varying (counter output : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atGuard : program guardLabel = MachineUnaryCounter.guard counter bodyLabel exitLabel)
    (base : Nat → K → List Bool) (suffix : List Bool) (ambient : Nat → σ)
    (rowBlock : Nat → List Bool) (cost : Nat → Nat) (n bodyBound : Nat)
    (bodies : VaryingVertexBodyTraces counter output guardLabel bodyLabel program
      base suffix ambient rowBlock cost n)
    (bounded : ∀ r, r < n → cost r ≤ bodyBound) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some guardLabel, (ambient n, none),
        MachineUnaryCounter.counterTapes counter (base n) n suffix⟩
      (some ⟨some exitLabel, (ambient 0, none),
…

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

  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 351