OAI/Computability/UniqueGames/Reduction/CloneMachineModelLemmas.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Affine word emission in the actual clone-table machine

The shared machine keeps its context fixed while copying one saved word. Its finite transducer therefore acts by a fixed symbol substitution. The lemmas below identify that substitution with the established unary encoding of offset + scale * value, including all header and equation-field contexts. Scale, offset, and the triple-table length remain symbolic.

  1. inductive OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.Tape line 18
  2. abbrev OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.Context line 22
  3. abbrev OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.State line 23
  4. abbrev OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.Alphabet line 24
  5. inductive OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.Label line 26
  6. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.defaultControl line 42
  7. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.initialState line 43
  8. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.headerTape line 45
  9. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.contextSource line 47
  10. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.contextScale line 51
  11. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.tripleField line 55
  12. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.contextOffset line 62
  13. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.affineEmit line 66
  14. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.emission line 70
  15. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.contextNext line 73
  16. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.cleanupNext line 80
  17. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.drain line 83
  18. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.program line 90
  19. def OAI.UniqueGamesTheorem.Reduction.CloneMachineModel.machine line 113
  20. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_eq_flatMap line 146

    Source documentation

    Identity control transitions reduce exactly to fixed symbol substitution.

    theorem output_eq_flatMap {Q : Type} [Fintype Q]
    (emit : Q → Bool → List Bool) (q : Q) (input : List Bool) :
    MachineTransducer.output (fun state _ => state) emit q input =
      input.flatMap (emit q) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output

  21. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_append line 155
  22. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.affineEmit_replicate_true line 162
  23. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.affineEmit_word line 170

    Source documentation

    This includes zero scale and zero offset, with no positivity assumptions.

    theorem affineEmit_word (scale offset v : Nat) :
    (encodeWord v).flatMap (affineEmit scale offset) =
      encodeWord (offset + scale * v) := by
…
  24. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.affineEmit_word_append line 177
  25. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.affineEmit_words line 182
  26. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_word line 191

    Source documentation

    Exact symbolic context transform used by the shared clone-table machine.

    theorem output_word (triples : List (Nat × Nat × Nat))
    (c : Context triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) c (encodeWord v) =
      encodeWord (contextOffset triples c + contextScale c * v) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output

  27. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_word_append line 198
  28. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_words line 205
  29. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_header_variables line 212
  30. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_header_count line 218

    Source documentation

    The equation-count multiplier remains the arbitrary symbolic table length.

    theorem output_header_count (triples : List (Nat × Nat × Nat)) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inl 1) (encodeWord v) =
      encodeWord (triples.length * v) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output

  31. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_field line 223
  32. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_first_field line 229
  33. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_second_field line 235
  34. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_third_field line 241
  35. theorem OAI.UniqueGamesTheorem.Reduction.CloneMachineAffine.output_rhs_field line 248

    Source documentation

    RHS words are copied exactly, including both legal Boolean values.

    theorem output_rhs_field (triples : List (Nat × Nat × Nat))
    (i : Fin triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inr (i, 3)) (encodeWord v) =
      encodeWord v := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output