OAI/Computability/UniqueGames/Machines/MachineRegularOwnerCleanup.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 11
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.State line 12
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 13
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq line 16

    Source documentation

    Constructor-by-constructor equality for a fixed sum of tape alphabets.

    private def sumDecidableEq {A B : Type} (left : DecidableEq A) (right : DecidableEq B) :
    DecidableEq (A ⊕ B)
  | .inl a, .inl b => match left a b with
      | .isTrue h => .isTrue (congrArg (Sum.inl : A → A ⊕ B) h)
      | .isFalse h => .isFalse (fun e => h (Sum.inl.inj e))
  | .inr a, .inr b => match right a b with
      | .isTrue h => .isTrue (congrArg (Sum.inr : B → A ⊕ B) h)
      | .isFalse h => .isFalse (fun e => h (Sum.inr.inj e))
  | .inl _, .inr _ => .isFalse (by intro h; cases h)
  | .inr _, .inl _ => .isFalse (by intro h; cases h)

/-- Every equality decision is explicitly assembled from fixed finite leaves.
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 29

    Source documentation

    Every equality decision is explicitly assembled from fixed finite leaves. There is no classical decision or recursive typeclass search on the tape sum.

    instance tapeDecidableEq : DecidableEq Tape :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Tape

  6. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 43

    Source documentation

    List membership uses Boolean equality. These instances are the explicit Boolean view of the executable equality procedure above.

    instance tapeBEq : BEq Tape where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Tape

  7. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 46
  8. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 50
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.core line 57
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 58
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.count line 59
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 60
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 61
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 62
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.level line 63
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 64
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 65
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 68

    Source documentation

    Every name is distinct, so the exact drain cost uses the entry lengths.

    def cleanupTapes : List Tape := [localRank, count, rotor, padding, level, dummyFuel]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.localRank, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.count, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.rotor, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.level, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel

  19. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 70
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 76
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 80
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 84

    Source documentation

    Coefficient one, no seed: the destination already contains its offset.

    def instruction (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt Alphabet Λ State
  | .scan => MachineUnaryAffineAt.scan padding scratch prefixTape 1
      (labels .scan) (labels .restore)
  | .restore => Reduction.MachineTransfer.loopAt scratch padding id false
      (labels .restore) (cleanupEntry labels exit)
  | .drain l => MachineDrainMany.instruction cleanupTapes
      (fun l => labels (.drain l)) exit l

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.scratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes

  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 93
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 96
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 99
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 102
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 109
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 114
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 118
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 123
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 129
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 135
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 162

    Source documentation

    Complete physical addition followed by the six exact drain loops. No phase run or precomputed sum word is supplied as a hypothesis.

    theorem traceAt (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ State)
    (code : ∀ l, program (labels l) = instruction labels exit l)
    (base : Tape → List Bool) (d o : Nat)
    (paddingWord : base padding = encodeWord d)
    (prefixWord : base prefixTape = encodeWord o)
    (scratchEmpty : base scratch = [])
    (ambient : MachineRegularOriginalBody.State) (register : Option Bool) :
    (advance (TM2.step program))^[steps base d]
      (some ⟨some (labels entry), (ambient, register), base⟩) =
      some ⟨exit, (ambient, none), finalTapes base d o⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.scratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes

  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 182