OAI/Computability/UniqueGames/Machines/MachineRegularFamily.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.CoreTape line 20
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.NativeTape line 21
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Tape line 22
4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Alphabet line 23
5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable line 24
6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.FamilyState line 25
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.State line 26
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.inputNative line 28
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.outputNative line 29
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.powerNative line 30
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sizeNative line 31
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.levelNative line 32
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.powerTape line 34
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sizeTape line 35
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.levelTape line 36
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyTape line 39

    Source documentation

    Unused private shadows of the two public roles remain empty.

    def familyTape (t : NativeTape) : Tape :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.NativeTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Tape

17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyView line 42
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyView_left line 46
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyView_right line 53
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.stateEquiv line 74
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.seedState line 77
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.readyState line 80
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sourceProgram line 82
24. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Label line 86
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.program line 94

    Source documentation

    Every size-dependent operation is performed by the checked native program. The entry load only resets the finite control state.

    def program (H : SmallTable) : Label → TM2.Stmt Alphabet Label State
      | .start => .load (fun _ => readyState H) (.goto fun _ => .family MachinePaddedExpanderFamily.main)
      | .family l => Placement.statement familyTape Label.family (some .drainPower) (sourceProgram H l)
      | .drainPower => MachineDrain.drain powerTape .drainPower (some .drainSize)
      | .drainSize => MachineDrain.drain sizeTape .drainSize (some .drainLevel)
      | .drainLevel => MachineDrain.drain levelTape .drainLevel none

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sourceProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drain, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.powerTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sizeTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.levelTape

26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.frame line 101
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.rotor line 105
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.resultCore line 108
29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working line 111
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working_power line 116
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working_size line 119
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working_level line 123
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.update_working_power line 127
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.update_working_size line 134
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.update_working_level line 144
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working_empty line 154
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.initial_other line 158
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.final_other line 165

    Source documentation

    The only retained native work words are the two sizes and the exhausted level.

    private theorem final_other (H : SmallTable) (k : Nat) (t : NativeTape)
        (hi : t ≠ inputNative) (ho : t ≠ outputNative) (hp : t ≠ powerNative)
        (hs : t ≠ sizeNative) (hl : t ≠ levelNative) :
        MachinePaddedExpanderFamily.finalTapes H k t = [] := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.NativeTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.inputNative, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.outputNative, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.powerNative, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.sizeNative, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.levelNative, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes

39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.initial_placement line 186
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.final_placement line 207
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.source_initial_state line 255
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.source_final_state line 259
43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyInTime line 265

    Source documentation

    The actual native family run, including geometric-level computation.

    noncomputable def familyInTime (H : SmallTable) (k : Nat) (core : CoreTape → List Bool)
        (hinput : core 4 = encodeWord k) (houtput : core 7 = []) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some (.family MachinePaddedExpanderFamily.main), readyState H, frame core⟩
          (some ⟨some .drainPower, readyState H,
            working (resultCore H k core)
              (encodeWord (PCP.PreprocessingLevels.paddedSize k))
              (encodeWord (PCP.PreprocessingLevels.paddedSize k)) (encodeWord 0)⟩)
          (MachinePaddedExpanderFamilyBounds.timePolynomial.eval (encodeWord k).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.resultCore, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize

44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.appendTrace line 286
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 291

    Source documentation

    Every retained private symbol is physically popped.

    theorem cleanupTrace (H : SmallTable) (m : Nat) (core : CoreTape → List Bool) :
        (advance (TM2.step (program H)))^[2*m+6]
          (some ⟨some .drainPower, readyState H,
            working core (encodeWord m) (encodeWord m) (encodeWord 0)⟩) =
          some ⟨none, readyState H, frame core⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.working, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.frame

46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 313
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.startInTime line 322
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.timePolynomial line 332
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 336
50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 349

    Source documentation

    Complete clean-frame execution, from the caller's actual unary request. No callback, table-construction premise, or caller-supplied runtime is assumed.

    noncomputable def familyCleanInTime (H : SmallTable) (k : Nat)
        (core : CoreTape → List Bool) (hinput : core 4 = encodeWord k)
        (houtput : core 7 = []) (state : State) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some .start, state, frame core⟩
          (some ⟨none, readyState H, frame (resultCore H k core)⟩)
          (timePolynomial.eval (encodeWord k).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.resultCore

51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.result_output line 365
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 368
53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.result_private_empty line 372
54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.placedInTime line 377

    Source documentation

    Direct embedding of the entire helper into another finite program.

    noncomputable def placedInTime {K Λ : Type} [DecidableEq K]
        (tape : Tape → K) (view : K → Option Tape)
        (left : ∀ t, view (tape t) = some t)
        (right : ∀ j t, view j = some t → tape t = j)
        (labels : Label → Λ) (exit : Option Λ) (extra : K → List Bool)
        (H : SmallTable) (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ State)
        (code : ∀ l, target (labels l) = Placement.statement tape labels exit (program H l))
        (k : Nat) (core : CoreTape → List Bool) (hinput : core 4 = encodeWord k)
        (houtput : core 7 = []) (state : State) :
        StateTransition.EvalsToInTime (TM2.step target)
          (Placement.configuration view labels exit extra ⟨some .start, state, frame core⟩)
          (some (Placement.configuration view labels exit extra
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularFamily.frame