OAI/Computability/UniqueGames/Machines/MachineRegularOwnerBodyBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Bounds for actual dummy-owner execution

The size parameter includes the old output length. During the owner loop, newly emitted dummy blocks are bounded by the actual complete regularized table codec. No hypothesis about a machine body's execution supplies a bound.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 21
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 24
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 26
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 29
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 32
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 41
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 57
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 68
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 80

    Source documentation

    Any finite prefix inside this owner is a part of the actual output table, including when the supplied prefix length is larger than the number of blocks.

    theorem ownerPrefix_length_le (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (n : Nat) :
    (blocksPrefix (PreprocessingRegularWords.dummyVertexBits t (padding t)
      (familyCloudTable H t) v) n).length ≤ regularPolynomial.eval (inputLength t) := by
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 88
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 101

    Source documentation

    One actual dummy block has a uniform polynomial cost at every prefix of the owner loop. The only inputs are the real table, indices, and old output.

    theorem dummySteps_le (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (j : Fin (padding t v)) (n : Nat) (output : List Bool) :
    MachineRegularVertexBlock.dummySteps t (padding t) (familyCloudTable H t) v j
      (output ++ blocksPrefix (PreprocessingRegularWords.dummyVertexBits t (padding t)
        (familyCloudTable H t) v) n).length ≤
      (blockPolynomial internalDegree).eval (bodySize t output) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummySteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize

  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 132
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 135
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 138
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 141
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 145
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 164
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 181
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 194

    Source documentation

    Exact cost of the six physical drain loops and the prefix addition, expressed through the actual entry stack lengths.

    theorem cleanupSteps_working (data : MachineRegularOwnerBody.Data)
    (fuel saved : List Bool) (d : Nat) :
    MachineRegularOwnerCleanup.steps (MachineRegularOwnerBody.working data fuel saved) d =
      2*(d+1) + data.localRank.length + data.count.length + data.rotor.length +
        data.padding.length + data.level.length + fuel.length + 6 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working

  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 204
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 243

    Source documentation

    The whole owner budget follows from the real recurrence and its separately proved stage bounds. The zero-padding branch performs no family or vertex work.

    theorem ownerTime_le (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (output : List Bool) :
    MachineRegularOwnerBody.ownerTime H t v output ≤ timePolynomial.eval (bodySize t output) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize

  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 260
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 265