OAI/Computability/UniqueGames/Reduction/AddressMachineInitial.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders line 16
2. def OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized line 21
3. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.input_header line 25
4. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.input_headerClean line 32
5. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_frame line 53
6. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_empty line 63
7. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_source line 74
8. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_variables line 79
9. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_occurrences line 91
10. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_base line 103
11. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_capacity line 108
12. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_reversed line 113
13. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_work line 127
14. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_current line 130
15. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_remaining line 134
16. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders_copyScratch line 138
17. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_frame line 142
18. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_header line 148
19. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_source line 156
20. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_variables line 163
21. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_occurrences line 166
22. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_base line 169
23. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_capacity line 173
24. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_reversed line 177
25. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_current line 183
26. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_remaining line 188
27. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_savedIndex line 194
28. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_empty line 198
29. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_work line 204
30. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_index line 208
31. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_scratch line 215
32. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_copyScratch line 222
33. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_field line 227
34. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_finalOutput line 235
35. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_privateAddress line 244
36. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_edgeClean line 254
37. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized_eq_setDigits_zero line 270

    Source documentation

    An exact equality with the checked schedule's initial digit configuration.

    theorem initialized_eq_setDigits_zero (F : SourceEncoding.Input) :
        initialized k T F = AddressOdometerSchedule.setDigits F.equations.length
          (fun _ : Fin k => 0) (afterHeaders k T F) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.afterHeaders

38. def OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.inTime line 296

    Source documentation

    Actual two-phase initialization from the concrete machine input.

    def inTime (F : SourceEncoding.Input) :
        StateTransition.EvalsToInTime (AddressMachineProgram.machine k T).step
          (initList (AddressMachineProgram.machine k T) (SourceEncoding.inputBits F))
          (some ⟨some (AddressMachineProgram.bodyStart k T), AddressMachineSpace.initialState k,
            initialized k T F⟩)
          ((MachineAddressHeaders.timePolynomial k s d T.vectors.length).eval
            (SourceEncoding.inputBits F).length + k * (2 * (SourceEncoding.inputBits F).length + 6) + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.timePolynomial

39. def OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.timePolynomial line 330
40. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.timePolynomial_eval line 334
41. def OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.inPolynomialTime line 341