OAI/Computability/MaxCut/Machines/MachinePaddedExpanderFamilyBounds.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timeCoefficient line 10
2. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial line 13
3. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial_encoding line 16
4. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.ceilingCost_le line 21
5. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.combinedCost_le line 37
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.familyCost_le line 47
7. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord line 57
8. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient line 62
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord_length_le line 66

   Source documentation

   Complete unary rotation-table output, including every delimiter.

   theorem outputWord_length_le
       (H : Table (cloudSize PCP.Expanders.baseDegree) PCP.Expanders.baseDegree) (k : Nat) :
       (outputWord H k).length ≤ outputCoefficient * (k + 1)^2 := by
   …

   Mentions: OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient

10. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInTime line 108

    Source documentation

    Actual geometric search, placed onto the eventual family-level tape.

    noncomputable def ceilingInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some main, initialState state register, initialTapes requested⟩
          (some ⟨some familyEntry, (state, (false, none)), handoffTapes requested⟩)
          ((MachineCeilingPower.timePolynomial PCP.ExpanderFamily.growth).eval
            (encodeWord requested).length) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.timePolynomial, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth, OAI.MaxCutGames.Foundations.Complexity.encodeWord

11. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime line 132

    Source documentation

    Actual table materialization consumes the level produced by the preceding phase while retaining the original request and its computed padded size.

    noncomputable def materializeInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some familyEntry, (state, (false, none)), handoffTapes requested⟩
          (some ⟨none, finalState H state, finalTapes H requested⟩)
          (MachineExpanderFamilyBounds.inputCoefficient * (requested + 1)^5) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient

12. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.paddedInTime line 155

    Source documentation

    A single concrete finite program takes the original unary request all the way to the exact forward family table. Both phase executions are supplied by proved machines; there is no construction or runtime hypothesis.

    noncomputable def paddedInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some main, initialState state register, initialTapes requested⟩
          (some ⟨none, finalState H state, finalTapes H requested⟩)
          (MachinePaddedExpanderFamilyBounds.timePolynomial.eval (encodeWord requested).length) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

13. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.placedInTime line 173

    Source documentation

    Static placements of the complete computation into a larger caller preserve every complement tape and consume exactly the same runtime budget.

    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))
        (requested : Nat) (state : MachineExpanderFamily.State ρ fixedDegree)
        (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step target)
          (Placement.configuration view labels exit extra
            ⟨some main, initialState state register, initialTapes requested⟩)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes

14. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.CoreTape line 209
15. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.NativeTape line 210
16. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Tape line 211
17. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Alphabet line 212
18. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable line 213
19. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.FamilyState line 214
20. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.State line 215
21. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.inputNative line 217
22. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.outputNative line 218
23. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.powerNative line 219
24. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sizeNative line 220
25. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.levelNative line 221
26. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.powerTape line 223
27. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sizeTape line 224
28. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.levelTape line 225
29. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyTape line 228

    Source documentation

    Unused private shadows of the two public roles remain empty.

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

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

30. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyView line 231
31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyView_left line 235
32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyView_right line 242
33. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.stateEquiv line 263
34. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.seedState line 266
35. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.readyState line 269
36. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sourceProgram line 271
37. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Label line 275
38. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.program line 283

    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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.readyState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sourceProgram, OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drain, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.powerTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sizeTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.levelTape

39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.frame line 290
40. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.rotor line 294
41. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.resultCore line 297
42. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working line 300
43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working_power line 305
44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working_size line 308
45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working_level line 312
46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.update_working_power line 316
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.update_working_size line 323
48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.update_working_level line 333
49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working_empty line 343
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.initial_other_inline_MachineRegularFamily line 347
51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.final_other_inline_MachineRegularFamily line 354

    Source documentation

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

    private theorem final_other_inline_MachineRegularFamily (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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.NativeTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.inputNative, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.outputNative, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.powerNative, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.sizeNative, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.levelNative, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes

52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.initial_placement line 375
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.final_placement line 396
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.source_initial_state line 444
55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.source_final_state line 448
56. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyInTime line 454

    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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.frame, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.resultCore, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize

57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.appendTrace_inline_MachineRegularFamily line 475
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 480

    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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.working, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.frame

59. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 502
60. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.startInTime line 511
61. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.timePolynomial line 521
62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 525
63. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 538

    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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.frame, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.resultCore

64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.result_output line 554
65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 557
66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.result_private_empty line 561
67. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.placedInTime line 566

    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.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.CoreTape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularFamily.frame

68. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 597
69. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.State line 598
70. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 601

    Source documentation

    A boundary test which inspects the first unary bit without consuming it.

    def zeroTest (operand : K) (exit : Option Λ) :
        TM2.Stmt (Alphabet (K := K)) Λ (State σ) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.State

71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 607
72. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes line 623

    Source documentation

    Slots 0 and 1 are the operands; slots 2 and 3 are their saved prefixes.

    def tapes (slots : Fin 4 ↪ K) (base : K → List Bool)
        (left right savedLeft savedRight : List Bool) : K → List Bool :=
    …

73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 628
74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 633
75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 638
76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 643
77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 648
78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 666
79. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.stop line 670
80. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.scan line 674
81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 689
82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 702
83. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 715
84. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 730
85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 761
86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 768
87. inductive OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.Label line 775
88. instance OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.(instance at line 781) line 781
89. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.statement line 785
90. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.steps line 793
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 795
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 851

    Source documentation

    Actual comparison on a caller frame: both complete operand tapes and all other tapes are preserved, both scratch tapes remain empty, and the finite result flag is precisely the strict comparison of the two unary values.

    theorem lessThanTrace (slots : Fin 4 ↪ K) (labels : Label → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.State

93. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 869
94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 871
95. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 877
96. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.machine line 893
97. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 904