OAI/Computability/MaxCut/Machines/MachineFieldProfile.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Preserved comparisons of actual field stacks and their finite equality profile. All whole-word equalities below are specifications of finite-head comparison.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile line 16
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile line 18
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile_encodeWord line 21
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.statement_roundtrip line 36
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.copyStateEquiv line 41
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.normalState line 48
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.copyStatement line 50
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.copyInCompareState line 55
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.nonDestructiveCompareInTime line 102
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.setEntry line 159
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 162
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.setExpected line 168
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.foldProfile line 172
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 175
  15. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape line 191
  16. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Label line 192
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.labelAt line 194
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.storePair line 197
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileProgram line 204

    Source documentation

    The fixed list of pairs determines all control labels and original fields. The program compares only copied work-stack heads, then stores one finite bit.

    def profileProgram {q : Nat} (cells : List (Fin q × Fin q)) (label : Label cells) :
    TM2.Stmt (fun _ : Tape q => Bool) (Label cells) (MachineCompare.State (Profile q)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Label, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile

  20. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.pairTime line 224
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixProfile line 228
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixTime line 232
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 236
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 244
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.stageInTime line 252

    Source documentation

    One fully constructed copy/copy/compare/store stage, restoring every stack.

    def stageInTime {q : Nat} (cells : List (Fin q × Fin q)) (r : Nat) (hr : r < cells.length)
    (base : Tape q → List Bool) (hwork : ∀ w : Fin 3, base (.inr w) = []) (profile : Profile q) :
    StateTransition.EvalsToInTime (TM2.step (profileProgram cells))
      ⟨some (labelAt cells r 0), normalState profile, base⟩
      (some ⟨some (labelAt cells (r + 1) 0),
        normalState (setExpected (fun i => base (.inl i)) profile cells[r]), base⟩)
      (pairTime (fun i => base (.inl i)) cells[r]) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileProgram, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.normalState, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.setExpected, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.pairTime

  26. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixInTime line 298

    Source documentation

    Compose the actual stages up to any fixed position in the pair list.

    def prefixInTime {q : Nat} (cells : List (Fin q × Fin q))
    (base : Tape q → List Bool) (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q)
    (r : Nat) (hr : r ≤ cells.length) :
    StateTransition.EvalsToInTime (TM2.step (profileProgram cells))
      ⟨some (labelAt cells 0 0), normalState initial, base⟩
      (some ⟨some (labelAt cells r 0),
        normalState (prefixProfile (fun i => base (.inl i)) initial cells r), base⟩)
      (prefixTime (fun i => base (.inl i)) cells r) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileProgram, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.normalState, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixProfile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.prefixTime

  27. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.allPairs line 318
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 321
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.length_allPairs line 324
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 327
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileMachine line 333

    Source documentation

    A concrete finite machine for the full field equality matrix.

    def profileMachine (q : Nat) : FinTM2 where
…
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileInTime line 345

    Source documentation

    Compute every matrix entry while preserving all original field stacks.

    def profileInTime (q : Nat) (base : Tape q → List Bool)
    (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q) :
    StateTransition.EvalsToInTime (profileMachine q).step
      ⟨some (labelAt (allPairs q) 0 0), normalState initial, base⟩
      (some ⟨none, normalState (equalityProfile (fun i => base (.inl i))), base⟩)
      (((allPairs q).map (pairTime (fun i => base (.inl i)))).sum + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileMachine, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.allPairs, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.normalState, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.pairTime

  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.pairTime_le line 371
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.totalTime_le line 380
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 392

    Source documentation

    A linear bound in the maximum original field length, for fixed q. The actual machine and execution witness are retained.

    def profileInTime_bounded (q : Nat) (base : Tape q → List Bool)
    (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q)
    (L : Nat) (hL : ∀ i, (base (.inl i)).length ≤ L) :
    StateTransition.EvalsToInTime (profileMachine q).step
      ⟨some (labelAt (allPairs q) 0 0), normalState initial, base⟩
      (some ⟨none, normalState (equalityProfile (fun i => base (.inl i))), base⟩)
      (q * q * (5 * L + 6) + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.Profile, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.profileMachine, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.allPairs, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.normalState, OAI.MaxCutGames.Foundations.Complexity.MachineFieldProfile.equalityProfile