OAI/Computability/UniqueGames/Machines/MachineCloudCount.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Tape line 12
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Tape.enumList line 16
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Tape.enumList_getElem?_ctorIdx_eq line 19
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Tape.enumList_nodup line 23
5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.(instance at line 25) line 25
6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Alphabet line 29
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.State line 30
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory line 32
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_original line 40
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_work line 42
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_target line 44
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_scratch line 46
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_count line 48
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory_spare line 50
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.update_memory_work line 53
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.update_memory_target line 57
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 61
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.update_memory_count line 65
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.finishField line 72
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldLoop line 75
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.hit line 90

    Source documentation

    Specification only: equality of the original natural values, unless an earlier step has already detected overflow.

    def hit (flag : Bool) (x v : Nat) : Nat := if flag = false ∧ x = v then 1 else 0

22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 92
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 109
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 125
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldTrace line 143

    Source documentation

    The actual field-reading trace. The scratch holds exactly the consumed target bits, and the output increment records equality of the complete field.

    theorem fieldTrace (again restore : Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (atField : program again = fieldLoop again restore)
        (original suffix targetSuffix spare : List Bool) (x v : Nat)
        (scratch count : List Bool) (ambient : σ) (flag : Bool) (register : Option Bool) :
        (advance (TM2.step program))^[x + 1]
          (some ⟨some again, ((ambient, flag), register),
            memory original (encodeWord x ++ suffix) (encodeWord v ++ targetSuffix)
              scratch count spare⟩) =
          some ⟨some restore, ((ambient, false), none),
            memory original suffix (encodeWord (v - x) ++ targetSuffix)
              (List.replicate (min x v) true ++ scratch)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 177
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 182

    Source documentation

    The actual restoring transfer returns every consumed target bit.

    theorem preservingFieldTrace (again restore next : Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (atField : program again = fieldLoop again restore)
        (atRestore : program restore = Reduction.MachineTransfer.loopAt
          .scratch .target id false restore (some next))
        (original suffix targetSuffix count spare : List Bool) (x v : Nat)
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[x + min x v + 2]
          (some ⟨some again, ((ambient, false), register),
            memory original (encodeWord x ++ suffix) (encodeWord v ++ targetSuffix)
              [] count spare⟩) =
          some ⟨some next, ((ambient, false), none),
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 214
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 236

    Source documentation

    Consecutive concrete field-discard instructions consume a fixed list of fields. The hypotheses specify code, not an abstract body execution.

    theorem discardFieldsTrace (labels : Nat → Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (fields : List Nat) (offset : Nat)
        (atField : ∀ i, i < fields.length → program (labels (offset + i)) =
          MachineLookup.discard .work (labels (offset + i)) (labels (offset + i + 1)))
        (original suffix target scratch count spare : List Bool)
        (ambient : σ) (flag : Bool) (register : Option Bool) :
        (advance (TM2.step program))^[(encodeWords fields).length]
          (some ⟨some (labels offset), ((ambient, flag), register),
            memory original (encodeWords fields ++ suffix) target scratch count spare⟩) =
          some ⟨some (labels (offset + fields.length)),
            ((ambient, flag), if fields = [] then register else none),
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discard, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.memory

30. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Label line 271
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.skipLabel line 276
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowEntry line 279
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program line 287

    Source documentation

    A single fixed program copies the input once, skips two headers, then compares the first field of each 4098-field row.

    def program : Label → TM2.Stmt Alphabet Label (State σ)
      | .copyFirst => Reduction.MachineTransfer.loopAt
          .original .spare id false .copyFirst (some .copySecond)
      | .copySecond => MachineCopy.forkLoop
          .spare .original .work false .copySecond (some .headerFirst)
      | .headerFirst => MachineLookup.discard .work .headerFirst .headerSecond
      | .headerSecond => MachineLookup.discard .work .headerSecond .row
      | .row => rowEntry
      | .field => fieldLoop .field .restore
      | .restore => Reduction.MachineTransfer.loopAt
          .scratch .target id false .restore (some (skipLabel 0))
      | .skip i => MachineLookup.discard .work (.skip i) (skipLabel (i.val + 1))

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.State, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discard, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.skipLabel

34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program_skip line 300
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 305
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowStep_empty line 315
37. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Row line 321
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowWords line 323
39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowTime line 325
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowTrace line 329

    Source documentation

    One complete stored row is consumed; the target and original are restored.

    theorem rowTrace (r : Row) (hwidth : r.2.length = 4097) (v : Nat)
        (original suffix targetSuffix count spare : List Bool) (ambient : σ)
        (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[rowTime v r]
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Row, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowTime

41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsHits line 364
42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsTime line 368
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsTrace line 373

    Source documentation

    The complete actual row scan halts with the number of matching tails.

    theorem rowsTrace (rs : List Row) (hwidth : ∀ r ∈ rs, r.2.length = 4097) (v : Nat)
        (original targetSuffix count spare : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[rowsTime v rs]
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Row, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsTime

44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowTime_le line 397
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsTime_le line 406
46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.inputWord line 416
47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.inputWord_eq line 419
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.inputWord_length line 423
49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.totalSteps line 430
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.countTrace line 435

    Source documentation

    One preserving copy, the two concrete header discards, and the proved row scan form the complete execution. The input and target tapes are unchanged.

    theorem countTrace (n m v : Nat) (rs : List Row)
        (hwidth : ∀ r ∈ rs, r.2.length = 4097)
        (targetSuffix count : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[totalSteps n m v rs]
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.Row, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.totalSteps

51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.totalSteps_le line 470
52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows line 479
53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows_width line 483
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows_words line 489
55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows_input line 496
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 501
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 508
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 515
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows_hits line 521
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 529

    Source documentation

    Cloud size is produced by reading the actual encoded tail fields, with the complete graph input and unary vertex query preserved on their tapes.

    theorem cloudCountTrace (t : GraphTables.Table) (v : Fin t.vertices)
        (targetSuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[totalSteps t.vertices t.darts v.val (tableRows t)]
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.totalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.tableRows

61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 544

    Source documentation

    A linear transition budget for this concrete cloud-count subroutine.

    def cloudCountInTime (t : GraphTables.Table) (v : Fin t.vertices)
        (targetSuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program (σ := σ)))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.program