OAI/Computability/UniqueGames/Machines/FinalCNFLoopLemmas.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The complete actual output-producing trace of the final CNF machine. Its terminal configuration still contains private work tapes; FinalCNFCleanup supplies the subsequent canonical halt required by the machine interface.

  1. structure OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 17
  2. structure OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 28
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 40
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 60
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 66

    Source documentation

    Induction follows the actual unary row counter and the actual unconsumed input suffix. Every iteration invokes the checked row program.

    noncomputable def loopInTime (headerPlan plan : Plan) (table : GraphTables.Table)
    (remaining : Nat) :
    ∀ (r : Nat), r + remaining = table.darts → ∀ (base : Tape → List Bool)
      (ambient : Ambient), LoopInvariant table r base →
        LoopRun headerPlan plan table r remaining base ambient := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.LoopRun

  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 131
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 135
  8. structure OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 140
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 148
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 165

    Source documentation

    The input is read from the genuine initList configuration. Header, every row, final guard, and reversal are all actual transitions of this one program.

    noncomputable def rawRun (plan : Plan) (table : GraphTables.Table) : RawRun plan table := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.RawRun

  11. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape line 214
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape.enumList line 221
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape.enumList_getElem?_ctorIdx_eq line 225
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape.enumList_nodup line 229
  15. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.(instance at line 231) line 231
  16. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label line 235
  17. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Ambient line 253
  18. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State line 254
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionStates line 259

    Source documentation

    The residue and the emitter's unit field are just permuted; no tape is read or written by this static change of finite state coordinates.

    def divisionStates (ρ : Type) (d : Nat) :
    MachineFixedDivMod.State (Ambient ρ d × Unit) (degree d) ≃ State ρ d where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstFinish line 266
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondFinish line 270
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.affinePlan line 274
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstPlan line 279
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondPlan line 283
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.outputPlan line 287
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupTape line 291
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape line 298
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement line 310

    Source documentation

    Every branch is a concrete finite TM2 statement. The fixed table H is evaluated only on finite control values, never on an unbounded tape value.

    def statement {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ) :
    Label d → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d)
  | .initialize =>
    .push (ports .quotientFirst) (fun _ => false)
      (.push (ports .quotientSecond) (fun _ => false)
        (.push (ports .remainderFirst) (fun _ => false)
          (.push (ports .remainderSecond) (fun _ => false)
            (.load (fun s => (s.1, none))
              (.goto fun _ => labels (.firstEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry)))))))
  | .firstEmit l =>
    PCP.AlphabetTable.Emitter.statement (firstPlan ρ d) (fun _ => ports .inputVertex)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstPlan

  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program line 375