OAI/Computability/MaxCut/Machines/CanonicalBodyMachine.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Lower a complete canonical-body template to the actual field-template machine. There are four saved fields per query position, numbered by field + 4 * position. The template constants depend only on finite coefficient and RHS data; names and occurrence identifiers remain saved tape contents.

  1. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.fieldEquiv line 21
  2. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.fieldIndex line 24
  3. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.fieldIndex_val line 27
  4. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.savedFields line 30
  5. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.savedFields_fieldIndex line 33
  6. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.lowerToken line 38
  7. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.lowerTemplate line 42
  8. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.lowerTemplate_length line 45
  9. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.tokenOutput_lowerToken line 48
  10. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.templateOutput_lowerTemplate line 55
  11. def OAI.MaxCutGames.Reduction.CanonicalBodyMachine.template line 64

    Source documentation

    This fixed token list is directly accepted by the actual template machine.

    def template {k s d : Nat} (z : Ambient s d) (a : Fin k → Fin 3 → Ambient s d)
    (b : Fin k → F2) : List (MachineFieldTemplate.Token (4*k)) :=
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token

  12. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.template_length line 68
  13. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.templateOutput_data line 73
  14. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.templateOutput_actualQuery line 82
  15. theorem OAI.MaxCutGames.Reduction.CanonicalBodyMachine.templateOutput_fromCoefficients line 92

    Source documentation

    Exact output using the finite coefficient table directly as program data.

    theorem templateOutput_fromCoefficients (S : ActualSource.Source) {k s d : Nat}
    (occ : ActualGame.Question S k) (c : ActualEnumeration.Coefficients k (Ambient s d)) :
    MachineFieldTemplate.templateOutput
        (template c.1 (CanonicalBodyTemplate.coefficientTriples c)
          (fun j => ActualGame.rhs S (occ j)))
        (savedFields (CanonicalBodyTemplate.sourceFields occ (ActualGame.names S))) =
      encodeWords (bodyWords (ActualOrbit.body (ActualGame.canonical S k s d)
        (occ, ActualEnumeration.fromCoefficients k (Ambient s d) c))) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.ActualGame.Question, OAI.MaxCutGames.Reduction.ActualEnumeration.Coefficients, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput, OAI.MaxCutGames.Reduction.CanonicalBodyMachine.template, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.coefficientTriples, OAI.MaxCutGames.Reduction.ActualGame.rhs, OAI.MaxCutGames.Reduction.CanonicalBodyMachine.savedFields, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields, OAI.MaxCutGames.Reduction.ActualGame.names, OAI.MaxCutGames.Reduction.ActualOrbit.body, OAI.MaxCutGames.Reduction.ActualGame.canonical, OAI.MaxCutGames.Reduction.ActualEnumeration.fromCoefficients

  16. abbrev OAI.MaxCutGames.Reduction.AddressMachineSpace.Extra line 108
  17. abbrev OAI.MaxCutGames.Reduction.AddressMachineSpace.Tape line 112
  18. abbrev OAI.MaxCutGames.Reduction.AddressMachineSpace.Control line 115
  19. abbrev OAI.MaxCutGames.Reduction.AddressMachineSpace.State line 116
  20. def OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState line 118
  21. def OAI.MaxCutGames.Reduction.AddressMachineSpace.headerArithmeticSlots line 122
  22. def OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape line 127
  23. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape_eq_iff line 130
  24. def OAI.MaxCutGames.Reduction.AddressMachineSpace.fullHeaderSlots line 134
  25. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.fullHeaderSlots_source line 146
  26. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.fullHeaderSlots_work line 147
  27. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.fullHeaderSlots_arithmetic line 148
  28. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.arithmeticSlots_fullHeaderSlots line 151
  29. def OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots line 155
  30. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots_source line 158
  31. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots_work line 159
  32. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots_variables line 160
  33. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots_occurrences line 162
  34. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.prefixSlots_scratch line 164
  35. def OAI.MaxCutGames.Reduction.AddressMachineSpace.canonicalField line 167
  36. def OAI.MaxCutGames.Reduction.AddressMachineSpace.rhsField line 170
  37. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.canonicalField_occurrence line 172
  38. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.canonicalField_name line 175
  39. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.canonicalField_ne_rhsField line 186
  40. def OAI.MaxCutGames.Reduction.AddressMachineSpace.privateAddress line 190
  41. def OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeSlot line 193
  42. def OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeDecode_inline_AddressMachineSpace line 204

    Source documentation

    A partial inverse proves separation without a default element of Fin k. It therefore applies unchanged at k = 0.

    private def edgeDecode_inline_AddressMachineSpace : Tape k s d noiseCount →
    Option (MachineAddressEdge.Tape (4 * k) (1 + 9 * k))
  | .savedIndex j => some (.inl (.field (CanonicalBodyMachine.fieldIndex j 3)))
  | .field j slot => if slot = 3 then none
      else some (.inl (.field (CanonicalBodyMachine.fieldIndex j slot)))
  | .extra (.inl (.inl .baseValue)) => some (.inl .radix)
  | .extra (.inl (.inl .capacity)) => some (.inr 0)
  | .extra (.inl (.inl .reversed)) => some (.inr 1)
  | .extra (.inr (.inl tape)) => some (.inl tape)
  | _ => none

    Mentions: OAI.MaxCutGames.Reduction.AddressMachineSpace.Tape, OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.CanonicalBodyMachine.fieldIndex

  43. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeDecode_canonicalField_inline_AddressMachineSpace line 215
  44. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeDecode_edgeSlot_inline_AddressMachineSpace line 220
  45. def OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots line 230
  46. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_fieldIndex line 238
  47. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressSlots_name line 249
  48. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressSlots_occurrence line 256
  49. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressSlots_radix line 262
  50. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressSlots_capacity line 265
  51. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressSlots_output line 268
  52. def OAI.MaxCutGames.Reduction.AddressMachineSpace.current line 272
  53. def OAI.MaxCutGames.Reduction.AddressMachineSpace.remaining line 273
  54. def OAI.MaxCutGames.Reduction.AddressMachineSpace.finalOutput line 274
  55. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.current_rev line 276
  56. def OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots line 279
  57. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots_radix line 290
  58. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots_scratch line 292
  59. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots_current line 293
  60. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots_remaining line 295
  61. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.current_ne_remaining line 298
  62. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.current_ne_finalOutput line 300
  63. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.remaining_ne_finalOutput line 302
  64. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.edgeSlot_ne_of_decode_none_inline_AddressMachineSpace line 305
  65. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_rhsField line 313
  66. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_source line 318
  67. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_copyScratch line 323
  68. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_headerTape line 330

    Source documentation

    Only the radix, capacity, and reversed accumulator intentionally overlap the address emitter's tapes with the arithmetic block.

    theorem addressEdgeSlots_ne_headerTape
    (tape : MachineAddressEdge.Tape (4 * k) (1 + 9 * k))
    (c : MachineAddressHeaders.Arithmetic.Control)
    (hb : c ≠ .baseValue) (hc : c ≠ .capacity) (hr : c ≠ .reversed) :
    addressEdgeSlots k s d noiseCount tape ≠ headerTape k s d noiseCount c := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control, OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots, OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape

  69. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_remaining line 338
  70. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots_ne_finalOutput line 343
  71. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape_ne_finalOutput line 348
  72. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape_ne_current line 352
  73. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.headerTape_ne_remaining line 356
  74. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.tupleOutput_headerTape line 360
  75. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.tupleOutput_source line 370
  76. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.tupleOutput_rhs line 375
  77. theorem OAI.MaxCutGames.Reduction.AddressMachineSpace.tupleOutput_occurrence line 383