OAI/Computability/UniqueGames/Machines/PoweringMachineEqualityField.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Actual producer for equality of two bounded walk endpoints

The two port words are fixed finite control. Each executes against the live rotor table from the same preserved starting vertex. Their endpoint fields are compared by the physical unary equality primitive. The emitted field is the Boolean equality of the two actual walk endpoints.

Work tapes may retain arbitrary histories. The table, start, scratch and two comparison copies satisfy exact frame theorems. There is no execution or running-time premise in the composite trace theorem.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 30
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.Tape line 31
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.State line 32
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.Label line 33
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.entry line 36
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.instruction line 38
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 54
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 58
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 62
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 68
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.steps line 78
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 85
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 103

    Source documentation

    The only variable-size work areas changed by a word are the declared query, scan, reverse, selected endpoint, and trajectory tapes.

    theorem wordTapes_other (graph : PortTables.Table n d) {t : Nat} (h : t ≤ max)
    (placement : Tape max → K) (target : Bool) (vertex : Fin n)
    (ports : Fin t → Fin d) (base : K → List Bool) (k : K)
    (hquery : k ≠ placement (.inl 2)) (hscan : k ≠ placement (.inl 3))
    (hreverse : k ≠ placement (.inl 4))
    (houtput : k ≠ placement (PoweringMachineTapes.endpoint max target))
    (hpositions : ∀ i : Fin max, k ≠ placement (.inr i)) :
    wordTapes graph h placement target vertex ports base k = base k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.endpoint, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.wordTapes

  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 123
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 144
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 160

    Source documentation

    This single statement covers table 0, start 1, scratch 5, and copies 8/9.

    theorem finalTapes_role (graph : PortTables.Table n d) (hl : l ≤ max) (hr : r ≤ max)
    (placement : Tape max → K) (distinct : Function.Injective placement) (vertex : Fin n)
    (left : Fin l → Fin d) (right : Fin r → Fin d) (base : K → List Bool)
    (j : Fin 11) (hrole : j = 0 ∨ j = 1 ∨ j = 5 ∨ j = 8 ∨ j = 9) :
    finalTapes graph hl hr placement vertex left right base (placement (.inl j)) =
      base (placement (.inl j)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.finalTapes

  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 171
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.joinTrace line 184
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 188
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 290
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineEqualityField.machine line 313