OAI/Computability/MaxCut/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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 20
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList line 24
  3. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_getElem?_ctorIdx_eq line 27
  4. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_nodup line 31
  5. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 33) line 33
  6. inductive OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 37
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList line 41
  8. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_getElem?_ctorIdx_eq line 43
  9. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_nodup line 47
  10. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 49) line 49
  11. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 53
  12. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderState line 54
  13. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.pushTrue line 57

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 62
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 74
  16. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram line 84

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.HeaderState

  17. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerMachine line 100
  18. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.initialTapes line 111
  19. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanTapes line 115
  20. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.finalTapes line 121
  21. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 127
  22. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 132
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.initializeStep line 136
  24. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 146
  25. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 157
  26. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanTrace line 175

    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.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration

  27. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerTrace line 192
  28. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerInTime line 205

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.initialTapes, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration

  29. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows line 216

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 219
  31. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 222
  32. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.rowBase line 229
  33. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 236

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 249
  35. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 265

    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.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes

  36. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 289

    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.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.rowBase, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows

  37. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 297

    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.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 301
  39. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 314
  40. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 329

    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.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes

  41. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 352