OAI/Computability/UniqueGames/Machines/MachineExpanderFamilyLoop.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual counted repetition of complete table-expansion cycles. The input counter is physically decremented, and the invariant carries the exact table at the completed family level.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 16
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 21
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 34
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 39
  5. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 44
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familySingleStep line 54
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 62

    Source documentation

    Every body is the already constructed actual resize run. There is no whole-loop, body-trace, or computational-correctness premise.

    noncomputable def levelLoopInTime {d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (completed remaining : Nat) (state : State ρ d) (suffix : List Bool) :
    LevelLoopRun positive H growth completed remaining state suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun